summaryrefslogtreecommitdiffstats
path: root/server
diff options
context:
space:
mode:
authorRutger Broekhoff2026-08-28 18:03:05 +0200
committerRutger Broekhoff2026-08-28 18:03:05 +0200
commit973aec43ea54bbf95b64fbcb636403401d1ca60e (patch)
tree41b7911c420766a9b463245b9296f44c5bf35258 /server
downloadroutemon-973aec43ea54bbf95b64fbcb636403401d1ca60e.tar.gz
routemon-973aec43ea54bbf95b64fbcb636403401d1ca60e.zip
Import from e4b104792206ee7ea64bf39c6b7d2c0c230f9d14
Diffstat (limited to 'server')
-rw-r--r--server/.gitignore7
-rw-r--r--server/CMakeLists.txt86
-rw-r--r--server/CMakePresets.json29
-rw-r--r--server/README16
-rw-r--r--server/ct.sh1
-rw-r--r--server/formal/.envrc1
-rw-r--r--server/formal/.gitignore17
-rw-r--r--server/formal/Makefile55
-rw-r--r--server/formal/_CoqProject5
-rw-r--r--server/formal/flake.lock61
-rw-r--r--server/formal/flake.nix26
-rw-r--r--server/formal/period.v828
-rw-r--r--server/formal/period_seq.v834
-rw-r--r--server/formal/util.v92
-rwxr-xr-xserver/hack/rwgps-get-auth-token.sh14
-rw-r--r--server/locale/.gitignore1
-rw-r--r--server/locale/README9
-rwxr-xr-xserver/locale/dev.sh7
-rw-r--r--server/locale/en_US.po64
-rw-r--r--server/locale/nl.po64
-rwxr-xr-xserver/locale/xget.sh13
-rw-r--r--server/migrations/1_init_down.sql1
-rw-r--r--server/migrations/1_init_up.sql7
-rw-r--r--server/migrations/2_kaas_up.sql23
-rw-r--r--server/routemon.pot58
-rw-r--r--server/src/api.cpp206
-rw-r--r--server/src/api.cppm79
-rw-r--r--server/src/config.cpp167
-rw-r--r--server/src/config.cppm39
-rw-r--r--server/src/database.cppm37
-rw-r--r--server/src/datex2.cppm296
-rw-r--r--server/src/geo.cppm40
-rw-r--r--server/src/gpx.cpp189
-rw-r--r--server/src/gpx.cppm43
-rw-r--r--server/src/http_client.cppm62
-rw-r--r--server/src/http_common.cppm139
-rw-r--r--server/src/http_server.cppm661
-rw-r--r--server/src/locale.cppm245
-rw-r--r--server/src/log.cppm148
-rw-r--r--server/src/main.cpp109
-rw-r--r--server/src/problem.cppm60
-rw-r--r--server/src/req_ctx.cppm51
-rw-r--r--server/src/routemon.cppm11
-rw-r--r--server/src/rwgps.cppm137
-rw-r--r--server/src/sqlite3.cppm257
-rw-r--r--server/src/srv.cppm221
-rw-r--r--server/src/time.cppm205
-rw-r--r--server/src/trace.cppm79
-rw-r--r--server/src/util.cppm254
-rw-r--r--server/src/xml.cpp61
-rw-r--r--server/src/xml.cppm632
51 files changed, 6747 insertions, 0 deletions
diff --git a/server/.gitignore b/server/.gitignore
new file mode 100644
index 0000000..0751de2
--- /dev/null
+++ b/server/.gitignore
@@ -0,0 +1,7 @@
1assets/
2src/*.o
3src/*.d
4build/
5config.json
6*.sqlite3
7vendor/
diff --git a/server/CMakeLists.txt b/server/CMakeLists.txt
new file mode 100644
index 0000000..df4eb90
--- /dev/null
+++ b/server/CMakeLists.txt
@@ -0,0 +1,86 @@
1cmake_minimum_required(VERSION 4.3)
2
3project(routemon LANGUAGES CXX)
4
5# Hardening options from https://best.openssf.org/Compiler-Hardening-Guides/Compiler-Options-Hardening-Guide-for-C-and-C++.html
6add_compile_options(
7 # -O2
8 # -g
9 -fno-omit-frame-pointer
10 -Wall -Wextra -Wformat -Wformat=2 -Wconversion -Wimplicit-fallthrough
11 -Werror=format-security
12 -U_FORTIFY_SOURCE # -D_FORTIFY_SOURCE=3 (unfortunately breaks the std module)
13 -D_GLIBCXX_ASSERTIONS
14 -fstrict-flex-arrays=3
15 -fstack-clash-protection -fstack-protector-strong
16 -fPIE -fcf-protection=full
17 -fno-delete-null-pointer-checks -fno-strict-overflow -fno-strict-aliasing -ftrivial-auto-var-init=zero
18 -DBOOST_ASIO_NO_DEPRECATED
19)
20add_link_options(
21 -pie
22 -Wl,-z,nodlopen -Wl,-z,noexecstack
23 -Wl,-z,relro -Wl,-z,now
24 -Wl,--as-needed -Wl,--no-copy-dt-needed-entries
25)
26
27add_library(routemon_lib)
28target_sources(routemon_lib
29 PUBLIC FILE_SET CXX_MODULES FILES
30 src/api.cppm
31 src/api.cpp
32 src/database.cppm
33 src/config.cppm
34 src/config.cpp
35 src/datex2.cppm
36 src/geo.cppm
37 src/gpx.cppm
38 src/gpx.cpp
39 src/http_client.cppm
40 src/http_common.cppm
41 src/http_server.cppm
42 src/locale.cppm
43 src/log.cppm
44 src/problem.cppm
45 src/req_ctx.cppm
46 src/routemon.cppm
47 src/rwgps.cppm
48 src/sqlite3.cppm
49 src/srv.cppm
50 src/time.cppm
51 src/trace.cppm
52 src/util.cppm
53 src/xml.cppm
54 src/xml.cpp
55)
56
57add_executable(routemon src/main.cpp)
58target_link_libraries(routemon routemon_lib)
59install(TARGETS routemon)
60
61find_package(Boost 1.90 REQUIRED COMPONENTS json locale url)
62target_link_libraries(routemon_lib Boost::headers Boost::json Boost::locale Boost::url)
63
64# Already arranged via Boost::locale but this makes it more explicit, I guess
65find_package(ICU REQUIRED COMPONENTS data i18n uc)
66target_link_libraries(routemon_lib ICU::data ICU::i18n ICU::uc)
67
68find_library(pugixml pugixml REQUIRED)
69target_link_libraries(routemon_lib pugixml)
70
71find_package(OpenSSL REQUIRED)
72target_link_libraries(routemon_lib OpenSSL::SSL)
73
74find_package(SQLite3 REQUIRED)
75target_link_libraries(routemon_lib SQLite3::SQLite3)
76
77find_package(Gettext REQUIRED)
78gettext_create_translations(
79 routemon.pot
80 ALL
81 locale/nl.po
82 locale/en_US.po
83)
84
85find_package(expat REQUIRED)
86target_link_libraries(routemon_lib expat::expat)
diff --git a/server/CMakePresets.json b/server/CMakePresets.json
new file mode 100644
index 0000000..ae7fd67
--- /dev/null
+++ b/server/CMakePresets.json
@@ -0,0 +1,29 @@
1{
2 "version": 4,
3 "configurePresets": [
4 {
5 "name": "arch",
6 "binaryDir": "${sourceDir}/build",
7 "generator": "Ninja",
8 "cacheVariables": {
9 "CMAKE_CXX_STANDARD": "26",
10 "CMAKE_COLOR_DIAGNOSTICS": true,
11 "CMAKE_EXPERIMENTAL_CXX_IMPORT_STD": "f35a9ac6-8463-4d38-8eec-5d6008153e7d",
12 "CMAKE_CXX_EXTENSIONS": false,
13 "CMAKE_CXX_MODULE_STD": true,
14 "CMAKE_EXPORT_COMPILE_COMMANDS": true
15 }
16 },
17 {
18 "name": "nix-derivation",
19 "cacheVariables": {
20 "CMAKE_CXX_STANDARD": "26",
21 "CMAKE_COLOR_DIAGNOSTICS": true,
22 "CMAKE_EXPERIMENTAL_CXX_IMPORT_STD": "451f2fe2-a8a2-47c3-bc32-94786d8fc91b",
23 "CMAKE_CXX_EXTENSIONS": false,
24 "CMAKE_CXX_MODULE_STD": true,
25 "CMAKE_EXPORT_COMPILE_COMMANDS": true
26 }
27 }
28 ]
29}
diff --git a/server/README b/server/README
new file mode 100644
index 0000000..04d5d5a
--- /dev/null
+++ b/server/README
@@ -0,0 +1,16 @@
1# Configure
2
3$ cmake --preset arch # (--fresh if the build folder already exists)
4
5# Build
6
7$ cmake --build build
8
9# Dependencies (and versions known to work)
10
11- CMake 4.3.4
12- clang version 22.1.6
13- Boost 1.91
14- pugixml 1.16
15- OpenSSL
16- ICU \ No newline at end of file
diff --git a/server/ct.sh b/server/ct.sh
new file mode 100644
index 0000000..29ad28b
--- /dev/null
+++ b/server/ct.sh
@@ -0,0 +1 @@
clang-tidy -checks='boost-*,bugprone-*,clang-analyzer-*,concurrency-*,cppcoreguidlines-*,misc-*,-misc-include-cleaner,-misc-no-recursion,-misc-use-internal-linkage,modernize-*,performance-*,portability-*,radability-*' -p build '--exclude-header-filter=.*' src/time.cpp
diff --git a/server/formal/.envrc b/server/formal/.envrc
new file mode 100644
index 0000000..3550a30
--- /dev/null
+++ b/server/formal/.envrc
@@ -0,0 +1 @@
use flake
diff --git a/server/formal/.gitignore b/server/formal/.gitignore
new file mode 100644
index 0000000..9023475
--- /dev/null
+++ b/server/formal/.gitignore
@@ -0,0 +1,17 @@
1*.aux
2*.glob
3*.vio
4*.vo
5*.vok
6*.vos
7.CoqMakefile.d
8.Makefile.coq.d
9.direnv
10.lia.cache
11Makefile.coq
12Makefile.coq.conf
13*#*.v#
14*#*.vok#
15*~
16.#*
17\#*# \ No newline at end of file
diff --git a/server/formal/Makefile b/server/formal/Makefile
new file mode 100644
index 0000000..ac8dba0
--- /dev/null
+++ b/server/formal/Makefile
@@ -0,0 +1,55 @@
1# Default target
2all: Makefile.coq
3 +@$(MAKE) -f Makefile.coq all
4.PHONY: all
5
6# Permit local customization
7-include Makefile.local
8
9# Forward most targets to Coq makefile (with some trick to make this phony)
10%: Makefile.coq phony
11 @#echo "Forwarding $@"
12 +@$(MAKE) -f Makefile.coq $@
13phony: ;
14.PHONY: phony
15
16clean: Makefile.coq
17 +@$(MAKE) -f Makefile.coq clean
18 @# Make sure not to enter the `_opam` folder.
19 find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
20 rm -f Makefile.coq .lia.cache builddep/*
21.PHONY: clean
22
23# Create Coq Makefile.
24Makefile.coq: _CoqProject Makefile
25 "$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
26
27# Install build-dependencies
28OPAMFILES=$(wildcard *.opam)
29BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
30
31builddep/%-builddep.opam: %.opam Makefile
32 @echo "# Creating builddep package for $<."
33 @mkdir -p builddep
34 @sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
35
36builddep-opamfiles: $(BUILDDEPFILES)
37.PHONY: builddep-opamfiles
38
39builddep: builddep-opamfiles
40 @# We want opam to not just install the build-deps now, but to also keep satisfying these
41 @# constraints. Otherwise, `opam upgrade` may well update some packages to versions
42 @# that are incompatible with our build requirements.
43 @# To achieve this, we create a fake opam package that has our build-dependencies as
44 @# dependencies, but does not actually install anything itself.
45 @echo "# Installing builddep packages."
46 @opam install $(OPAMFLAGS) $(BUILDDEPFILES)
47.PHONY: builddep
48
49# Backwards compatibility target
50build-dep: builddep
51.PHONY: build-dep
52
53# Some files that do *not* need to be forwarded to Makefile.coq.
54# ("::" lets Makefile.local overwrite this.)
55Makefile Makefile.local _CoqProject $(OPAMFILES):: ;
diff --git a/server/formal/_CoqProject b/server/formal/_CoqProject
new file mode 100644
index 0000000..92d635c
--- /dev/null
+++ b/server/formal/_CoqProject
@@ -0,0 +1,5 @@
1-Q . routemon
2
3util.v
4period.v
5period_seq.v \ No newline at end of file
diff --git a/server/formal/flake.lock b/server/formal/flake.lock
new file mode 100644
index 0000000..f4a7de9
--- /dev/null
+++ b/server/formal/flake.lock
@@ -0,0 +1,61 @@
1{
2 "nodes": {
3 "flake-utils": {
4 "inputs": {
5 "systems": "systems"
6 },
7 "locked": {
8 "lastModified": 1731533236,
9 "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
10 "owner": "numtide",
11 "repo": "flake-utils",
12 "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
13 "type": "github"
14 },
15 "original": {
16 "owner": "numtide",
17 "repo": "flake-utils",
18 "type": "github"
19 }
20 },
21 "nixpkgs": {
22 "locked": {
23 "lastModified": 1777077449,
24 "narHash": "sha256-AIiMJiqvGrN4HyLEbKAoCSRRYn0rnlW5VbKNIMIYqm4=",
25 "owner": "NixOS",
26 "repo": "nixpkgs",
27 "rev": "a4bf06618f0b5ee50f14ed8f0da77d34ecc19160",
28 "type": "github"
29 },
30 "original": {
31 "owner": "NixOS",
32 "ref": "nixos-25.11",
33 "repo": "nixpkgs",
34 "type": "github"
35 }
36 },
37 "root": {
38 "inputs": {
39 "flake-utils": "flake-utils",
40 "nixpkgs": "nixpkgs"
41 }
42 },
43 "systems": {
44 "locked": {
45 "lastModified": 1681028828,
46 "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
47 "owner": "nix-systems",
48 "repo": "default",
49 "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
50 "type": "github"
51 },
52 "original": {
53 "owner": "nix-systems",
54 "repo": "default",
55 "type": "github"
56 }
57 }
58 },
59 "root": "root",
60 "version": 7
61}
diff --git a/server/formal/flake.nix b/server/formal/flake.nix
new file mode 100644
index 0000000..57efa11
--- /dev/null
+++ b/server/formal/flake.nix
@@ -0,0 +1,26 @@
1{
2 inputs = {
3 nixpkgs.url = "github:NixOS/nixpkgs/nixos-25.11";
4 flake-utils.url = "github:numtide/flake-utils";
5 };
6
7 outputs = { self, nixpkgs, flake-utils, ... }:
8 flake-utils.lib.eachDefaultSystem (system:
9 let
10 pkgs = import nixpkgs { inherit system; };
11
12 # From 22-04-2026
13 stdpp = with pkgs; coqPackages.lib.overrideCoqDerivation {
14 version = "dev";
15 release."dev".sha256 = "hN+sEZcIaFoFF2+4dStTc0TRz5A03US6csEk5q0r/z8=";
16 release."dev".rev = "d3c67aa46ed22b1e593457cd34fc711f1a53b8be";
17 } coqPackages.stdpp;
18 in
19 {
20 devShells.default = with pkgs; mkShell {
21 buildInputs = [ coq stdpp ];
22 };
23
24 formatter = pkgs.nixpkgs-fmt;
25 });
26}
diff --git a/server/formal/period.v b/server/formal/period.v
new file mode 100644
index 0000000..82921db
--- /dev/null
+++ b/server/formal/period.v
@@ -0,0 +1,828 @@
1From stdpp Require Import numbers option sorting ssreflect.
2From stdpp Require Import options.
3From routemon Require Import util.
4
5Definition timestamp := Z.
6Variant limit :=
7 | NegInftyLimit
8 | TsLimit (x : timestamp)
9 | PosInftyLimit.
10Instance limit_eq_dec : EqDecision limit.
11Proof. solve_decision. Qed.
12
13Notation "-∞" := NegInftyLimit.
14Notation "+∞" := PosInftyLimit.
15Coercion TsLimit : timestamp >-> limit.
16
17(* The interval [start, end). Considered empty when start >= end. *)
18Record period :=
19 Period
20 { period_start : limit
21 ; period_end : limit
22 }.
23Notation "'[' s ',' e ')'" := (Period s e).
24
25(* Consider making an inductive variant of these? *)
26Definition limit_le (l1 l2 : limit) :=
27 match l1, l2 with
28 | -∞, _ | _, +∞ => True
29 | TsLimit t1, TsLimit t2 => (t1 ≤ t2)%Z
30 | _, _ => False
31 end.
32Arguments limit_le !_ !_ / : assert.
33Definition limit_lt l1 l2 :=
34 match l1 with
35 | -∞ =>
36 match l2 with
37 | -∞ => False
38 | _ => True
39 end
40 | TsLimit t1 =>
41 match l2 with
42 | -∞ => False
43 | TsLimit t2 => (t1 < t2)%Z
44 | +∞ => True
45 end
46 | +∞ => False
47 end.
48Arguments limit_lt !_ !_ / : assert.
49Instance limit_le_dec : RelDecision limit_le.
50Proof. intros [] []; simpl; solve_decision. Qed.
51Instance limit_lt_dec : RelDecision limit_lt.
52Proof. intros [] []; simpl; solve_decision. Qed.
53Instance limit_lt_pi l1 l2 : ProofIrrel (limit_lt l1 l2).
54Proof. destruct l1, l2; apply _. Qed.
55
56Instance relation_equiv {A} : Equiv (relation A) :=
57 λ R1 R2, ∀ x y, R1 x y ↔ R2 x y.
58
59Lemma strict_limit_le_limit_lt :
60 strict limit_le ≡ limit_lt.
61Proof.
62 split.
63 - intros []. destruct x, y; simpl in *; try done. lia.
64 - intros H. destruct x, y; unfold strict; simpl in *; try done; auto with lia.
65Qed.
66
67Instance : Reflexive limit_le.
68Proof. intros l. by destruct l; simpl. Qed.
69Instance : Transitive limit_le.
70Proof. intros [] [] []; simpl; try done. lia. Qed.
71Instance : PreOrder limit_le.
72Proof. constructor; apply _. Qed.
73Instance : AntiSymm (=) limit_le.
74Proof.
75 intros [] []; simpl; try done.
76 intros H1 H2. f_equal. by apply Z.le_antisymm.
77Qed.
78Instance : PartialOrder limit_le.
79Proof. constructor; apply _. Qed.
80Instance : Trichotomy (strict limit_le).
81Proof with auto with lia.
82 intros [] []; unfold strict; simpl...
83 destruct (Z.lt_trichotomy x x0) as [H|[->|H]]...
84Qed.
85Instance : TotalOrder limit_le.
86Proof. constructor; apply _. Qed.
87
88Instance : StrictOrder (strict limit_le) := _.
89(* TODO: apparently useless??
90Instance rel_equiv_proper {A} (x y : A) : Proper ((≡) ==> (↔)) (λ R, R x y).
91Proof. easy. Qed.
92Search Proper iff eq.
93*)
94Instance complement_equiv {A} : Proper ((≡) ==> (≡)) (@complement A).
95Proof. intros R1 R2 HR12. split; unfold complement; intros Hequiv []%HR12%Hequiv. Qed.
96Instance Reflexive_equiv {A} : Proper ((≡) ==> (↔)) (@Reflexive A).
97Proof.
98 intros R1 R2 Hequiv. unfold Reflexive.
99 split; intros H x; by apply Hequiv.
100Qed.
101Instance Irreflexive_equiv {A} : Proper ((≡) ==> (↔)) (@Irreflexive A).
102Proof. unfold Irreflexive. by intros R1 R2 ->. Qed.
103Instance Transitive_equiv {A} : Proper ((≡) ==> (↔)) (@Transitive A).
104Proof.
105 intros R1 R2 Hequiv. unfold Transitive.
106 by split; intros H x y z Hxy%Hequiv Hyz%Hequiv; eapply Hequiv, H.
107Qed.
108Instance StrictOrder_equiv {A} : Proper ((≡) ==> (↔)) (@StrictOrder A).
109Proof.
110 intros R1 R2 Hequiv. split; intros [Hirr Htrans].
111 - by rewrite ->Hequiv in Hirr, Htrans.
112 - by rewrite <-Hequiv in Hirr, Htrans.
113Qed.
114Instance Trichotomy_equiv {A} : Proper ((≡) ==> (↔)) (@Trichotomy A).
115Proof.
116 intros R1 R2 Hequiv. split; intros.
117 - intros x y. by rewrite -(Hequiv x y) -(Hequiv y x).
118 - intros x y. by rewrite (Hequiv x y) (Hequiv y x).
119Qed.
120
121Instance : StrictOrder limit_lt.
122Proof. rewrite -strict_limit_le_limit_lt. apply _. Qed.
123Instance : Trichotomy limit_lt.
124Proof. rewrite -strict_limit_le_limit_lt. apply _. Qed.
125
126Definition limit_lt_ts' (l : limit) (t2 : timestamp) :=
127 match l with
128 | -∞ => True
129 | TsLimit t1 => (t1 < t2)%Z
130 | +∞ => False
131 end.
132Definition ts_le_limit' (t1 : timestamp) (l : limit) :=
133 match l with
134 | -∞ => False
135 | TsLimit t2 => (t1 ≤ t2)%Z
136 | +∞ => True
137 end.
138Lemma limit_lt_limit_lt_ts' l t2 : limit_lt_ts' l t2 ↔ limit_lt l t2.
139Proof. by destruct l. Qed.
140Lemma ts_le_limit'_limit_le t1 l : ts_le_limit' t1 l ↔ limit_le t1 l.
141Proof. by destruct l. Qed.
142
143Declare Scope limit_scope.
144Delimit Scope limit_scope with lim.
145Notation "l1 < l2" := (limit_lt l1 l2) : limit_scope.
146Notation "l1 ≤ l2" := (limit_le l1 l2) : limit_scope.
147Notation "l1 < l2 < l3" := (l1 < l2 ∧ l2 < l3)%lim : limit_scope.
148Notation "l1 ≤ l2 < l3" := (l1 ≤ l2 ∧ l2 < l3)%lim : limit_scope.
149Notation "l1 < l2 ≤ l3" := (l1 < l2 ∧ l2 ≤ l3)%lim : limit_scope.
150Notation "l1 ≤ l2 ≤ l3" := (l1 ≤ l2 ∧ l2 ≤ l3)%lim : limit_scope.
151Open Scope limit_scope.
152
153Instance period_elem_of : ElemOf timestamp period :=
154 λ t '[s, e), (s ≤ t < e).
155Instance period_elem_of_dec t (p : period) : Decision (t ∈ p).
156Proof. destruct p as [s e]. apply _. Qed.
157
158Lemma limit_le_lt l1 l2 : l1 < l2 ↔ l1 ≤ l2 ∧ l1 ≠ l2.
159Proof. by rewrite -(strict_limit_le_limit_lt l1 l2) strict_spec_alt. Qed.
160
161Lemma limit_le_cases {l1 l2} : l1 ≤ l2 ↔ l1 = l2 ∨ l1 < l2.
162Proof.
163 rewrite -(strict_limit_le_limit_lt l1 l2) strict_spec_alt. split.
164 - intros Hl12. destruct (decide (l1 = l2)) as [<-|Hne]; tauto.
165 - by intros [<-|[Hl12 _]].
166Qed.
167
168Lemma limit_lt_le_lt {l1} l2 {l3} : l1 ≤ l2 < l3 → l1 < l3.
169Proof. by intros [[<-|?]%limit_le_cases ?]; last etrans. Qed.
170
171Definition period_empty '[s, e) := e ≤ s.
172Definition period_empty_alt (p : period) := ∀ t, t ∉ p.
173Lemma period_empty_alt_iff p : period_empty p ↔ period_empty_alt p.
174Proof.
175 destruct p as [s e].
176 rewrite /period_empty /period_empty_alt /=.
177 split; intros H.
178 - intros t [contra []]%limit_lt_le_lt%limit_le_lt.
179 by eapply (anti_symm limit_le).
180 - destruct s as [|s|], e as [|e|]; try done.
181 + exfalso. apply (H (Z.pred e)). rewrite /elem_of /period_elem_of /=. lia.
182 + exfalso. by apply (H 0%Z).
183 + rewrite /elem_of /period_elem_of /= in H.
184 specialize (H s). simpl. lia.
185 + exfalso. apply (H s). rewrite /elem_of /period_elem_of /=. lia.
186Qed.
187Instance period_empty_dec p : Decision (period_empty p).
188Proof. destruct p as [s e]. solve_decision. Qed.
189
190Definition period_nonempty '[s, e) := s < e.
191Instance period_nonempty_dec p : Decision (period_nonempty p).
192Proof. destruct p. apply _. Qed.
193Instance period_nonempty_pi p : ProofIrrel (period_nonempty p).
194Proof. destruct p. apply _. Qed.
195
196Instance period_equiv : Equiv period :=
197 λ p1 p2, ∀ t, t ∈ p1 ↔ t ∈ p2.
198Instance period_equiv_reflexive : Reflexive period_equiv.
199Proof. done. Qed.
200Instance period_equiv_trans : Transitive period_equiv.
201Proof. intros p1 p2 p3 H1 H2 t. by rewrite H1. Qed.
202Instance period_equiv_symm : Symmetric period_equiv.
203Proof. by intros p1 p2 H t. Qed.
204Instance period_equiv_equiv : Equivalence period_equiv.
205Proof. constructor; apply _. Qed.
206
207(* All empty periods are equivalent *)
208Lemma period_empty_equiv p1 p2 : period_empty p1 → period_empty p2 ↔ p1 ≡ p2.
209Proof.
210 intros Hp1%period_empty_alt_iff. split.
211 - intros Hp2%period_empty_alt_iff. intros t.
212 split; [intros []%(Hp1 _) | intros []%(Hp2 _)].
213 - intros Hequiv. apply period_empty_alt_iff.
214 intros t []%Hequiv%(Hp1 _).
215Qed.
216
217Instance empty_period : Empty period := [TsLimit 0%Z, TsLimit 0%Z).
218Definition empty_period_empty : period_empty empty_period.
219Proof. done. Qed.
220
221Definition limit_min (l1 l2 : limit) := if decide (l1 ≤ l2) then l1 else l2.
222Definition limit_max (l1 l2 : limit) := if decide (l1 ≤ l2) then l2 else l1.
223
224Notation "l1 '`min`' l2" := (limit_min l1 l2) : limit_scope.
225Notation "l1 '`max`' l2" := (limit_max l1 l2) : limit_scope.
226
227Definition limit_min_ts (t1 t2 : timestamp) :
228 t1 `min` t2 = TsLimit (t1 `min` t2)%Z.
229Proof.
230 unfold limit_min.
231 destruct (decide (t1 ≤ t2));
232 simpl in *; f_equal; lia.
233Qed.
234
235Definition limit_max_ts (t1 t2 : timestamp) :
236 t1 `max` t2 = TsLimit (t1 `max` t2)%Z.
237Proof.
238 unfold limit_max.
239 destruct (decide (t1 ≤ t2));
240 simpl in *; f_equal; lia.
241Qed.
242
243Instance period_intersection : Intersection period := λ '[s1, e1) '[s2, e2),
244 [ s1 `max` s2, e1 `min` e2 ).
245
246Lemma intersect_and (p1 p2 : period) t :
247 t ∈ (p1 ∩ p2) ↔ t ∈ p1 ∧ t ∈ p2.
248Proof.
249 (* It really should be possible to optimize this proof somehow. *)
250 destruct p1 as [[|s1|] [|e1|]], p2 as [[|s2|] [|e2|]];
251 rewrite /intersection /period_intersection /elem_of /period_elem_of /limit_min /limit_max /limit_le /limit_lt /=;
252 repeat case_decide; tauto || lia.
253Qed.
254
255(* The points in time given by p1 except those given by p2, given as a before/after pair. *)
256Definition except '[s1, e1) '[s2, e2) : period * period :=
257 ( [ s1, e1 `min` s2 ),
258 [ s1 `max` e2, e1 ) ).
259
260Lemma limit_lt_ne l1 l2 : l1 < l2 → l1 ≠ l2.
261Proof. rewrite -(strict_limit_le_limit_lt l1 l2) strict_spec_alt. easy. Qed.
262
263Lemma not_limit_le l1 l2 : ¬ (l1 ≤ l2) ↔ l2 < l1.
264Proof.
265 destruct (trichotomy limit_lt l1 l2) as [Hl12|[<-|Hl21]].
266 - split; intros H.
267 + exfalso. apply H, limit_le_cases. by right.
268 + exfalso. by eapply asymmetry.
269 - split; intros H.
270 + exfalso. apply H, limit_le_cases. by left.
271 + by apply (_ : Irreflexive limit_lt) in H.
272 - split; intros H; first done.
273 intros [<-|Hl12]%limit_le_cases.
274 + by apply (_ : Irreflexive limit_lt) in H.
275 + by eapply asymmetry.
276Qed.
277
278Lemma not_limit_le' : complement limit_le ≡ flip limit_lt.
279Proof. apply: not_limit_le. Qed.
280
281Instance relation_equiv_reflexive {A} : Reflexive (@relation_equiv A).
282Proof. done. Qed.
283Instance relation_equiv_trans {A} : Transitive (@relation_equiv A).
284Proof. intros R1 R2 R3 H12 H23 x y. by rewrite H12 -H23. Qed.
285Instance relation_equiv_symm {A} : Symmetric (@relation_equiv A).
286Proof. by intros R1 R2 H12 x y. Qed.
287Instance relation_equiv_equiv {A} : Equivalence (@relation_equiv A).
288Proof. constructor; apply _. Qed.
289
290Lemma relation_flip_equiv {A} : Proper ((≡@{relation A}) ==> (≡)) flip.
291Proof. intros R1 R2 H12 x y. simpl. by rewrite (H12 y x). Qed.
292
293(* Could also be more generic *)
294Lemma relation_flip_involutive {A} (R : relation A) : flip (flip R) ≡ R.
295Proof. done. Qed.
296
297Lemma complement_involutive {A} `{!RelDecision (R : relation A)} : complement (complement R) ≡ R.
298Proof.
299 intros x y. split; intros Hxy.
300 - by destruct (decide (R x y)).
301 - by apply.
302Qed.
303
304Lemma not_limit_lt' : complement limit_lt ≡ flip limit_le.
305Proof.
306 rewrite -(relation_flip_involutive limit_lt) complement_inverse.
307 trans (flip (complement (complement limit_le))).
308 { apply relation_flip_equiv, complement_equiv, symmetry, not_limit_le'. }
309 apply relation_flip_equiv, complement_involutive.
310Qed.
311
312Lemma not_limit_lt l1 l2 : ¬ (l1 < l2) ↔ l2 ≤ l1.
313Proof. apply not_limit_lt'. Qed.
314
315(* TODO: make conclusion positive? *)
316Lemma period_nonempty_equiv_L_1 (s1 e1 s2 e2 : limit) :
317 period_nonempty [s1, e1) →
318 period_nonempty [s2, e2) →
319 [s1, e1) ≡ [s2, e2) →
320 ¬ s1 < s2.
321Proof.
322 unfold period_nonempty.
323 intros Hne1 Hne2 Hequiv Hs12.
324 destruct s2 as [|s2|]; [by destruct s1|..|by destruct s1].
325 destruct s1 as [|s1|]; last done.
326 * assert (Hs2a : s2 ∈ [s2, e2)).
327 { unfold elem_of, period_elem_of. by destruct e2. }
328 pose proof (proj2 (Hequiv s2) Hs2a) as [_ Hs2b].
329 assert (Hs2c : Z.pred s2 ∈ [-∞, e1)).
330 { unfold elem_of, period_elem_of.
331 by destruct e1 as [|e1|]; [|simpl in *; lia|]. }
332 pose proof (proj1 (Hequiv (Z.pred s2)) Hs2c) as [contra _].
333 simpl in contra. lia.
334 * assert (Hs1 : s1 ∈ [s1, e1)).
335 { unfold elem_of, period_elem_of. by destruct e1. }
336 pose proof (proj1 (Hequiv s1) Hs1) as [[Heq|Heq]%limit_le_cases _].
337 { rewrite Heq in Hs12. by eapply (_ : Irreflexive limit_lt). }
338 by eapply asymmetry.
339Qed.
340
341(* TODO: make conclusion positive? *)
342Lemma period_nonempty_equiv_L_2 (s1 e1 s2 e2 : limit) :
343 period_nonempty [s1, e1) →
344 period_nonempty [s2, e2) →
345 [s1, e1) ≡ [s2, e2) →
346 ¬ e1 < e2.
347Proof.
348 intros Hne1 Hne2 Hequiv He12.
349 destruct e1 as [|e1|]; [by destruct s1|..|done].
350 destruct e2 as [|e2|]; first done.
351 * (* e2 - 1 ∈ [s2, e2) → e2 - 1 ∈ [s1, e1) → s1 ≤ e2 - 1 < e1 → e2 ≤ e1 → e2 = e1 ∨ e2 < e1 *)
352 assert (He2a : Z.pred e2 ∈ [s2, e2)).
353 { unfold elem_of, period_elem_of.
354 by destruct s2 as [|s2|]; [simpl in *; lia..|]. }
355 pose proof (proj2 (Hequiv (Z.pred e2)) He2a) as [_ He2b].
356 simpl in *. lia.
357 * (* We want to plug e1 into the right side to get a
358 contradiction, so we need s2 ≤ e1. It suffices to show that
359 s2 ≤ e1 - 1 *)
360 assert (He1a : Z.pred e1 ∈ [s1, e1)).
361 { unfold elem_of, period_elem_of.
362 by destruct s1 as [|s1|]; [simpl in *; lia..|]. }
363 pose proof (proj1 (Hequiv (Z.pred e1)) He1a) as [He1b _].
364 assert (He1c : e1 ∈ [s2, +∞)).
365 { unfold elem_of, period_elem_of.
366 by destruct s2 as [|s2|]; [|simpl in *; lia|]. }
367 pose proof (proj2 (Hequiv e1) He1c) as [_ []%(_ : Irreflexive limit_lt)].
368Qed.
369
370Lemma period_nonempty_equiv_L p1 p2 :
371 period_nonempty p1 →
372 period_nonempty p2 →
373 p1 ≡ p2 → p1 = p2.
374Proof.
375 destruct p1 as [s1 e1], p2 as [s2 e2].
376 unfold equiv, period_equiv.
377 intros Hne1 Hne2 Hequiv.
378 f_equal.
379 - destruct (decide (s1 < s2)) as [Hs12|[<-|Hs21]%not_limit_lt%limit_le_cases]; [|done|].
380 + exfalso. by apply (period_nonempty_equiv_L_1 s1 e1 s2 e2).
381 + exfalso. by apply (period_nonempty_equiv_L_1 s2 e2 s1 e1).
382 - destruct (decide (e1 < e2)) as [He12|[<-|He21]%not_limit_lt%limit_le_cases]; [|done|].
383 + exfalso. by apply (period_nonempty_equiv_L_2 s1 e1 s2 e2).
384 + exfalso. by apply (period_nonempty_equiv_L_2 s2 e2 s1 e1).
385Qed.
386
387Definition period_empty_not_nonempty p : ¬ period_empty p ↔ period_nonempty p.
388Proof. destruct p. apply not_limit_le. Qed.
389
390Lemma limit_lt_min l1 l2 l3 :
391 l1 < l2 ∧ l1 < l3 ↔ l1 < l2 `min` l3.
392Proof.
393 split.
394 - intros [Hl12 Hl13]. unfold limit_min. by case_decide.
395 - unfold limit_min. intros H. case_decide.
396 + split; first done.
397 apply limit_le_cases in H0 as [<-|H0]; first done.
398 by etrans.
399 + apply not_limit_le in H0.
400 by split; first etrans.
401Qed.
402
403Lemma limit_max_le l1 l2 l3 :
404 l1 ≤ l3 ∧ l2 ≤ l3 ↔ l1 `max` l2 ≤ l3.
405Proof.
406 split.
407 - intros [Hl12 Hl23]. unfold limit_max. by case_decide.
408 - unfold limit_max. intros H. case_decide.
409 + by split; first etrans.
410 + apply not_limit_le in H0. split; first done.
411 apply limit_le_lt in H0 as [H0 _]. by etrans.
412Qed.
413Lemma limit_le_max l1 l2 l3 :
414 l1 ≤ l2 `max` l3 ↔ l1 ≤ l2 ∨ l1 ≤ l3.
415Proof.
416 unfold limit_max.
417 destruct (decide (l2 ≤ l3)) as [Hl23|Hl23%not_limit_le].
418 - split; first tauto. intros [H|H]; last done. by etrans.
419 - split; first tauto. intros [H|H]; first done.
420 by trans l3; last (apply limit_le_cases; right).
421Qed.
422
423Lemma except_lem p1 p2 t :
424 t ∈ p1 ∧ t ∉ p2 ↔
425 t ∈ (except p1 p2).1 ∨ t ∈ (except p1 p2).2.
426Proof.
427 destruct p1 as [s1 e1], p2 as [s2 e2]. split.
428 - intros [Hp1 Hp2].
429 (* on the left if t < s2, on the right if e2 ≤ t *)
430 destruct (decide (t < s2)) as [Hts2|Hts2].
431 + (* t < s2 *)
432 left. simpl. split.
433 * apply Hp1.
434 * apply limit_lt_min. split; last done.
435 rewrite /elem_of /period_elem_of in Hp1. easy.
436 + (* ¬ (t < s2) (↔ s2 ≤ t) *)
437 apply not_limit_lt in Hts2.
438 right. simpl. split.
439 * apply limit_max_le. split.
440 -- apply Hp1.
441 -- apply not_limit_lt. intros contra. by apply Hp2.
442 * apply Hp1.
443 - intros [H|H]; simpl in *.
444 + split.
445 * unfold elem_of, period_elem_of in *. split.
446 -- apply H.
447 -- by destruct H as [_ [H _]%limit_lt_min].
448 * unfold elem_of, period_elem_of in *.
449 destruct H as [H1 [H2 H3]%limit_lt_min].
450 intros [Hc1 Hc2].
451 apply limit_le_cases in Hc1 as [Hc1|Hc1].
452 -- inv Hc1. by apply (_ : Irreflexive limit_lt) in H3.
453 -- eapply asymmetry; [apply H3 | apply Hc1].
454 + unfold elem_of, period_elem_of in H.
455 rewrite -limit_max_le in H. destruct H as [[H1 H2] H3].
456 split; first done.
457 intros [Hc1 Hc2].
458 apply limit_le_cases in H2 as [H2|H2].
459 -- inv H2. by apply (_ : Irreflexive limit_lt) in Hc2.
460 -- eapply asymmetry; [apply H2 | apply Hc2].
461Qed.
462
463Lemma limit_max_lt l1 l2 l3 :
464 l1 `max` l2 < l3 ↔ l1 < l3 ∧ l2 < l3.
465Proof.
466 unfold limit_max.
467 destruct (decide (l1 ≤ l2)) as [Hl12|Hl12%not_limit_le].
468 - split; last easy. intros H. by split; first eapply limit_lt_le_lt.
469 - split; last easy. intros H. by split; last etrans.
470Qed.
471
472Lemma limit_min_lt l1 l2 l3 :
473 l1 `min` l2 < l3 ↔ l1 < l3 ∨ l2 < l3.
474Proof.
475 unfold limit_min.
476 destruct (decide (l1 ≤ l2)%lim) as [Hl12|Hl12%not_limit_le].
477 - split; first tauto. by intros [H|H]; last eapply limit_lt_le_lt.
478 - split; first tauto. by intros [H|H]; first etrans.
479Qed.
480
481Lemma limit_lt_max l1 l2 l3 :
482 l1 < l2 `max` l3 ↔ l1 < l2 ∨ l1 < l3.
483Proof.
484 unfold limit_max.
485 destruct (decide (l2 ≤ l3)) as [Hl23|Hl23%not_limit_le].
486 - split; first tauto. intros [H|H]; last done.
487 by apply limit_le_cases in Hl23 as [<-|Hl23]; last etrans.
488 - split; first tauto. by intros [H|H]; last etrans.
489Qed.
490
491Instance limit_min_comm : Comm (=) limit_min.
492Proof.
493 unfold limit_min.
494 intros [] []; repeat case_decide;
495 try done; simpl in *; f_equal; lia.
496Qed.
497Instance limit_max_comm : Comm (=) limit_max.
498Proof.
499 unfold limit_max.
500 intros [] []; repeat case_decide;
501 try done; simpl in *; f_equal; lia.
502Qed.
503
504Lemma limit_max_eq_l l1 l2 : l1 `max` l2 = l1 ↔ l2 ≤ l1.
505Proof.
506 unfold limit_max. case_decide; split.
507 - by intros ->.
508 - intros H12. by eapply (_ : AntiSymm (=) limit_le).
509 - intros _. apply limit_le_cases. right.
510 by apply not_limit_le.
511 - by intros _.
512Qed.
513Lemma limit_max_eq_r l1 l2 : l1 `max` l2 = l2 ↔ l1 ≤ l2.
514Proof. rewrite [l1 `max` l2]comm. apply limit_max_eq_l. Qed.
515
516Lemma limit_max_l l1 l2 : l2 ≤ l1 → l1 `max` l2 = l1.
517Proof. apply limit_max_eq_l. Qed.
518Lemma limit_max_r l1 l2 : l1 ≤ l2 → l1 `max` l2 = l2.
519Proof. apply limit_max_eq_r. Qed.
520
521Definition ne_period := { p : period | period_nonempty p }.
522
523Instance ne_period_elem_of : ElemOf timestamp ne_period :=
524 λ t p, t ∈ `p.
525Instance ne_period_elem_of_dec t (p : ne_period) : Decision (t ∈ p).
526Proof. apply _. Qed.
527
528(* TODO: rename to ne_period_before *)
529Definition period_before '([s1, e1) ↾ _ : ne_period) '([s2, e2) ↾ _ : ne_period) :=
530 e1 < s2.
531
532Instance period_before_pi p1 p2 : ProofIrrel (period_before p1 p2).
533Proof. destruct p1 as [[s1 e1] Hne1], p2 as [[s2 e2] Hne2]. apply _. Qed.
534
535Instance period_before_trans : Transitive period_before.
536Proof.
537 intros [[s1 e1] Hne1] [[s2 e2] Hne2] [[s3 e3] Hne3] H1 H2.
538 unfold period_before in *. simpl in *.
539 by trans s2; last trans e2.
540Qed.
541
542Instance period_before_irrefl : Irreflexive period_before.
543Proof.
544 intros [[s e] Hne] Hp. simpl in *.
545 eapply (_ : Irreflexive limit_lt). by etrans.
546Qed.
547
548Instance period_before_strict_order : StrictOrder period_before.
549Proof. split; apply _. Qed.
550
551Definition ne_period_rel (R : relation ne_period) : relation period :=
552 λ p1 p2, ∃ H1 H2, R (p1 ↾ H1) (p2 ↾ H2).
553
554Instance ne_period_rel_trans `{!Transitive R} : Transitive (ne_period_rel R).
555Proof.
556 intros p1 p2 p3 (H1 & H2 & HR12) (H2' & H3 & HR23).
557 exists H1, H3. replace H2' with H2 in HR23; last apply proof_irrel.
558 by etrans.
559Qed.
560
561Instance ne_period_rel_irrefl `{!Irreflexive R} : Irreflexive (ne_period_rel R).
562Proof.
563 intros p. intros (H1 & H2 & HR).
564 replace H2 with H1 in HR; last apply proof_irrel.
565 by apply (_ : Irreflexive R) in HR.
566Qed.
567
568Instance ne_period_rel_pi (R : relation ne_period) `{!∀ x y, ProofIrrel (R x y)} x y :
569 ProofIrrel (ne_period_rel R x y).
570Proof. apply _. Qed.
571
572Lemma except_parts_order p1 p2 :
573 period_nonempty p2 →
574 period_nonempty (except p1 p2).1 →
575 period_nonempty (except p1 p2).2 →
576 ne_period_rel period_before (except p1 p2).1 (except p1 p2).2.
577Proof.
578 destruct p1 as [s1 e1], p2 as [s2 e2]. simpl. intros H0 Hne1 Hne2.
579 unfold period_before. split; [done|split; [done|]].
580 apply limit_min_lt. right. apply limit_lt_max. right. apply H0.
581Qed.
582
583Definition period_nonempty_alt (p : period) := ∃ t, t ∈ p.
584
585Lemma period_nonempty_alt_iff p :
586 period_nonempty p ↔ period_nonempty_alt p.
587Proof.
588 unfold period_nonempty, period_nonempty_alt.
589 destruct p as [s e]. split.
590 - intros Hlt. destruct s as [|s|]; last done.
591 + destruct e as [|e|]; first done.
592 * exists (Z.pred e). by split; last (simpl; lia).
593 * exists 0%Z. done.
594 + exists s. done.
595 - intros [t Ht]. by eapply limit_lt_le_lt.
596Qed.
597
598Instance period_eq_dec : EqDecision period.
599Proof. solve_decision. Qed.
600
601Instance period_disjoint : Disjoint period :=
602 λ p1 p2, period_empty (p1 ∩ p2).
603
604Instance period_intersection_comm : Comm (=) period_intersection.
605Proof.
606 intros [s1 e1] [s2 e2].
607 by rewrite /= [s2 `max` s1]comm [e2 `min` e1]comm.
608Qed.
609Instance period_disjoint_symm : Symmetric period_disjoint.
610Proof. intros p1 p2. unfold period_disjoint. by rewrite comm. Qed.
611
612Lemma limit_min_eq_l l1 l2 : l1 `min` l2 = l1 ↔ l1 ≤ l2.
613Proof.
614 unfold limit_min. case_decide; first done. split.
615 - intros ->. exfalso. by apply H.
616 - intros []%H.
617Qed.
618Lemma limit_min_eq_r l1 l2 : l1 `min` l2 = l2 ↔ l2 ≤ l1.
619Proof. rewrite [l1 `min` l2]comm. apply limit_min_eq_l. Qed.
620
621Lemma limit_min_l l1 l2 : l1 ≤ l2 → l1 `min` l2 = l1.
622Proof. apply limit_min_eq_l. Qed.
623Lemma limit_min_r l1 l2 : l2 ≤ l1 → l1 `min` l2 = l2.
624Proof. apply limit_min_eq_r. Qed.
625
626Lemma limit_lt_le_trans {l1} l2 {l3} : l1 < l2 → l2 ≤ l3 → l1 < l3.
627Proof. by intros Hlt12 [->|Hlt23]%limit_le_cases; last etrans. Qed.
628
629Instance period_union : Union period :=
630 λ '[s1, e1) '[s2, e2), [s1 `min` s2, e1 `max` e2).
631
632Lemma limit_min_le l1 l2 l3 :
633 l1 ≤ l3 ∨ l2 ≤ l3 ↔
634 l1 `min` l2 ≤ l3.
635Proof.
636 unfold limit_min. case_decide; split.
637 - by intros [H13|H23]; last trans l2.
638 - intros H13. by left.
639 - apply not_limit_le in H. intros [H13|H23]; last done.
640 trans l1; last done.
641 apply limit_le_cases. by right.
642 - intros H23. by right.
643Qed.
644
645Lemma limit_le_min l1 l2 l3 :
646 l1 ≤ l2 ∧ l1 ≤ l3 ↔
647 l1 ≤ l2 `min` l3.
648Proof.
649 unfold limit_min. case_decide; split.
650 - by intros [H12 _].
651 - intros ?. by split; last trans l2.
652 - by intros [_ H13].
653 - intros ?. split; last done.
654 apply not_limit_le in H.
655 trans l3; first done.
656 apply limit_le_cases. by right.
657Qed.
658
659Lemma period_union_lem_1 t (p1 p2 : period) :
660 t ∈ p1 ∨ t ∈ p2 → t ∈ p1 ∪ p2.
661Proof.
662 destruct p1 as [s1 e1], p2 as [s2 e2].
663 unfold union, period_union.
664 intros [Ht|Ht]; split.
665 - apply limit_min_le. left. apply Ht.
666 - apply limit_lt_max. left. apply Ht.
667 - apply limit_min_le. right. apply Ht.
668 - apply limit_lt_max. right. apply Ht.
669Qed.
670
671Definition unifiable '[s1, e1) '[s2, e2) :=
672 s2 ≤ e1 ∧ s1 ≤ e2.
673
674Instance unifiable_dec : RelDecision unifiable.
675Proof. intros [] []. solve_decision. Qed.
676
677Lemma not_limit_le_lt l1 l2 l3 :
678 ¬ l1 ≤ l2 < l3 ↔ l2 < l1 ∨ l3 ≤ l2.
679Proof.
680 split.
681 - intros H123.
682 destruct (decide (l2 < l1)) as [?|H21%not_limit_lt]; first by left.
683 destruct (decide (l3 ≤ l2)) as [?|H32%not_limit_le]; first by right.
684 exfalso. by apply H123.
685 - intros [H21|H32] contra.
686 + eapply not_limit_le; [apply H21|apply contra].
687 + eapply not_limit_lt; [apply H32|apply contra].
688Qed.
689
690Lemma limit_lt_le l1 l2 : l1 < l2 → l1 ≤ l2.
691Proof. intros Hlt. apply limit_le_cases. by right. Qed.
692
693Lemma period_union_lem_2 t (p1 p2 : period) :
694 unifiable p1 p2 →
695 t ∈ p1 ∪ p2 → t ∈ p1 ∨ t ∈ p2.
696Proof.
697 intros Hunif Hunion.
698 destruct (decide (t ∈ p1)) as [?|Ht1]; first by left.
699 destruct (decide (t ∈ p2)) as [?|Ht2]; first by right.
700 exfalso.
701
702 destruct p1 as [s1 e1], p2 as [s2 e2].
703 unfold elem_of, period_elem_of in *.
704 simpl in *. destruct Hunif as [Hunif1 Hunif2].
705
706 (* If t is not in p1, then it must be in p2 *)
707 apply Ht2. clear Ht2.
708 apply not_limit_le_lt in Ht1.
709 destruct Ht1 as [Ht1|Ht1].
710 - (* t is not in p1 because it is before p1 (where p2 must hence be) *)
711 destruct Hunion as [Hunion1 Hunion2].
712 apply limit_min_le in Hunion1 as [[->|contra]%limit_le_cases | Hunion1].
713 { exfalso. by eapply (_ : Irreflexive limit_lt). }
714 { exfalso. by eapply (asymmetry (R:=limit_lt)). }
715 split; first done. by eapply limit_lt_le_trans.
716 - destruct Hunion as [Hunion1 Hunion2].
717 apply limit_lt_max in Hunion2 as [Hunion2 | Hunion2].
718 + apply limit_le_cases in Ht1 as [->|contra].
719 { exfalso. by eapply (_ : Irreflexive limit_lt). }
720 { exfalso. by eapply (asymmetry (R:=limit_lt)). }
721 + split; last done. by trans e1.
722Qed.
723
724Instance period_union_comm : Comm (=) period_union.
725Proof.
726 unfold period_union. intros [s1 e1] [s2 e2].
727 by rewrite limit_min_comm limit_max_comm.
728Qed.
729
730Instance period_singleton : Singleton timestamp period :=
731 λ t, [t, TsLimit (Z.succ t)).
732Lemma period_singleton_lem_1 t : t ∈ ({[t]} : period).
733Proof. by split; simpl; last lia. Qed.
734Lemma period_singleton_lem_2 t t' : t' ∈ ({[t]} : period) → t' = t.
735Proof.
736 unfold singleton, period_singleton.
737 intros [H11 H12]. destruct t, t'; try done; simpl in *; lia.
738Qed.
739Lemma period_singleton_nonempty t : period_nonempty {[t]}.
740Proof.
741 apply period_nonempty_alt_iff.
742 exists t. apply period_singleton_lem_1.
743Qed.
744
745Lemma unifiable_period_union p1 p2 p3 :
746 unifiable p1 p2 → unifiable p2 p3 →
747 unifiable (p1 ∪ p2) p3.
748Proof.
749 destruct p1 as [s1 e1], p2 as [s2 e2], p3 as [s3 e3].
750 intros [Hunif11 Hunif12] [Hunif21 Hunif22]. simpl. split.
751 + apply limit_le_max. by right.
752 + apply limit_min_le. by right.
753Qed.
754
755Instance unifiable_symm : Symmetric unifiable.
756Proof. by intros [] [] []. Qed.
757
758Definition Σlift {A} {Φ : A → Prop} (R : relation A) : relation {x : A | Φ x} :=
759 λ '(x↾_) '(y↾_), R x y.
760
761Instance Σlift_symm {A Φ} `{!Symmetric R} : Symmetric (@Σlift A Φ R).
762Proof. intros [x Hx] [y Hy] HR. simpl in *. by apply symmetry. Qed.
763
764(* TODO: probably unused? *)
765Instance Σlift_dec {A Φ} `{!RelDecision R} : RelDecision (@Σlift A Φ R).
766Proof. intros [x Hx] [y Hy]. by simpl. Qed.
767
768Definition ne_period_unifiable : relation ne_period := Σlift unifiable.
769
770Lemma period_unifiable_not_before p1 p2 : ne_period_unifiable p1 p2 → ¬ period_before p1 p2.
771Proof.
772 destruct p1 as [[s1 e1] Hne1], p2 as [[s2 e2] Hne2]. simpl in *.
773 intros [Hunif1 Hunif2] Hbefore.
774 apply limit_le_cases in Hunif1 as [->|contra].
775 - by eapply (_ : Irreflexive limit_lt).
776 - by eapply (asymmetry (R:=limit_lt)).
777Qed.
778
779(* TODO: define total relation on Σperiod_nonempty, p1 p2 := unifiable p1 p2 ∨ p1 < p2.
780 (Then have [AntiSymm unifiable (≤@{Σperiod_nonempty})].)
781 Show decidability, perform mergesort.
782 Then make the rest of normalization consist in unification of the periods.
783 *)
784
785Definition ne_period_le p1 p2 := ne_period_unifiable p1 p2 ∨ period_before p1 p2.
786
787Instance ne_period_le_antisymm : AntiSymm ne_period_unifiable ne_period_le.
788Proof.
789 intros p1 p2 [H12|H12] [H21|H21]; [done|done|..].
790 - exfalso. apply symmetry in H21.
791 by eapply period_unifiable_not_before.
792 - exfalso. by eapply asymmetry.
793Qed.
794
795Lemma ne_period_neither_before_unifiable p1 p2 :
796 ¬ period_before p1 p2 → ¬ period_before p2 p1 →
797 ne_period_unifiable p1 p2.
798Proof.
799 destruct p1 as [[s1 e1] Hne1], p2 as [[s2 e2] Hne2].
800 simpl in *. by intros ?%not_limit_lt ?%not_limit_lt.
801Qed.
802
803Instance period_before_dec : RelDecision period_before.
804Proof.
805 intros [[s1 e1] ?] [[s2 e2] ?]. simpl in *.
806 solve_decision.
807Qed.
808
809Lemma ne_period_not_unifiable p1 p2 :
810 ¬ ne_period_unifiable p1 p2 →
811 period_before p1 p2 ∨ period_before p2 p1.
812Proof.
813 intros Hnunif.
814 destruct (decide (period_before p1 p2)) as [?|H12]; first by left.
815 destruct (decide (period_before p2 p1)) as [?|H21]; first by right.
816 exfalso. by apply Hnunif, ne_period_neither_before_unifiable.
817Qed.
818
819Instance ne_period_le_total : Total ne_period_le.
820Proof.
821 intros p1 p2.
822 destruct (decide (ne_period_unifiable p1 p2)) as [Hunif|Hnunif].
823 - (* which one we pick does not matter *)
824 by do 2 left.
825 - apply ne_period_not_unifiable in Hnunif as [H12|H21].
826 + left. by right.
827 + right. by right.
828Qed.
diff --git a/server/formal/period_seq.v b/server/formal/period_seq.v
new file mode 100644
index 0000000..705e505
--- /dev/null
+++ b/server/formal/period_seq.v
@@ -0,0 +1,834 @@
1From stdpp Require Import numbers option sorting ssreflect.
2From stdpp Require Import options.
3From routemon Require Import period util.
4
5(* This setup would require the proof irrelevance stuff
6
7Record period_seq :=
8 PeriodSeq
9 { periods : list period
10 ; Hnonempty : Forall period_nonempty periods
11 ; Hsorted : Sorted period_before periods
12 }.
13*)
14
15Definition period_seq := list ne_period.
16
17Definition period_seq_nf (ps : period_seq) :=
18 Sorted period_before ps.
19
20Instance period_seq_elem_of : ElemOf timestamp period_seq :=
21 λ t, Exists (λ p, t ∈ p).
22Instance period_seq_elem_of_dec t (ps : period_seq) : Decision (t ∈ ps).
23Proof.
24 induction ps as [|p ps].
25 - right. inv 1.
26 - destruct IHps.
27 + left. by apply Exists_cons_tl.
28 + destruct (decide (t ∈ p)).
29 * left. by apply Exists_cons_hd.
30 * right. by inv 1.
31Qed.
32
33Instance period_seq_equiv : Equiv period_seq :=
34 λ ps1 ps2, ∀ t, t ∈ ps1 ↔ t ∈ ps2.
35
36Definition ne_period_intersection (p1 p2 : ne_period) :=
37 let p := `p1 ∩ `p2 in
38 match decide (period_nonempty p) with
39 | left H => Some (p ↾ H)
40 | right _ => None
41 end.
42
43Definition ne_period_start (p : ne_period) :=
44 period_start (`p).
45Definition ne_period_end (p : ne_period) :=
46 period_end (`p).
47
48Definition period_seq_intersection_1 go ps1 ps2 :=
49 match ps1, ps2 with
50 | p1 :: ps1', p2 :: ps2' =>
51 let mp12 := ne_period_intersection p1 p2 in
52 let rest := if decide (ne_period_end p1 < ne_period_end p2)%lim then go ps1' ps2 else go ps1 ps2' in
53 match mp12 with
54 | Some p12 => p12 :: rest
55 | None => rest
56 end
57 | _, _ => []
58 end.
59Fixpoint period_seq_intersection_aux n :=
60 match n with
61 | 0 => const (const [])
62 | S n => period_seq_intersection_1 (period_seq_intersection_aux n)
63 end.
64Instance period_seq_intersection : Intersection period_seq :=
65 λ ps1 ps2, period_seq_intersection_aux (S (length ps1 + length ps2)) ps1 ps2.
66
67Lemma period_seq_intersection_eq ps1 ps2 :
68 period_seq_intersection ps1 ps2 =
69 match ps1, ps2 with
70 | p1 :: ps1', p2 :: ps2' =>
71 let mp12 := ne_period_intersection p1 p2 in
72 let rest := if decide (ne_period_end p1 < ne_period_end p2)%lim
73 then period_seq_intersection ps1' ps2
74 else period_seq_intersection ps1 ps2' in
75 match mp12 with
76 | Some p12 => p12 :: rest
77 | None => rest
78 end
79 | _, _ => []
80 end.
81Proof.
82 destruct ps1 as [|p1 ps1], ps2 as [|p2 ps2]; [done..|].
83 have Hlen1 : S (S (length ps1 + length ps2)) = S (length (p1 :: ps1) + length ps2) by simpl; lia.
84 have Hlen2 : S (S (length ps1 + length ps2)) = S (length ps1 + length (p2 :: ps2)) by simpl; lia.
85 by rewrite
86 /period_seq_intersection /period_seq_intersection_aux
87 !length_cons Nat.add_succ_l Nat.add_succ_r -/period_seq_intersection_aux.
88Qed.
89
90Opaque period_seq_intersection.
91
92Lemma period_seq_nf_cons p ps :
93 period_seq_nf (p :: ps) ↔
94 period_seq_nf ps ∧
95 Forall (λ q, ne_period_end p < ne_period_start q)%lim ps.
96Proof.
97 split.
98 - intros HSort%Sorted_StronglySorted; last apply _.
99 inv HSort. repeat split; try done.
100 + by apply StronglySorted_Sorted.
101 + eapply Forall_impl; first done.
102 intros [[sq eq] Hq] Hbef.
103 by destruct p as [[sp ep] Hp].
104 - intros (Hnf & Hlt).
105 constructor; first done. destruct ps as [|q ps]; constructor.
106 inv Hlt. destruct p as [[sp ep] Hp], q as [[sq eq] Hq]. by simpl in *.
107Qed.
108
109(*
110Lemma list_elem_of_cons_inv `{!EqDecision A} (x y : A) (l : list A) :
111 x ∈ y :: l ↔ x = y ∨ x ≠ y ∧ x ∈ l.
112Proof.
113 split.
114 - destruct (decide (x = y)) as [<-|H].
115 + intros _. by left.
116 + inv 1. by right.
117 - by intros [<-|[_ H]]; constructor.
118Qed.
119*)
120
121Lemma list_elem_of_cons_inv {A} (x y : A) (l : list A) :
122 x ∈ y :: l ↔ x = y ∨ x ∈ l.
123Proof.
124 split.
125 - by inv 1; [left|right].
126 - by intros [<-|H]; constructor.
127Qed.
128
129Lemma Sorted_list_elem_of_R_trans {A} `{!Transitive R} (x y z : A) (l : list A) :
130 Sorted R (y :: l) → z ∈ y :: l → R x y → R x z.
131Proof.
132 intros [HSort Hyl]%Sorted_inv.
133 revert y Hyl.
134 induction HSort as [|y' l' HSort IH Hy'l']; intros y.
135 - intros _. by inv 1; last inv H2.
136 - intros Hyy'%HdRel_inv.
137 intros [->|Hz]%list_elem_of_cons_inv; first done.
138 intros Hxy.
139 have : R x y' by eapply (_ : Transitive R).
140 by apply IH.
141Qed.
142
143Lemma Sorted_list_elem_of_cons_inv {A} `{!Transitive R} (x y : A) (l : list A) :
144 Sorted R (y :: l) →
145 x ∈ y :: l → x = y ∧ Forall (R x) l ∨ R y x ∧ x ∈ l.
146Proof.
147 intros HSort [->|H%list_elem_of_In]%list_elem_of_In%in_inv.
148 - left. by apply Sorted_StronglySorted in HSort as [_ ?]%StronglySorted_inv.
149 - right. inv HSort. inv H3; first inv H.
150 by split; first eapply Sorted_list_elem_of_R_trans.
151Qed.
152
153Lemma period_seq_nf_elem_of_cons_inv (p1 p2 : ne_period) (ps : period_seq) :
154 period_seq_nf (p2 :: ps) →
155 p1 ∈ p2 :: ps → p1 = p2 ∧ Forall (period_before p1) ps ∨
156 period_before p2 p1 ∧ p1 ∈ ps.
157Proof. apply Sorted_list_elem_of_cons_inv. Qed.
158
159Inductive option_Exists {A} (Φ : A → Prop) : option A → Prop :=
160 | Exists_Some (x : A) : Φ x → option_Exists Φ (Some x).
161
162Lemma option_Exists_from_option {A} Φ (mx : option A) :
163 option_Exists Φ mx ↔ from_option Φ False mx.
164Proof. split; by [inv 1 | destruct mx]. Qed.
165
166Lemma period_seq_intersect_lem_aux (p1 p2 : ne_period) (ps1 ps2 : period_seq) :
167 is_Some (ne_period_intersection p1 p2) →
168 period_seq_nf ps1 → period_seq_nf ps2 →
169 p1 ∈ ps1 → p2 ∈ ps2 →
170 option_Exists (.∈ ps1 ∩ ps2) (ne_period_intersection p1 p2).
171Proof.
172 intros Hne. revert ps2.
173 induction ps1 as [|[s1 e1] ps1]; first inv 3.
174 intros ps2 Hnf1 Hnf2 H1 H2. revert ps2 Hnf2 H2.
175 induction ps2 as [|[s2 e2] ps2]; first inv 2.
176 intros Hnf2 H2.
177
178 apply option_Exists_from_option.
179 rewrite /intersection period_seq_intersection_eq /=.
180 apply period_seq_nf_elem_of_cons_inv in H1 as [[-> Hp1]|[Hlt1 H1]]; last done.
181 + apply period_seq_nf_elem_of_cons_inv in H2 as [[-> Hp2]|[Hlt2 H2]]; last done.
182 * unfold ne_period_intersection.
183 case_decide.
184 -- exfalso. simpl in Hne.
185 apply limit_le_cases in H as [contra|contra].
186 ++ rewrite contra in Hne. by eapply (_ : Irreflexive limit_lt).
187 ++ by apply asymmetry in Hne.
188 -- constructor.
189 * case_decide.
190 -- case_decide.
191 ++ (* we need to show that [s1, e1) ## p2 *)
192 exfalso. assert ([s1, e1) ## p2).
193 { unfold disjoint, period_disjoint, period_empty.
194 destruct p2 as [s3 e3]. simpl.
195 destruct Hlt2 as [Hne2 [Hne3 Hlt2]].
196 simpl in Hlt2.
197
198 trans (e1 `min` e2)%lim.
199 { apply limit_le_cases. left.
200 trans e1.
201 - apply limit_min_eq_l, limit_le_cases. right.
202 by trans e2; last trans s3.
203 - apply symmetry, limit_min_eq_l, limit_le_cases. by right. }
204 etrans; first done.
205 apply limit_max_le.
206 split.
207 - apply limit_le_max. by left.
208 - apply limit_le_max. right.
209 apply limit_le_cases. right. by trans e2. }
210 by eapply period_empty_not_nonempty.
211 ++ by apply IHps2; first apply period_seq_nf_cons in Hnf2 as [_ [? _]].
212 -- case_decide.
213 ++ apply not_limit_le in H.
214 (* [s1, e1) ## p2 since e1 < e2 and e2 < p2, but [s1, e1) ∩ p2 ≠ ∅ in hyp *)
215 exfalso. assert ([s1, e1) ## p2).
216 { unfold disjoint, period_disjoint, period_empty.
217 destruct p2 as [s3 e3]. simpl.
218 destruct Hlt2 as [Hne2 [Hne3 Hlt2]].
219 simpl in Hlt2.
220
221 rewrite limit_min_l; last first.
222 { apply limit_le_cases. right.
223 by trans e2; last trans s3. }
224 apply limit_le_max. right.
225 apply limit_le_cases. right.
226 by trans e2. }
227 by eapply period_empty_not_nonempty.
228 ++ constructor. by apply IHps2; first apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
229 + apply period_seq_nf_elem_of_cons_inv in H2 as [[-> Hp2]|[Hlt2 H2]]; last done.
230 * case_decide.
231 -- case_decide.
232 ++ apply IHps1; try done.
233 ** by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
234 ** by constructor.
235 ++ apply not_limit_lt in H0. exfalso. assert (p1 ## [s2, e2)).
236 { unfold disjoint, period_disjoint, period_empty.
237 destruct p1 as [s3 e3]. simpl.
238 destruct Hlt1 as [Hne1 [Hne3 Hlt1]].
239 simpl in Hlt1.
240
241 trans (e1 `min` e2)%lim.
242 { apply limit_le_cases. left.
243 trans e2.
244 - apply limit_min_eq_r. trans e1; first done.
245 apply limit_le_cases. right. by trans s3.
246 - by apply symmetry, limit_min_eq_r. }
247 etrans; first done.
248 apply limit_max_le.
249 split.
250 - apply limit_le_max. left.
251 apply limit_le_cases. right. by trans e1.
252 - apply limit_le_max. by right. }
253 by eapply period_empty_not_nonempty.
254 -- case_decide.
255 ++ constructor. apply IHps1; try done.
256 ** by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
257 ** by constructor.
258 ++ apply not_limit_lt in H0. apply not_limit_le in H.
259 exfalso. assert (p1 ## [s2, e2)).
260 { unfold disjoint, period_disjoint, period_empty.
261 destruct p1 as [s3 e3]. simpl.
262 destruct Hlt1 as [Hne1 [Hne3 Hlt1]].
263 simpl in Hlt1.
264
265 rewrite limit_min_r; last first.
266 { trans e1; first done.
267 apply limit_le_cases. right.
268 by trans s3. }
269 trans e1; first done.
270 apply limit_le_max. left.
271 apply limit_le_cases. by right. }
272 by eapply period_empty_not_nonempty.
273 * case_decide.
274 -- case_decide.
275 ++ apply IHps1; try done.
276 ** by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
277 ** by constructor.
278 ++ by apply IHps2; first apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
279 -- case_decide; constructor.
280 ++ apply IHps1; try done.
281 ** by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
282 ** by constructor.
283 ++ by apply IHps2; first apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
284Qed.
285
286Lemma period_seq_intersection_inv (p : period) (ps1 ps2 : period_seq) :
287 period_seq_nf ps1 → period_seq_nf ps2 → p ∈ ps1 ∩ ps2 →
288 ∃ p1 p2, p1 ∈ ps1 ∧ p2 ∈ ps2 ∧ p = p1 ∩ p2.
289Proof.
290 intros Hnf1. revert ps2.
291 induction ps1; first inv 2.
292 induction ps2.
293 { intros _ contra.
294 rewrite period_seq_intersection_eq in contra.
295 destruct a. inv contra. }
296 destruct a as [s1 e1], a0 as [s2 e2].
297 intros Hnf2 Hint.
298 rewrite period_seq_intersection_eq in Hint.
299 simpl in Hint. case_decide; case_decide.
300 - apply IHps1 in Hint as (q1 & q2 & Hq1 & Hq2 & ->); last done.
301 + exists q1, q2. by repeat split; first constructor.
302 + by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
303 - apply IHps2 in Hint as (q1 & q2 & Hq1 & Hq2 & ->).
304 + exists q1, q2. by repeat split; last constructor.
305 + by apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
306 - inv Hint.
307 + exists [s1, e1), [s2, e2). repeat split; constructor.
308 + apply IHps1 in H3 as (q1 & q2 & Hq1 & Hq2 & ->); last done.
309 * exists q1, q2. by repeat split; first constructor.
310 * by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
311 - inv Hint.
312 + exists [s1, e1), [s2, e2). repeat split; constructor.
313 + apply IHps2 in H3 as (q1 & q2 & Hq1 & Hq2 & ->).
314 * exists q1, q2. by repeat split; last constructor.
315 * by apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
316Qed.
317
318Lemma period_seq_intersection_lem t (ps1 ps2 : period_seq) :
319 period_seq_nf ps1 → period_seq_nf ps2 →
320 t ∈ ps1 ∧ t ∈ ps2 ↔ t ∈ ps1 ∩ ps2.
321Proof.
322 intros Hnf1 Hnf2.
323 split.
324 - intros [H1 H2].
325 unfold elem_of, period_seq_elem_of in H1, H2.
326 apply Exists_exists in H1 as (p1 & Hp1 & Ht1).
327 apply Exists_exists in H2 as (p2 & Hp2 & Ht2).
328 assert (Ht : t ∈ p1 ∩ p2). { by apply intersect_and. }
329 clear Ht1 Ht2.
330 unfold elem_of, period_seq_elem_of.
331 apply Exists_exists. exists (p1 ∩ p2).
332 split; first apply period_seq_intersect_lem_aux; try done.
333 apply period_nonempty_alt_iff. by exists t.
334 - intros (p & Hp & Ht)%Exists_exists.
335 apply period_seq_intersection_inv in Hp as (p1 & p2 & Hp1 & Hp2 & ->); try done.
336 apply intersect_and in Ht as [Ht1 Ht2].
337 split; apply Exists_exists; by eexists.
338Qed.
339
340Definition period_seq_extent (ps : period_seq) : period :=
341 match head ps, last ps with
342 | Some [s, _), Some [_, e) => [s, e)
343 | _, _ => ∅
344 end.
345
346(*
347Lemma period_seq_extent_hd ps :
348 period_seq_nf ps →
349 Forall (period_start (period_seq_extent ps)
350
351Lemma period_seq_extent_spec t ps :
352 period_seq_nf ps → t ∈ ps →
353 t ∈ period_seq_extent ps.
354Proof.
355 Search StronglySorted.
356 induction ps as [|p ps]; first inv 2.
357 intros Hnf. inv 1.
358 -
359
360Qed.
361*)
362
363(*
364Definition period_seq_intersection_extent (ps1 ps2 : period_seq) :
365 period_seq_nf ps1 → period_seq_nf ps2 →
366 period_seq_extent (ps1 ∩ ps2) = period_seq_extent ps1 ∩ period_seq_extent ps2.
367Proof.
368 intros Hnf1 Hnf2.
369 destruct (decide (period_empty (period_seq_extent (ps1 ∩ ps2)))).
370 - admit.
371 - apply period_empty_not_nonempty in n.
372 apply period_nonempty_equiv_L; first done.
373 + admit.
374 + intros t.
375 Search period equiv eq.
376*)
377
378(* The intersection preserves normal forms *)
379Lemma period_seq_intersection_nf (ps1 ps2 : period_seq) :
380 period_seq_nf ps1 → period_seq_nf ps2 → period_seq_nf (ps1 ∩ ps2).
381Proof.
382 intros Hnf1. revert ps2.
383 induction ps1 as [|[s1 e1] ps1]; induction ps2 as [|[s2 e2] ps2]; [done..|].
384 intros Hnf2. rewrite period_seq_intersection_eq /=.
385 case_decide.
386 - case_decide.
387 + by apply IHps1; first apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
388 + apply IHps2. by apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
389 - case_decide.
390 + apply IHps1 in Hnf2 as Hnf2'; last by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
391 destruct Hnf2' as [Hne HSort]. split.
392 * by constructor; first apply period_empty_not_nonempty.
393 * constructor; first done.
394 rewrite {1}/intersection /period_intersection.
395 apply period_seq_nf_cons in Hnf1 as (Hne1 & Hnf1 & Hlt1).
396 destruct (ps1 ∩ ([s2, e2) :: ps2)) as [|[sq eq] qs] eqn:Hqs; constructor.
397 assert (Hq : [sq, eq) ∈ ps1 ∩ ([s2, e2) :: ps2)).
398 { rewrite Hqs. constructor. }
399 unfold period_before. repeat split.
400 -- by apply period_empty_not_nonempty.
401 -- by eapply Forall_forall; first apply Hne.
402 -- specialize (IHps1 Hnf1).
403 apply period_seq_intersection_inv in Hq as ([sq1 eq1] & [sq2 eq2] & Hq1%list_elem_of_In & Hq2 & Hq); [|done..].
404 apply (proj1 (List.Forall_forall _ _) Hlt1) in Hq1.
405 injection Hq as -> ->.
406 simplify_eq/=.
407 apply limit_min_lt. left.
408 apply limit_lt_max. by left.
409 + apply IHps1 in Hnf2 as Hnf2'; last by apply period_seq_nf_cons in Hnf1 as (_ & ? & _).
410 destruct Hnf2' as [Hne HSort].
411 apply not_limit_lt in H0. split.
412 * constructor.
413 -- by apply period_empty_not_nonempty.
414 -- apply IHps2. by apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
415 * constructor.
416 -- apply IHps2. by apply period_seq_nf_cons in Hnf2 as (_ & ? & _).
417 -- rewrite {1}/intersection /period_intersection.
418 apply period_seq_nf_cons in Hnf1 as Hnf1'.
419 destruct Hnf1' as (Hp1 & Hnf1' & Hne1).
420 apply period_seq_nf_cons in Hnf2 as (Hne2 & Hnf2 & Hlt2).
421 apply IHps2 in Hnf2 as Hnf2'.
422 destruct (([s1, e1) :: ps1) ∩ ps2) as [|[sq eq] qs] eqn:Hqs; constructor.
423 assert (Hq : [sq, eq) ∈ ([s1, e1) :: ps1) ∩ ps2).
424 { rewrite Hqs. constructor. }
425 unfold period_before. repeat split.
426 ++ by apply period_empty_not_nonempty.
427 ++ by eapply Forall_forall; first apply Hnf2'.
428 ++ apply period_seq_intersection_inv in Hq as ([sq1 eq1] & [sq2 eq2] & Hq1 & Hq2%list_elem_of_In & Hq); [|done..].
429 apply (proj1 (List.Forall_forall _ _) Hlt2) in Hq2.
430 injection Hq as -> ->.
431 simplify_eq/=.
432 apply limit_min_lt. right.
433 apply limit_lt_max. by right.
434Qed.
435
436Definition period_seq_intersection_comm_equiv ps1 ps2 :
437 period_seq_nf ps1 → period_seq_nf ps2 →
438 ps1 ∩ ps2 ≡ ps2 ∩ ps1.
439Proof.
440 intros Hnf1 Hnf2 t.
441 split; by intros [H2 H1]%period_seq_intersection_lem;
442 first apply period_seq_intersection_lem.
443Qed.
444
445Lemma period_seq_nf_cons_equiv_inv_start_1 p1 ps1 p2 ps2:
446 period_seq_nf (p1 :: ps1) →
447 period_seq_nf (p2 :: ps2) →
448 p1 :: ps1 ≡ p2 :: ps2 →
449 ¬ (period_start p1 < period_start p2)%lim.
450Proof.
451 intros Hnf1 Hnf2 Hequiv Hp12.
452 apply period_seq_nf_cons in Hnf1 as (Hne1 & Hnf1 & Hlt1), Hnf2 as (Hne2 & Hnf2 & Hlt2).
453 destruct p1 as [s1 e1], p2 as [s2 e2]. simpl in Hp12.
454 destruct s2 as [|s2|]; [by destruct s1| |done].
455 destruct s1 as [|s1|]; last done.
456 - destruct e1 as [|e1|]; first done.
457 + assert (Z.pred (s2 `min` e1) ∈ [-∞, e1) :: ps1).
458 { constructor. by split; [|simpl; lia]. }
459 apply Hequiv in H. inv H.
460 * destruct H1 as [H1 _]. simpl in H1. lia.
461 * apply Exists_exists in H1 as ([sp ep] & Hp & Hs2).
462 rewrite Forall_forall in Hlt2.
463 apply Hlt2 in Hp. simpl in Hp.
464 destruct Hs2 as [Hs21 Hs22].
465 assert (contra : (s2 < s2)%lim).
466 { trans e2; first done.
467 apply (limit_lt_le_trans sp); first done.
468 etrans; first apply Hs21. simpl. lia. }
469 by eapply (_ : Irreflexive limit_lt).
470 + assert (Z.pred s2 ∈ [-∞, +∞) :: ps1).
471 { by constructor. }
472 apply Hequiv in H. inv H.
473 * destruct H1 as [H1 _]. simpl in H1. lia.
474 * apply Exists_exists in H1 as ([sp ep] & Hp & Hs2).
475 rewrite Forall_forall in Hlt2.
476 apply Hlt2 in Hp. simpl in Hp.
477 destruct Hs2 as [Hs21 Hs22].
478 assert (contra : (s2 < s2)%lim).
479 { trans e2; first done.
480 apply (limit_lt_le_trans sp); first done.
481 etrans; first apply Hs21. simpl. lia. }
482 by eapply (_ : Irreflexive limit_lt).
483 - assert (s1 ∈ [s1, e1) :: ps1).
484 { by constructor. }
485 apply Hequiv in H. inv H.
486 + destruct H1 as [[[= ->]|H1]%limit_le_cases _].
487 * by eapply (_ : Irreflexive limit_lt).
488 * by eapply (asymmetry (R:=limit_lt)).
489 + apply Exists_exists in H1 as ([sp ep] & Hp & Hs1).
490 rewrite Forall_forall in Hlt2.
491 apply Hlt2 in Hp. simpl in Hp.
492 assert (contra : (s1 < s1)%lim).
493 { trans s2; first done.
494 trans e2; first done.
495 by apply (limit_lt_le_trans sp); last apply Hs1. }
496 by eapply (_ : Irreflexive limit_lt).
497Qed.
498
499Instance period_seq_equiv_trans : Transitive (≡@{period_seq}).
500Proof.
501 intros ps1 ps2 ps3 Heq12 Heq23 t. split.
502 - by intros Ht%Heq12%Heq23.
503 - by intros Ht%Heq23%Heq12.
504Qed.
505
506Instance period_seq_equiv_symm : Symmetric (≡@{period_seq}).
507Proof. intros ps1 ps2 Heq12 t. split; by intros Ht%Heq12. Qed.
508
509Lemma period_seq_nf_cons_equiv_inv_start p1 ps1 p2 ps2:
510 period_seq_nf (p1 :: ps1) →
511 period_seq_nf (p2 :: ps2) →
512 p1 :: ps1 ≡ p2 :: ps2 →
513 period_start p1 = period_start p2.
514Proof.
515 intros Hnf1 Hnf2 Hequiv.
516 destruct (decide (period_start p1 < period_start p2)%lim) as [Hs12|Hs21].
517 - exfalso. by eapply period_seq_nf_cons_equiv_inv_start_1 in Hs12.
518 - apply not_limit_lt, limit_le_cases in Hs21 as [Hs21|Hs21]; first done.
519 exfalso. by eapply period_seq_nf_cons_equiv_inv_start_1 in Hs21.
520Qed.
521
522Lemma period_seq_nf_cons_equiv_inv_end_1 p1 ps1 p2 ps2:
523 period_seq_nf (p1 :: ps1) →
524 period_seq_nf (p2 :: ps2) →
525 p1 :: ps1 ≡ p2 :: ps2 →
526 ¬ (period_end p1 < period_end p2)%lim.
527Proof.
528 intros Hnf1 Hnf2 Hequiv Hp12.
529 assert (Hs : period_start p1 = period_start p2).
530 { by eapply period_seq_nf_cons_equiv_inv_start. }
531 apply period_seq_nf_cons in Hnf1 as (Hne1 & Hnf1 & Hlt1), Hnf2 as (Hne2 & Hnf2 & Hlt2).
532 destruct p1 as [s1 e1], p2 as [s2 e2]. simpl in Hs, Hp12.
533 rewrite <-Hs in *. rename s1 into s. clear Hs s2.
534 destruct e1 as [|e1|]; [by destruct s| |done].
535 assert (e1 ∈ [s, e2) :: ps2).
536 { constructor. by split; [apply limit_le_cases; right|]. }
537 apply Hequiv in H. inv H.
538 + destruct H1 as [_ H12]. by eapply (_ : Irreflexive limit_lt).
539 + apply Exists_exists in H1 as (p & Hp & He1).
540 rewrite Forall_forall in Hlt1.
541 apply Hlt1 in Hp.
542 destruct p as [sp ep].
543 unfold period_end, period_start in Hp.
544 assert (contra : (e1 < e1)%lim).
545 { by eapply limit_lt_le_trans; last apply He1. }
546 by eapply (_ : Irreflexive limit_lt).
547Qed.
548
549Lemma period_seq_nf_cons_equiv_inv_end p1 ps1 p2 ps2:
550 period_seq_nf (p1 :: ps1) →
551 period_seq_nf (p2 :: ps2) →
552 p1 :: ps1 ≡ p2 :: ps2 →
553 period_end p1 = period_end p2.
554Proof.
555 intros Hnf1 Hnf2 Hequiv.
556 destruct (decide (period_end p1 < period_end p2)%lim) as [He12|He21].
557 - exfalso. by eapply period_seq_nf_cons_equiv_inv_end_1 in He12.
558 - apply not_limit_lt, limit_le_cases in He21 as [He21|He21]; first done.
559 exfalso. by eapply period_seq_nf_cons_equiv_inv_end_1 in He21.
560Qed.
561
562Lemma period_seq_nf_cons_equiv_inv p1 ps1 p2 ps2:
563 period_seq_nf (p1 :: ps1) →
564 period_seq_nf (p2 :: ps2) →
565 p1 :: ps1 ≡ p2 :: ps2 →
566 p1 = p2.
567Proof.
568 intros Hnf1 Hnf2 Hequiv.
569 trans [period_start p1, period_end p1); first by destruct p1.
570 trans [period_start p2, period_end p2); last by destruct p2.
571 erewrite period_seq_nf_cons_equiv_inv_start; try done.
572 by erewrite period_seq_nf_cons_equiv_inv_end.
573Qed.
574
575Lemma period_seq_nf_equiv_L ps1 ps2 :
576 period_seq_nf ps1 →
577 period_seq_nf ps2 →
578 ps1 ≡ ps2 → ps1 = ps2.
579Proof.
580 intros Hnf1. revert ps2.
581 induction ps1 as [|p1 ps1]; intros ps2 Hnf2 Hequiv.
582 - destruct ps2; first done.
583 assert (period_nonempty p) as [t Ht]%period_nonempty_alt_iff.
584 { inv Hnf2. by inv H. }
585 assert (t ∈ p :: ps2) as contra%Hequiv.
586 { by apply Exists_cons_hd. }
587 inv contra.
588 - destruct ps2 as [|p2 ps2].
589 + assert (period_nonempty p1) as [t Ht]%period_nonempty_alt_iff.
590 { inv Hnf1. by inv H. }
591 assert (t ∈ p1 :: ps1) as contra%Hequiv.
592 { by apply Exists_cons_hd. }
593 inv contra.
594 + assert (p1 = p2) as <-.
595 { by eapply period_seq_nf_cons_equiv_inv. }
596 rename p1 into p.
597 apply period_seq_nf_cons in Hnf1 as (Hne1 & Hnf1 & Hlt1), Hnf2 as (Hne2 & Hnf2 & Hlt2).
598 f_equal. apply IHps1; [done..|].
599 intros t. split; intros Ht.
600 * assert (t ∈ p :: ps1) as H%Hequiv.
601 { by apply Exists_cons_tl. }
602 inv H; last done.
603 apply Exists_exists in Ht as ([sq eq] & Hp & Ht).
604 rewrite Forall_forall in Hlt1.
605 apply Hlt1 in Hp.
606 exfalso. destruct p as [s e].
607 simpl in *.
608 assert (contra : (t < t)%lim).
609 { trans e; first apply H1.
610 by eapply limit_lt_le_trans; last apply Ht. }
611 by eapply (_ : Irreflexive limit_lt).
612 * assert (t ∈ p :: ps2) as H%Hequiv.
613 { by apply Exists_cons_tl. }
614 inv H; last done.
615 apply Exists_exists in Ht as ([sq eq] & Hp & Ht).
616 rewrite Forall_forall in Hlt2.
617 apply Hlt2 in Hp.
618 exfalso. destruct p as [s e].
619 simpl in *.
620 assert (contra : (t < t)%lim).
621 { trans e; first apply H1.
622 by eapply limit_lt_le_trans; last apply Ht. }
623 by eapply (_ : Irreflexive limit_lt).
624Qed.
625
626Definition period_seq_intersection_comm ps1 ps2 :
627 period_seq_nf ps1 → period_seq_nf ps2 →
628 ps1 ∩ ps2 = ps2 ∩ ps1.
629Proof.
630 intros Hnf1 Hnf2.
631 apply period_seq_nf_equiv_L.
632 - by apply period_seq_intersection_nf.
633 - by apply period_seq_intersection_nf.
634 - by apply period_seq_intersection_comm_equiv.
635Qed.
636
637Instance period_seq_equiv_refl : Reflexive (≡@{period_seq}).
638Proof. done. Qed.
639
640Instance period_seq_equiv_equivalence : Equivalence (≡@{period_seq}).
641Proof. split; apply _. Qed.
642
643Variant bound :=
644 | LtBound of limit
645 | GeBound of limit.
646
647Definition bound_le b1 b2 :=
648 match b1, b2 with
649 | GeBound l1, GeBound l2 => (l1 ≤ l2)%lim
650 | GeBound _, LtBound _ => True
651 | LtBound l1, LtBound l2 => (l1 ≤ l2)%lim
652 | LtBound _, GeBound _ => False
653 end.
654Instance bound_lt_dec : RelDecision bound_le.
655Proof. intros [l1|l1] [l2|l2]; simpl; solve_decision. Qed.
656
657Instance bound_le_refl : Reflexive bound_le.
658Proof. by intros []; simpl. Qed.
659
660Instance bound_le_trans : Transitive bound_le.
661Proof. intros [] [] [] ? ?; simpl in *; done || by etrans. Qed.
662
663Instance bound_le_preorder : PreOrder bound_le.
664Proof. split; apply _. Qed.
665
666Instance bound_le_antisymm : AntiSymm (=) bound_le.
667Proof. intros [] [] ? ?; simpl in *; done || f_equal; by eapply (_ : AntiSymm (=) limit_le). Qed.
668
669Instance bound_le_partial_order : PartialOrder bound_le.
670Proof. split; apply _. Qed.
671
672Instance bound_le_trichotomy : Trichotomy (strict bound_le).
673Proof.
674 intros [] []; simpl in *.
675 - destruct (trichotomy _ l l0) as [?|[?|?]].
676 + left. split; simpl.
677 * apply limit_le_cases. by right.
678 * by apply not_limit_le.
679 + right. left. by subst.
680 + right. right. split; simpl.
681 * apply limit_le_cases. by right.
682 * by apply not_limit_le.
683 - right. right. split; simpl; [done|by intros ?].
684 - left. split; simpl; [done|by intros ?].
685 - destruct (trichotomy _ l l0) as [?|[?|?]].
686 + left. split; simpl.
687 * apply limit_le_cases. by right.
688 * by apply not_limit_le.
689 + right. left. by subst.
690 + right. right. split; simpl.
691 * apply limit_le_cases. by right.
692 * by apply not_limit_le.
693Qed.
694
695Instance bound_le_total_order : TotalOrder bound_le.
696Proof. split; apply _. Qed.
697
698Definition period_bounds '[s, e) :=
699 if decide (period_nonempty [s, e)) then [GeBound s; LtBound e] else [].
700
701Definition period_seq_bounds (ps : period_seq) :=
702 ps ≫= period_bounds.
703
704Definition period_seq_bounds_sorted (ps : period_seq) :=
705 merge_sort bound_le (period_seq_bounds ps).
706
707Variant window_filter_action :=
708 KickLeft | KickRight | NoAction.
709Fixpoint window_filter_aux {A} (f : A → A → window_filter_action) (x : A) (l : list A) :=
710 match l with
711 | [] => [x]
712 | y :: l' =>
713 match f x y with
714 | KickLeft => window_filter_aux f y l'
715 | KickRight => window_filter_aux f x l'
716 | NoAction => x :: window_filter_aux f y l'
717 end
718 end.
719Definition window_filter {A} (f : A → A → window_filter_action) (l : list A) :=
720 match l with
721 | [] => []
722 | x :: l' => window_filter_aux f x l'
723 end.
724
725Definition period_seq_bounds_clean (ps : period_seq) :=
726 window_filter (λ b1 b2, match b1, b2 with
727 | GeBound _, LtBound _ => NoAction
728 | GeBound _, GeBound _ => KickRight
729 | LtBound _, GeBound _ => NoAction
730 | LtBound _, LtBound _ => KickLeft
731 end)
732 (period_seq_bounds_sorted ps).
733
734Fixpoint period_seq_from_bounds (bs : list bound) : period_seq :=
735 match bs with
736 | GeBound s :: LtBound e :: bs' => [s, e) :: period_seq_from_bounds bs'
737 | _ => []
738 end.
739
740Definition period_seq_normalize (ps : period_seq) :=
741 period_seq_from_bounds (period_seq_bounds_clean ps).
742
743
744Lemma period_seq_normalize_lem_1 (ps : period_seq) :
745 period_seq_normalize ps ≡ ps.
746Proof.
747 Search merge_sort.
748 Search Total Trichotomy.
749
750
751(* TODO: continue here *) Admitted.
752
753Lemma period_seq_normalize_lem_2 (ps : period_seq) :
754 period_seq_nf (period_seq_normalize ps).
755Proof. (* TODO: and here *) Admitted.
756
757Definition period_seq_union (ps1 ps2 : period_seq) :=
758 period_seq_normalize (ps1 ++ ps2).
759Lemma period_seq_union_lem t ps1 ps2 :
760 t ∈ period_seq_union ps1 ps2 ↔ t ∈ ps1 ∨ t ∈ ps2.
761Proof.
762 split.
763 - intros Ht%(period_seq_normalize_lem_1 (ps1 ++ ps2)).
764 apply Exists_app in Ht as [Ht|Ht]; by [left|right].
765 - intros [Ht|Ht]; apply period_seq_normalize_lem_1, Exists_app; by [left|right].
766Qed.
767Lemma period_seq_union_nf ps1 ps2 :
768 period_seq_nf (period_seq_union ps1 ps2).
769Proof. apply period_seq_normalize_lem_2. Qed.
770
771Definition nf_period_seq := sig period_seq_nf.
772
773Instance period_seq_nf_pi ps : ProofIrrel (period_seq_nf ps).
774Proof.
775 unfold period_seq_nf. intros [P11 P12] [P21 P22].
776 f_equal; [apply Forall_pi | apply Sorted_pi]; apply _.
777Qed.
778
779Instance period_seq_empty : Empty period_seq := [].
780Lemma period_seq_empty_nf : period_seq_nf ∅.
781Proof. done. Qed.
782
783Instance period_seq_singleton : Singleton timestamp period_seq :=
784 λ t, [{[t]}].
785Lemma period_seq_singleton_lem_1 t : t ∈ ({[t]} : period_seq).
786Proof.
787 unfold singleton, period_seq_singleton.
788 constructor. apply period_singleton_lem_1.
789Qed.
790Lemma period_seq_singleton_lem_2 t t' : t' ∈ ({[t]} : period_seq) → t' = t.
791Proof.
792 unfold singleton, period_seq_singleton.
793 inv 1; last inv H1.
794 by apply period_singleton_lem_2.
795Qed.
796Lemma period_seq_singleton_nf t : period_seq_nf {[t]}.
797Proof.
798 unfold singleton, period_seq_singleton.
799 split.
800 - constructor; last constructor.
801 apply period_singleton_nonempty.
802 - constructor; constructor.
803Qed.
804
805Instance nf_period_seq_elem_of : ElemOf timestamp nf_period_seq :=
806 λ t ps, t ∈ `ps.
807Instance nf_period_seq_empty : Empty nf_period_seq :=
808 ∅ ↾ period_seq_empty_nf.
809Instance nf_period_seq_union : Union nf_period_seq :=
810 λ '(ps1↾_) '(ps2↾_), period_seq_union ps1 ps2 ↾ (period_seq_union_nf ps1 ps2).
811Instance nf_period_seq_singleton : Singleton timestamp nf_period_seq :=
812 λ t, {[t]} ↾ period_seq_singleton_nf t.
813
814Instance nf_period_seq_semiset : SemiSet timestamp nf_period_seq.
815Proof.
816 split.
817 - intros t Ht. inv Ht.
818 - split.
819 + apply period_seq_singleton_lem_2.
820 + intros <-. apply period_seq_singleton_lem_1.
821 - intros [ps1 Hnf1] [ps2 Hnf2] t.
822 unfold union, nf_period_seq_union, elem_of, nf_period_seq_elem_of.
823 simpl. apply period_seq_union_lem.
824Qed.
825
826Instance nf_period_seq_intersection : Intersection nf_period_seq :=
827 λ '(ps1↾Hnf1) '(ps2↾Hnf2), (ps1 ∩ ps2) ↾ (period_seq_intersection_nf ps1 ps2 Hnf1 Hnf2).
828
829(* TODO: difference!
830
831Instance nf_period_seq_set : Set_ timestamp nf_period_seq.
832Proof. (* TODO *) Qed.
833
834*)
diff --git a/server/formal/util.v b/server/formal/util.v
new file mode 100644
index 0000000..8e16ffc
--- /dev/null
+++ b/server/formal/util.v
@@ -0,0 +1,92 @@
1From stdpp Require Import numbers option sorting ssreflect.
2From stdpp Require Import options.
3
4Definition transportf {X} (P : X → Type) {x x' : X} : x = x' → P x → P x'.
5Proof. by induction 1. Defined.
6
7Instance HdRel_pi {A} (R : relation A) `{!EqDecision A} `{!∀ x y, ProofIrrel (R x y)} a l : ProofIrrel (HdRel R a l).
8Proof.
9 intros HR1 HR2.
10 assert (Hnil : ∀ xs (Hxs : [] = xs) (HR : HdRel R a xs),
11 HR = transportf _ Hxs (HdRel_nil R a)).
12 { intros. destruct HR; last done.
13 by replace Hxs with (eq_refl ([] : list A)); last apply eq_pi, list_eq_dec. }
14 assert (Hcons : ∀ xs x y xs' (Hxs : y :: xs' = xs) (HR : HdRel R x xs) (Hxy : R x y),
15 HR = transportf (HdRel R x) Hxs (HdRel_cons R x y xs' Hxy)).
16 { intros. destruct HR; first done.
17 injection Hxs as <- <-.
18 replace Hxs with (eq_refl (y :: xs')); last apply eq_pi, list_eq_dec.
19 simpl.
20 by replace r with Hxy by apply H. }
21 destruct l.
22 - trans (transportf (HdRel R a) eq_refl (HdRel_nil R a)).
23 + apply Hnil.
24 + symmetry. apply Hnil.
25 - apply HdRel_inv in HR1 as Haa0.
26 trans (transportf (HdRel R a) eq_refl (HdRel_cons R a a0 l Haa0)).
27 + apply Hcons.
28 + symmetry. apply Hcons.
29Qed.
30
31Instance Sorted_pi {A} (R : relation A) `{!EqDecision A} `{!∀ x y, ProofIrrel (R x y)} l : ProofIrrel (Sorted R l).
32Proof.
33 intros HS1 HS2.
34 assert (Hbase : ∀ xs (Hxs : [] = xs) (HS : Sorted R xs), HS = transportf _ Hxs (Sorted_nil R)).
35 { intros. destruct HS; last done.
36 by replace Hxs with (eq_refl ([] : list A)); last apply eq_pi, list_eq_dec. }
37 assert (Hind : ∀ xs x xs'
38 (Hxs : x :: xs' = xs) (HS : Sorted R xs)
39 (Hx : HdRel R x xs') (HS' : Sorted R xs')
40 (IH : ∀ HS1' HS2' : Sorted R xs', HS1' = HS2'),
41 HS = transportf _ Hxs (Sorted_cons HS' Hx)).
42 { intros. destruct HS; first done.
43 injection Hxs as <- <-.
44 replace Hxs with (eq_refl (x :: xs')); last apply eq_pi, list_eq_dec.
45 simpl.
46 replace h with Hx by apply: HdRel_pi.
47 by replace HS with HS' by apply IH. }
48 induction l.
49 - trans (transportf _ eq_refl (Sorted_nil R)).
50 + apply Hbase.
51 + symmetry. apply Hbase.
52 - destruct (Sorted_inv HS1) as [Hl Hal].
53 trans (transportf _ eq_refl (Sorted_cons Hl Hal)).
54 + apply Hind, IHl.
55 + symmetry. apply Hind, IHl.
56Qed.
57
58Instance Forall_pi {A} (P : A → Prop) (l : list A) `{!EqDecision A} `{!∀ a, ProofIrrel (P a)} : ProofIrrel (Forall P l).
59Proof.
60 intros HF1 HF2.
61 assert (Hbase : ∀ xs (Hxs : [] = xs) (HF : Forall P xs), HF = transportf (Forall P) Hxs (ListDef.Forall_nil P)).
62 { intros xs Hxs HF. destruct HF; last done.
63 by replace Hxs with (eq_refl ([] : list A)); last apply eq_pi, list_eq_dec. }
64 assert (Hind : ∀ xs x xs'
65 (Hxs : x :: xs' = xs) (HF : Forall P xs)
66 (Hx : P x) (HF' : Forall P xs')
67 (IH : ∀ HF1' HF2' : Forall P xs', HF1' = HF2'),
68 HF = transportf _ Hxs (ListDef.Forall_cons P x xs' Hx HF')).
69 { intros. destruct HF; first done.
70 injection Hxs as <- <-.
71 replace Hxs with (eq_refl (x :: xs')); last apply eq_pi, list_eq_dec.
72 simpl.
73 replace p with Hx by apply H.
74 by replace HF with HF' by apply IH. }
75 induction l.
76 - trans (transportf _ eq_refl (ListDef.Forall_nil P)).
77 + apply Hbase.
78 + symmetry. apply Hbase.
79 - apply Forall_inv in HF1 as Ha.
80 apply Forall_inv_tail in HF1 as Hl.
81 trans (transportf _ eq_refl (ListDef.Forall_cons P a l Ha Hl)).
82 + apply Hind, IHl.
83 + symmetry. apply Hind, IHl.
84Qed.
85
86Instance ex_pi {A} {B : A → Prop} `{!ProofIrrel A} `{!∀ x, ProofIrrel (B x)} :
87 ProofIrrel (∃ (x : A), B x).
88Proof.
89 intros [x Hx] [y Hy].
90 assert (y = x) by apply proof_irrel. subst.
91 assert (Hx = Hy) by apply proof_irrel. by subst.
92Qed.
diff --git a/server/hack/rwgps-get-auth-token.sh b/server/hack/rwgps-get-auth-token.sh
new file mode 100755
index 0000000..d7a14a5
--- /dev/null
+++ b/server/hack/rwgps-get-auth-token.sh
@@ -0,0 +1,14 @@
1#!/bin/bash
2
3rwgps_api_key="$(jq <config.json '.rwgps.api_key' -r)"
4
5echo -n "RWGPS account email: "
6read rwgps_email
7echo -n "RWGPS account password: "
8read rwgps_password
9
10jq -nc --arg email "$rwgps_email" --arg password "$rwgps_password" \
11 '{"user": {"email": $email, "password": $password}}' \
12 | curl --json @- -H "x-rwgps-api-key: $rwgps_api_key" \
13 https://ridewithgps.com/api/v1/auth_tokens.json
14echo
diff --git a/server/locale/.gitignore b/server/locale/.gitignore
new file mode 100644
index 0000000..caf01ec
--- /dev/null
+++ b/server/locale/.gitignore
@@ -0,0 +1 @@
dev/ \ No newline at end of file
diff --git a/server/locale/README b/server/locale/README
new file mode 100644
index 0000000..2710bce
--- /dev/null
+++ b/server/locale/README
@@ -0,0 +1,9 @@
1# Initializing for a new language
2
3$ msginit -i ../routemon.pot -l lang_country.encoding
4
5e.g. $ msginit -i ../routemon.pot -l nl_NL.UTF-8
6
7# Generating .mo files during development
8
9$ dev.sh \ No newline at end of file
diff --git a/server/locale/dev.sh b/server/locale/dev.sh
new file mode 100755
index 0000000..ad2fd46
--- /dev/null
+++ b/server/locale/dev.sh
@@ -0,0 +1,7 @@
1#!/bin/bash
2
3for pofile in *.po; do
4 dir="dev/${pofile%.po}/LC_MESSAGES"
5 mkdir -p "$dir"
6 msgfmt "$pofile" -o "$dir/routemon.mo"
7done
diff --git a/server/locale/en_US.po b/server/locale/en_US.po
new file mode 100644
index 0000000..d221ac0
--- /dev/null
+++ b/server/locale/en_US.po
@@ -0,0 +1,64 @@
1# English translations for routemon package.
2# Copyright (C) 2026 Rutger Broekhoff <[email protected]>
3# This file is distributed under the same license as the routemon package.
4# Rutger Broekhoff <[email protected]>, 2026.
5#
6msgid ""
7msgstr ""
8"Project-Id-Version: PACKAGE VERSION\n"
9"Report-Msgid-Bugs-To: \n"
10"POT-Creation-Date: 2026-08-28 09:20+0200\n"
11"PO-Revision-Date: 2026-08-28 14:31+0200\n"
12"Last-Translator: Rutger Broekhoff <[email protected]>\n"
13"Language-Team: English\n"
14"Language: en_US\n"
15"MIME-Version: 1.0\n"
16"Content-Type: text/plain; charset=UTF-8\n"
17"Content-Transfer-Encoding: 8bit\n"
18"Plural-Forms: nplurals=2; plural=(n != 1);\n"
19
20#: ../src/http_server.cppm:232
21msgid "No body expected for this request"
22msgstr "No body expected for this request"
23
24#: ../src/http_server.cppm:500
25msgid "Bad request"
26msgstr "Bad request"
27
28#: ../src/http_server.cppm:511 ../src/http_server.cppm:562
29msgid "Method not allowed"
30msgstr "Method not allowed"
31
32#: ../src/http_server.cppm:527
33msgid ""
34"Path of normalized (RFC 3986, § 6) origin-form request-target (RFC 9112, § "
35"3.2.1) should be absolute"
36msgstr "Path of normalized (RFC 3986, § 6) origin-form request-target (RFC 9112, § 3.2.1) should be absolute"
37
38#: ../src/http_server.cppm:538
39msgid "Not found"
40msgstr "Not found"
41
42#: ../src/http_server.cppm:549
43msgid "Method not implemented"
44msgstr "Method not implemented"
45
46#: ../src/http_server.cppm:573
47msgid ""
48"Invalid request-target, expected asterisk-form or origin-form (see RFC 9112, "
49"§ 3.2)"
50msgstr "Invalid request-target, expected asterisk-form or origin-form (see RFC 9112, § 3.2)"
51
52#: ../src/srv.cppm:148
53msgid "Failed to parse GPX file"
54msgstr "Failed to parse GPX file"
55
56#: ../src/srv.cppm:160
57msgid "Internal server error"
58msgstr "Internal server error"
59
60#~ msgid "Invalid point in GPX file"
61#~ msgstr "Invalid point in GPX file"
62
63#~ msgid "GPX file has no points in track"
64#~ msgstr "GPX file has no points in track"
diff --git a/server/locale/nl.po b/server/locale/nl.po
new file mode 100644
index 0000000..96b6cd9
--- /dev/null
+++ b/server/locale/nl.po
@@ -0,0 +1,64 @@
1# Translations for the routemon project.
2# Copyright (C) 2026 Rutger Broekhoff <[email protected]>
3# This file is distributed under the same license as the routemon package.
4# Rutger Broekhoff <[email protected]>, 2026.
5#
6msgid ""
7msgstr ""
8"Project-Id-Version: routemon 0.1.0\n"
9"Report-Msgid-Bugs-To: \n"
10"POT-Creation-Date: 2026-08-28 09:20+0200\n"
11"PO-Revision-Date: 2026-08-28 14:35+0200\n"
12"Last-Translator: Rutger Broekhoff <[email protected]>\n"
13"Language-Team: Dutch <[email protected]>\n"
14"Language: nl\n"
15"MIME-Version: 1.0\n"
16"Content-Type: text/plain; charset=UTF-8\n"
17"Content-Transfer-Encoding: 8bit\n"
18"Plural-Forms: nplurals=2; plural=(n != 1);\n"
19
20#: ../src/http_server.cppm:232
21msgid "No body expected for this request"
22msgstr "Geen body verwacht voor deze aanvraag"
23
24#: ../src/http_server.cppm:500
25msgid "Bad request"
26msgstr "Ongeldige aanvraag"
27
28#: ../src/http_server.cppm:511 ../src/http_server.cppm:562
29msgid "Method not allowed"
30msgstr "Aanvraagmethode niet toegestaan"
31
32#: ../src/http_server.cppm:527
33msgid ""
34"Path of normalized (RFC 3986, § 6) origin-form request-target (RFC 9112, § "
35"3.2.1) should be absolute"
36msgstr "Pad van genormaliseerde (RFC 3986, § 6) origin-form request-target (RFC 9112, § 3.2.1) behoort absoluut te zijn"
37
38#: ../src/http_server.cppm:538
39msgid "Not found"
40msgstr "Niet gevonden"
41
42#: ../src/http_server.cppm:549
43msgid "Method not implemented"
44msgstr "Aanvraagmethode niet geïmplementeerd"
45
46#: ../src/http_server.cppm:573
47msgid ""
48"Invalid request-target, expected asterisk-form or origin-form (see RFC 9112, "
49"§ 3.2)"
50msgstr "Ongeldige request-target, asterisk-form of origin-form verwacht (zie RFC 9112, § 3.2)"
51
52#: ../src/srv.cppm:148
53msgid "Failed to parse GPX file"
54msgstr "GPX-bestand kon niet geladen worden"
55
56#: ../src/srv.cppm:160
57msgid "Internal server error"
58msgstr "Interne serverfout"
59
60#~ msgid "Invalid point in GPX file"
61#~ msgstr "Ongeldig punt in GPX-bestand"
62
63#~ msgid "GPX file has no points in track"
64#~ msgstr "GPX-bestand mist punten in de track"
diff --git a/server/locale/xget.sh b/server/locale/xget.sh
new file mode 100755
index 0000000..06b5775
--- /dev/null
+++ b/server/locale/xget.sh
@@ -0,0 +1,13 @@
1#!/bin/bash
2
3xgettext --keyword=translate:1,1t --keyword=translate:1c,2,2t \
4 --keyword=translate:1,2,3t --keyword=translate:1c,2,3,4t \
5 --keyword=gettext:1 --keyword=pgettext:1c,2 \
6 --keyword=ngettext:1,2 --keyword=npgettext:1c,2,3 \
7 --from-code=UTF-8 --language=C++ \
8 ../src/*.cpp ../src/*.cppm \
9 -o ../routemon.pot
10
11for po_file in *.po; do
12 msgmerge "$po_file" ../routemon.pot -U
13done
diff --git a/server/migrations/1_init_down.sql b/server/migrations/1_init_down.sql
new file mode 100644
index 0000000..795e617
--- /dev/null
+++ b/server/migrations/1_init_down.sql
@@ -0,0 +1 @@
DROP TABLE migration;
diff --git a/server/migrations/1_init_up.sql b/server/migrations/1_init_up.sql
new file mode 100644
index 0000000..7edb398
--- /dev/null
+++ b/server/migrations/1_init_up.sql
@@ -0,0 +1,7 @@
1BEGIN;
2
3CREATE TABLE migration (version);
4
5INSERT INTO migration VALUES (1);
6
7COMMIT;
diff --git a/server/migrations/2_kaas_up.sql b/server/migrations/2_kaas_up.sql
new file mode 100644
index 0000000..0c7837a
--- /dev/null
+++ b/server/migrations/2_kaas_up.sql
@@ -0,0 +1,23 @@
1BEGIN;
2
3-- TODO enable strict mode so that primary key is automatically enforced to not be NULL
4CREATE TABLE received_route (
5 id INTEGER PRIMARY KEY,
6
7 received_route_source route_source NOT NULL,
8 recieved_route_strava_id TEXT,
9
10 -- ON DELETE what?
11 FOREIGN KEY (received_route_source_id) REFERENCES received_route_source (id),
12 CHECK (received_route_source IN ('gpx_upload', 'strava', 'rwgps')),
13 CHECK ((received_route_source = 'strava') = (received_route_strava_id IS NULL))
14);
15
16CREATE TABLE received_route_linestring (
17 received_route_id INT NOT NULL,
18 linestring BLOB NOT NULL,
19
20 FOREIGN KEY (received_route_id) REFERENCES received_route (id)
21);
22
23COMMIT;
diff --git a/server/routemon.pot b/server/routemon.pot
new file mode 100644
index 0000000..711df4b
--- /dev/null
+++ b/server/routemon.pot
@@ -0,0 +1,58 @@
1# SOME DESCRIPTIVE TITLE.
2# Copyright (C) YEAR THE PACKAGE'S COPYRIGHT HOLDER
3# This file is distributed under the same license as the PACKAGE package.
4# FIRST AUTHOR <EMAIL@ADDRESS>, YEAR.
5#
6#, fuzzy
7msgid ""
8msgstr ""
9"Project-Id-Version: PACKAGE VERSION\n"
10"Report-Msgid-Bugs-To: \n"
11"POT-Creation-Date: 2026-08-28 09:20+0200\n"
12"PO-Revision-Date: YEAR-MO-DA HO:MI+ZONE\n"
13"Last-Translator: FULL NAME <EMAIL@ADDRESS>\n"
14"Language-Team: LANGUAGE <[email protected]>\n"
15"Language: \n"
16"MIME-Version: 1.0\n"
17"Content-Type: text/plain; charset=UTF-8\n"
18"Content-Transfer-Encoding: 8bit\n"
19
20#: ../src/http_server.cppm:232
21msgid "No body expected for this request"
22msgstr ""
23
24#: ../src/http_server.cppm:500
25msgid "Bad request"
26msgstr ""
27
28#: ../src/http_server.cppm:511 ../src/http_server.cppm:562
29msgid "Method not allowed"
30msgstr ""
31
32#: ../src/http_server.cppm:527
33msgid ""
34"Path of normalized (RFC 3986, § 6) origin-form request-target (RFC 9112, § "
35"3.2.1) should be absolute"
36msgstr ""
37
38#: ../src/http_server.cppm:538
39msgid "Not found"
40msgstr ""
41
42#: ../src/http_server.cppm:549
43msgid "Method not implemented"
44msgstr ""
45
46#: ../src/http_server.cppm:573
47msgid ""
48"Invalid request-target, expected asterisk-form or origin-form (see RFC 9112, "
49"§ 3.2)"
50msgstr ""
51
52#: ../src/srv.cppm:148
53msgid "Failed to parse GPX file"
54msgstr ""
55
56#: ../src/srv.cppm:160
57msgid "Internal server error"
58msgstr ""
diff --git a/server/src/api.cpp b/server/src/api.cpp
new file mode 100644
index 0000000..b3c8e31
--- /dev/null
+++ b/server/src/api.cpp
@@ -0,0 +1,206 @@
1module;
2
3#include <boost/geometry.hpp>
4#include <boost/json.hpp>
5
6module routemon:api$impl;
7
8import std;
9import :api;
10import :datex2;
11import :geo;
12import :gpx;
13import :log;
14import :req_ctx;
15import :time;
16import :trace;
17
18namespace {
19
20 namespace chrono = std::chrono;
21 namespace json = boost::json;
22 namespace views = std::views;
23
24} // namespace <anonymous>
25
26namespace routemon::api {
27
28 auto json_value_from_point(geo::point const& p) -> json::value {
29 return json::array{bgeo::get<1>(p), bgeo::get<0>(p)};
30 }
31 auto json_value_from_linestring(geo::linestring const& ls) -> json::value {
32 json::array a;
33 for (auto const& p : ls)
34 a.push_back(json_value_from_point(p));
35 return a;
36 }
37 auto json_value_from_linestrings(std::vector<geo::linestring> const& lss) -> json::value {
38 json::array a;
39 for (auto const& ls : lss)
40 a.push_back(json_value_from_linestring(ls));
41 return a;
42 }
43
44 auto tag_invoke(json::value_from_tag, json::value& jv, relevant_road_closure const& clo) -> void {
45 jv = json::object{
46 {"relevant_lss", json_value_from_linestrings(clo.relevant_lss)},
47 };
48 }
49 auto tag_invoke(json::value_from_tag, json::value& jv, relevant_situation const& sit) -> void {
50 jv = json::object{
51 {"id", json::value_from(sit.id)},
52 {"location", sit.location ? json_value_from_point(*sit.location) : nullptr},
53 {"comments", json::value_from(sit.comments)},
54 {"relevant_road_closures", json::value_from(sit.relevant_road_closures)},
55 };
56 }
57 auto tag_invoke(json::value_from_tag, json::value& jv, track_segment const& seg) -> void {
58 jv = json::object{
59 {"points", json_value_from_linestring(seg.points)},
60 };
61 }
62 auto tag_invoke(json::value_from_tag, json::value& jv, track const& track) -> void {
63 jv = json::object{
64 {"segments", json::value_from(track.segments)},
65 };
66 }
67 auto tag_invoke(json::value_from_tag, json::value& jv, process_gpx_result const& res) -> void {
68 jv = json::object{
69 {"tracks", json::value_from(res.tracks)},
70 {"relevant_situations", json::value_from(res.relevant_situations)},
71 };
72 }
73 auto tag_invoke(json::value_from_tag, json::value& jv, sysinfo const& info) -> void {
74 jv = json::object{
75 {"using_publication_of", std::format("{:%FT%TZ}", info.using_publication_of)},
76 };
77 }
78
79 handler::handler(log::logger const& l, datex2::situation_publication pub)
80 : l_{l.sub("handler")}, pub_{std::move(pub)}
81 {
82 l_.info("Building indices");
83 auto const before_build = chrono::steady_clock::now();
84 for (auto const& sit : pub_.situations) {
85 for (auto const& rc : sit->road_closures) {
86 for (auto const& ls : rc->relevant_line_strings) {
87 auto box = geo::box{};
88 bgeo::envelope(*ls, box);
89 lse_index_.insert(std::make_tuple(box, ls, rc));
90 }
91 for (auto p : rc->relevant_points) {
92 p_index_.insert(std::make_pair(p, rc));
93 }
94 }
95 }
96 auto const after_build = chrono::steady_clock::now();
97 auto const dur_build = chrono::duration_cast<chrono::milliseconds>(after_build - before_build);
98 l_.info("Indices built in {}", dur_build);
99 l_.info("LSE index size: {}", lse_index_.size());
100 l_.info("Point index size: {}", p_index_.size());
101 }
102
103 auto handler::process_gpx(gpx::file&& gpx_file) -> std::optional<process_gpx_result> {
104 auto const now = chrono::utc_clock::now();
105 auto const relevant = std::initializer_list<time::period>{time::period{now - chrono::days(7), now + chrono::days(7)}};
106 auto const check_periods = time::period_seq{relevant.begin(), relevant.end()};
107
108 auto splits_with_overlap_segments = std::vector<geo::linestring>{};
109 for (auto const& track : gpx_file.tracks)
110 for (auto const& seg : track.segments)
111 geo::split_linestring_with_overlap_segments(seg.waypoints, 5000 /* meters max total dist until a new split is forced */,
112 splits_with_overlap_segments);
113 auto const before_query = chrono::steady_clock::now();
114
115 l_.debug("Querying for relevant situations");
116 auto relevant_road_closures = std::unordered_set<std::shared_ptr<datex2::road_closure>>{};
117 auto ls_checked = 0uz;
118 auto p_checked = 0uz;
119 auto i = 0;
120 for (geo::linestring const& part : splits_with_overlap_segments) {
121 l_.debug("Checking part [{}/{}]", ++i, splits_with_overlap_segments.size());
122
123 auto part_box = geo::box{};
124 bgeo::envelope(part, part_box);
125
126 for (auto it = lse_index_.qbegin(bgeo::index::intersects(part_box)); it != lse_index_.qend(); it++) {
127 // Cannot use structured bindings here, as boost::geometry::get interferes with ADL.
128 // It is a candidate as the namespace boost::geometry is part of the associated namespace set,
129 // which happens because geo::linestring ≡ boost::geometry::model::linestring<geo::point> is part
130 // of the whole tuple type (lse_index_value) that is the value_type of the iterator.
131 std::shared_ptr<geo::linestring> const& ls = std::get<1>(*it);
132 std::shared_ptr<datex2::road_closure> const& rc = std::get<2>(*it);
133 if (rc->validity && rc->validity->intersect(check_periods).periods().empty())
134 continue;
135 if (bgeo::distance(*ls, part, geo::vincenty_strategy{}) < 5.0)
136 relevant_road_closures.emplace(rc);
137 ls_checked++;
138 }
139 for (auto it = p_index_.qbegin(bgeo::index::intersects(part_box)); it != p_index_.qend(); it++) {
140 // Cannot use structured bindings here for the same reason as above.
141 geo::point const& p = std::get<0>(*it);
142 std::shared_ptr<datex2::road_closure> const& rc = std::get<1>(*it);
143 if (rc->validity && rc->validity->intersect(check_periods).periods().empty())
144 continue;
145 if (bgeo::distance(p, part, geo::vincenty_strategy{}) < 5.0)
146 relevant_road_closures.emplace(rc);
147 p_checked++;
148 }
149 }
150
151 auto const after_query = chrono::steady_clock::now();
152 l_.debug("Done (checked {} line string(s) and {} point(s)) in {}",
153 ls_checked, p_checked, chrono::duration_cast<chrono::milliseconds>(after_query - before_query));
154
155 auto relevant_situations = std::unordered_set<std::shared_ptr<datex2::situation>>{};
156 for (auto const& rc : relevant_road_closures)
157 relevant_situations.emplace(rc->parent);
158
159 l_.debug("Identified {} relevant road closure(s), part of {} unique situation(s)",
160 relevant_road_closures.size(), relevant_situations.size());
161 for (auto const& sit : relevant_situations)
162 l_.debug("Relevant situation: {}", sit->id);
163
164 return process_gpx_result{
165 .tracks = gpx_file.tracks
166 | views::transform([](auto const& trk) -> track {
167 return {
168 .segments = trk.segments
169 | views::transform([](auto const& seg) -> track_segment {
170 return {.points = seg.waypoints};
171 })
172 | std::ranges::to<std::vector<track_segment>>(),
173 };
174 })
175 | std::ranges::to<std::vector<track>>(),
176 .relevant_situations = relevant_situations
177 | views::transform([&](std::shared_ptr<datex2::situation> sit) -> relevant_situation {
178 return {
179 .id = sit->id,
180 .location = sit->location,
181 .comments = sit->comments,
182 .relevant_road_closures = relevant_road_closures
183 | views::filter([&](std::shared_ptr<datex2::road_closure> const& rc) -> bool {
184 return std::shared_ptr{rc->parent} == sit;
185 })
186 | views::transform([](std::shared_ptr<datex2::road_closure> const& rc) -> relevant_road_closure {
187 return {
188 .relevant_lss = rc->relevant_line_strings
189 | views::transform([](auto const& lsp) -> geo::linestring {
190 return *lsp;
191 })
192 | std::ranges::to<std::vector<geo::linestring>>(),
193 };
194 })
195 | std::ranges::to<std::vector<relevant_road_closure>>(),
196 };
197 })
198 | std::ranges::to<std::vector<relevant_situation>>(),
199 };
200 }
201
202 auto handler::sysinfo() -> struct sysinfo {
203 return {.using_publication_of = pub_.publication_time};
204 }
205
206} // namespace routemon::api
diff --git a/server/src/api.cppm b/server/src/api.cppm
new file mode 100644
index 0000000..caeb44c
--- /dev/null
+++ b/server/src/api.cppm
@@ -0,0 +1,79 @@
1module;
2
3#include <boost/geometry.hpp>
4#include <boost/json.hpp>
5
6export module routemon:api;
7
8import std;
9import :datex2;
10import :geo;
11import :gpx;
12import :log;
13import :time;
14import :trace;
15
16namespace {
17
18 namespace chrono = std::chrono;
19 namespace json = boost::json;
20 namespace views = std::views;
21
22} // namespace <anonymous>
23
24export
25namespace routemon::api {
26
27 struct relevant_road_closure {
28 std::vector<geo::linestring> relevant_lss;
29 };
30 auto tag_invoke(json::value_from_tag, json::value& jv, relevant_road_closure const& clo) -> void;
31
32 struct relevant_situation {
33 std::string id;
34 std::optional<geo::point> location;
35 std::vector<std::string> comments;
36 std::vector<relevant_road_closure> relevant_road_closures;
37 };
38 auto tag_invoke(json::value_from_tag, json::value& jv, relevant_situation const& sit) -> void;
39
40 struct track_segment {
41 geo::linestring points;
42 };
43 auto tag_invoke(json::value_from_tag, json::value& jv, track_segment const& seg) -> void;
44
45 struct track {
46 std::vector<track_segment> segments;
47 };
48 auto tag_invoke(json::value_from_tag, json::value& jv, track const& track) -> void;
49
50 struct process_gpx_result {
51 std::vector<track> tracks;
52 std::vector<relevant_situation> relevant_situations;
53 };
54 auto tag_invoke(json::value_from_tag, json::value& jv, process_gpx_result const& res) -> void;
55
56 struct sysinfo {
57 time::timestamp using_publication_of;
58 };
59 auto tag_invoke(json::value_from_tag, json::value& jv, sysinfo const& info) -> void;
60
61 class handler {
62 using lse_index_value = std::tuple<geo::box, std::shared_ptr<geo::linestring>, std::shared_ptr<datex2::road_closure>>;
63 using p_index_value = std::pair<geo::point, std::shared_ptr<datex2::road_closure>>;
64 using lse_index = bgeo::index::rtree<lse_index_value, bgeo::index::quadratic<16>>;
65 using p_index = bgeo::index::rtree<p_index_value, bgeo::index::quadratic<16>>;
66
67 log::logger l_;
68 datex2::situation_publication pub_;
69 lse_index lse_index_;
70 p_index p_index_;
71
72 public:
73 explicit handler(log::logger const& l, datex2::situation_publication pub);
74
75 auto process_gpx(gpx::file&& gpx_file) -> std::optional<process_gpx_result>;
76 auto sysinfo() -> sysinfo;
77 };
78
79} // namespace routemon::api
diff --git a/server/src/config.cpp b/server/src/config.cpp
new file mode 100644
index 0000000..3b17691
--- /dev/null
+++ b/server/src/config.cpp
@@ -0,0 +1,167 @@
1module;
2
3#include <boost/json.hpp>
4#include <boost/system/system_error.hpp>
5
6module routemon:config$impl;
7
8import std;
9import :config;
10import :log;
11import :util;
12
13namespace json = boost::json;
14
15namespace routemon::config {
16
17 class location {
18 std::optional<std::pair<std::string_view, util::not_null<location const*>>> next_;
19
20 auto append_to(std::string& s) const -> void {
21 if (next_) {
22 s += next_->first;
23 s += ".";
24 next_->second->append_to(s);
25 }
26 }
27
28 public:
29 location() = default;
30
31 explicit location(location const& next, std::string_view entry)
32 : next_{std::make_pair(entry, util::not_null{&next})}
33 {}
34
35 [[nodiscard]] auto to_string() const -> std::string {
36 if (!next_)
37 return "";
38 auto s = std::string{next_->first};
39 next_->second->append_to(s);
40 return s;
41 }
42
43 auto sub(std::string_view entry) const& -> location {
44 return location{*this, entry};
45 }
46 };
47
48 class object_reader {
49 location loc_;
50 json::object const& obj_;
51 std::unordered_set<std::string> visited_;
52
53 public:
54 object_reader(json::value const& jv, location loc)
55 try : loc_{std::move(loc)}, obj_{jv.as_object()}
56 {} catch (boost::system::system_error const&) {
57 throw std::runtime_error{std::format("expected an object at {}", loc.to_string())};
58 }
59
60 auto check_unused() const -> void {
61 for (auto const& kv : obj_) {
62 if (!visited_.contains(std::string{kv.key()})) {
63 throw std::runtime_error{std::format("unexpected key {}", loc_.sub(kv.key()).to_string())};
64 }
65 }
66 }
67
68 template<class T>
69 auto expect_at(std::string_view key) -> T {
70 visited_.emplace(key);
71 auto const loc = loc_.sub(key);
72 if (auto const jv = obj_.try_at(key)) {
73 try {
74 return json::value_to<T>(*jv, loc);
75 } catch (boost::system::system_error const& e) {
76 throw std::runtime_error{std::format("failed to read {}: {}", loc.to_string(), e.code().message())};
77 }
78 } else {
79 throw std::runtime_error{std::format("did not find expected key {}", loc.to_string())};
80 }
81 }
82 };
83
84 auto as_checked_object(json::value const& jv, location const& loc, std::invocable<object_reader&> auto const& f) -> decltype(f(std::declval<object_reader&>())) {
85 auto r = object_reader{jv, loc};
86 auto&& v = f(r);
87 r.check_unused();
88 return std::forward<decltype(f(r))>(v);
89 }
90
91 auto tag_invoke(json::value_to_tag<rwgps> const&, json::value const& jv, location const& loc) -> rwgps {
92 return as_checked_object(jv, loc, [](object_reader& r) -> rwgps {
93 return {
94 .api_key = r.expect_at<std::string>("api_key"),
95 .auth_token = r.expect_at<std::string>("auth_token"),
96 };
97 });
98 }
99
100 auto tag_invoke(json::value_to_tag<situations> const&, json::value const& jv, location const& loc) -> situations {
101 return as_checked_object(jv, loc, [](object_reader& r) -> situations {
102 return {
103 .datex2_filename = r.expect_at<std::string>("datex2_filename"),
104 };
105 });
106 }
107
108 auto tag_invoke(json::value_to_tag<database> const&, json::value const& jv, location const& loc) -> database {
109 return as_checked_object(jv, loc, [](object_reader& r) -> database {
110 return {
111 .sqlite3_filename = r.expect_at<std::string>("sqlite3_filename"),
112 };
113 });
114 }
115
116 auto tag_invoke(json::value_to_tag<http_server> const&, json::value const& jv, location const& loc) -> http_server {
117 return as_checked_object(jv, loc, [](object_reader& r) -> http_server {
118 return {
119 .lax_cors = r.expect_at<bool>("lax_cors"),
120 };
121 });
122 }
123
124 auto tag_invoke(json::value_to_tag<logger> const&, json::value const& jv, location const& loc) -> logger {
125 return as_checked_object(jv, loc, [obj_loc = loc](object_reader& r) -> logger {
126 auto const level_str = r.expect_at<std::string>("level");
127 auto level = log::level{};
128 if (level_str == "debug")
129 level = log::level::debug;
130 else if (level_str == "info")
131 level = log::level::info;
132 else if (level_str == "warn")
133 level = log::level::warn;
134 else if (level_str == "error")
135 level = log::level::error;
136 else
137 throw std::runtime_error{std::format("unable to parse log level {:?} at {}: expected one of {{debug, info, warn, error}}", level_str, obj_loc.sub("level").to_string())};
138 return logger{level};
139 });
140 }
141
142 auto json_value_to_app(json::value const& jv) -> app {
143 return as_checked_object(jv, location{}, [](object_reader& r) -> app {
144 return {
145 .rwgps = r.expect_at<rwgps>("rwgps"),
146 .situations = r.expect_at<situations>("situations"),
147 .database = r.expect_at<database>("database"),
148 .http_server = r.expect_at<http_server>("http_server"),
149 .logger = r.expect_at<logger>("logger"),
150 };
151 });
152 }
153
154 auto load_file(std::string const& filename) -> app {
155 auto f = std::ifstream{filename}; // TODO: ensure that we are opening in binary mode?
156 if (!f.is_open())
157 throw std::runtime_error{std::format("failed to open {}", filename)};
158 auto jv = json::value{};
159 try {
160 jv = json::parse(f);
161 } catch (boost::system::system_error const& e) {
162 throw std::runtime_error{std::format("failed to parse: {}", e.code().message())};
163 }
164 return json_value_to_app(jv);
165 }
166
167} // namespace routemon::config
diff --git a/server/src/config.cppm b/server/src/config.cppm
new file mode 100644
index 0000000..ef827a6
--- /dev/null
+++ b/server/src/config.cppm
@@ -0,0 +1,39 @@
1export module routemon:config;
2
3import std;
4import :log;
5
6namespace routemon::config {
7
8 export struct rwgps {
9 std::string api_key;
10 std::string auth_token;
11 };
12
13 export struct situations {
14 std::string datex2_filename;
15 };
16
17 export struct database {
18 std::string sqlite3_filename;
19 };
20
21 export struct http_server {
22 bool lax_cors;
23 };
24
25 export struct logger {
26 log::level level;
27 };
28
29 export struct app {
30 rwgps rwgps;
31 situations situations;
32 database database;
33 http_server http_server;
34 logger logger;
35 };
36
37 export auto load_file(std::string const& filename) -> app;
38
39} // namespace routemon::config
diff --git a/server/src/database.cppm b/server/src/database.cppm
new file mode 100644
index 0000000..0312dda
--- /dev/null
+++ b/server/src/database.cppm
@@ -0,0 +1,37 @@
1export module routemon:database;
2
3import std;
4import :sqlite3;
5
6namespace routemon::database {
7
8 static constexpr std::int64_t expected_database_version = 1;
9
10 export class connection {
11 sqlite3::connection dbc_;
12
13 explicit connection(sqlite3::connection dbc) : dbc_{std::move(dbc)} {}
14
15 friend auto open(std::string const& filename) -> std::shared_ptr<connection>;
16
17 public:
18 // Nothing here yet
19 };
20
21 export auto open(std::string const& filename) -> std::shared_ptr<connection> {
22 auto dbc = sqlite3::open(filename);
23 try {
24 auto version = std::optional<std::int64_t>{};
25 dbc.query("SELECT version FROM migration;").scan_single(version);
26 if (!version)
27 throw std::runtime_error{"failed to fetch database migration version"};
28 if (version != expected_database_version) {
29 throw std::runtime_error{std::format("database migration version ({}) does not match expected version ({}), consider running migrations", *version, expected_database_version)};
30 }
31 } catch (std::exception const& e) {
32 throw std::runtime_error{std::format("failed to query database version: {}", e.what())};
33 }
34 return std::shared_ptr<connection>{new connection{std::move(dbc)}};
35 }
36
37} // namespace routemon::database
diff --git a/server/src/datex2.cppm b/server/src/datex2.cppm
new file mode 100644
index 0000000..b507e6f
--- /dev/null
+++ b/server/src/datex2.cppm
@@ -0,0 +1,296 @@
1module;
2
3#include <boost/geometry/algorithms/is_empty.hpp>
4#include <boost/geometry/srs/transformation.hpp>
5#include <boost/geometry/srs/epsg.hpp>
6
7#include <pugixml.hpp>
8
9export module routemon:datex2;
10
11import std;
12import :geo;
13import :time;
14import :util;
15
16using namespace std::literals::string_view_literals;
17
18namespace routemon::datex2 {
19
20 export struct situation;
21
22 export struct road_closure {
23 std::weak_ptr<situation> parent;
24 std::optional<time::period_seq> validity;
25 std::vector<geo::point> relevant_points = {};
26 std::vector<std::shared_ptr<geo::linestring>> relevant_line_strings = {};
27 };
28
29 export struct situation {
30 std::string id;
31 std::optional<geo::point> location = std::nullopt; // as shown on the map, not used for querying
32 std::vector<std::string> comments = {};
33 std::vector<std::shared_ptr<road_closure>> road_closures = {};
34 };
35
36 export struct situation_publication {
37 time::timestamp publication_time;
38 std::vector<std::shared_ptr<situation>> situations;
39 };
40
41 auto parse_timestamp(char const* in) -> std::optional<time::timestamp> {
42 auto res = time::timestamp{};
43 auto is = std::istringstream{in};
44 is >> std::chrono::parse("%Y-%m-%dT%H:%M:%SZ", res);
45 return is.fail() ? std::nullopt : std::make_optional(res);
46 }
47
48 export class loader {
49 // ETRS 89 (EPSG:4258) -> WGS 84 (EPSG:4326)
50 bgeo::srs::transformation<bgeo::srs::static_epsg<4258>, bgeo::srs::static_epsg<4326>> etrs89_to_wgs84_{};
51
52 std::multiset<std::string> warnings_;
53
54 auto add_location_from_xml(road_closure& rc, pugi::xml_node const& loc_xml) -> void {
55 auto loc_xml_type = std::string_view{loc_xml.attribute("xsi:type").value()};
56 if (loc_xml_type == "loc:ItineraryByIndexedLocations") {
57 for (auto const loc_cont_xml : loc_xml.children("loc:locationContainedInItinerary")) {
58 add_location_from_xml(rc, loc_cont_xml.child("loc:location"));
59 }
60 } else if (loc_xml_type == "loc:LinearLocation" || loc_xml_type == "loc:SingleRoadLinearLocation") {
61 auto const& loc_gml_xml = loc_xml.child("loc:gmlLineString");
62 if (!loc_gml_xml)
63 return;
64
65 auto const srs_name = std::string_view{loc_gml_xml.attribute("srsName").value()};
66 if (srs_name != "WGS 84"sv) {
67 warnings_.insert(std::format("don't now how to handle the CRS {}", srs_name));
68 return;
69 }
70 auto const pos_list_str = std::string_view{loc_gml_xml.child_value("loc:posList")};
71 // lat1 long1 lat2 long2 ... lat(n-1) long(n-1) latn longn
72
73 auto ls = std::make_shared<geo::linestring>();
74
75 auto lat_set = false;
76 auto lat = 0.0;
77 for (auto const lat_or_long_str : std::views::split(pos_list_str, " "sv)) {
78 auto mlat_or_long = util::parse_double(std::string_view{lat_or_long_str});
79 if (!mlat_or_long) {
80 warnings_.insert(std::format("failed to parse coordinate {:?}", std::string_view{lat_or_long_str}));
81 return;
82 }
83
84 if (!lat_set) {
85 lat = *mlat_or_long;
86 lat_set = true;
87 } else {
88 bgeo::append(*ls, geo::point{*mlat_or_long, lat});
89 lat = 0;
90 lat_set = false;
91 }
92 }
93
94 if (bgeo::is_empty(*ls)) {
95 warnings_.emplace("empty line string in data set");
96 return;
97 }
98
99 rc.relevant_line_strings.push_back(ls);
100 } else if (loc_xml_type == "loc:PointLocation") {
101 auto const& coords_xml = loc_xml.child("loc:pointByCoordinates").child("loc:pointCoordinates");
102 if (!coords_xml)
103 return;
104
105 auto mlat = util::parse_double(coords_xml.child_value("loc:latitude"));
106 auto mlon = util::parse_double(coords_xml.child_value("loc:longitude"));
107 if (!mlat || !mlon) {
108 warnings_.emplace("failed to parse PointLocation coordinates");
109 return;
110 }
111
112 // Vaag genoeg zegt NDW dat het hier om WGS 84 gaat:
113 // https://docs.ndw.nu/en/dataformaten/datex2-v3/elementen/locationreferencing/pointCoordinates/
114 // maar heeft het UML-model van DATEX II v3 het over ETRS 89:
115 // https://docs.datex2.eu/_static/data/v3.7/umlmodel/html/EARoot/EA3/EA3/EA5/EA676.htm
116
117 auto const coords_etrs89 = geo::point{*mlon, *mlat};
118 auto coords_wgs84 = geo::point{};
119 etrs89_to_wgs84_.forward(coords_etrs89, coords_wgs84);
120
121 rc.relevant_points.push_back(coords_wgs84);
122 } else {
123 warnings_.insert(std::format("don't know how to hande location of type {}, ignoring", loc_xml.attribute("xsi:type").value()));
124 return;
125 }
126 }
127
128 auto handle_road_or_carriageway_or_lane_management(pugi::xml_node const& record_xml, std::weak_ptr<situation> parent) -> std::optional<std::shared_ptr<road_closure>> {
129 auto const type = std::string_view{record_xml.child("sit:roadOrCarriagewayOrLaneManagementType").child_value()};
130 if (type != "carriagewayClosures" && type != "roadClosed")
131 // TODO: checken of er nog andere types fietsers de doorgang zouden kunnen blokkeren?
132 return std::nullopt;
133
134 auto const& restricted_vehicle_types_xml = record_xml.child("sit:forVehiclesWithCharacteristicsOf");
135 bool likely_restriction_for_bikes = restricted_vehicle_types_xml.empty();
136 for (auto const vehicle_type_xml : restricted_vehicle_types_xml.children("com:vehicleType")) {
137 auto vehicle_type = std::string_view{vehicle_type_xml.child_value()};
138 if (vehicle_type == "anyVehicle" || vehicle_type == "bicycle" ||
139 vehicle_type == "unknown" || vehicle_type == "other") {
140 likely_restriction_for_bikes = true;
141 }
142 }
143 if (!likely_restriction_for_bikes)
144 return std::nullopt;
145
146 //---- Check if within the defined validity period
147
148 auto validity = std::optional<time::period_seq>{};
149 auto const& validity_xml = record_xml.child("sit:validity");
150 if (validity_xml && validity_xml.child_value("com:validityStatus") == "definedByValidityTimeSpec"sv) {
151 auto const& validity_spec_xml = validity_xml.child("com:validityTimeSpecification");
152
153 auto valid_periods = std::vector<time::period>{};
154 auto exception_periods = std::vector<time::period>{};
155
156 // TODO: com:overallEndTime may be missing (according to the DATEX II v3 data model)
157 auto const overall_start_time = parse_timestamp(validity_spec_xml.child_value("com:overallStartTime"));
158 auto const overall_end_time = parse_timestamp(validity_spec_xml.child_value("com:overallEndTime"));
159 if (overall_start_time && overall_end_time && *overall_start_time < *overall_end_time) {
160 valid_periods.emplace_back(*overall_start_time, *overall_end_time);
161
162 for (auto const valid_period_xml : validity_xml.children("com:validPeriod")) {
163 auto const start_of_period = parse_timestamp(valid_period_xml.child_value("com:startOfPeriod"));
164 auto const end_of_period = parse_timestamp(valid_period_xml.child_value("com:endOfPeriod"));
165 if (start_of_period && end_of_period && *start_of_period < *end_of_period) {
166 valid_periods.emplace_back(*start_of_period, *end_of_period);
167 }
168 }
169 for (auto const exception_period_xml : validity_xml.children("com:exceptionPeriod")) {
170 auto const start_of_period = parse_timestamp(exception_period_xml.child_value("com:startOfPeriod"));
171 auto const end_of_period = parse_timestamp(exception_period_xml.child_value("com:endOfPeriod"));
172 if (start_of_period && end_of_period && *start_of_period < *end_of_period) {
173 exception_periods.emplace_back(*start_of_period, *end_of_period);
174 }
175 }
176
177 validity = time::period_seq{valid_periods.begin(), valid_periods.end()}
178 .except(time::period_seq{exception_periods.begin(), exception_periods.end()});
179 } else {
180 warnings_.insert(std::format("invalid overall start / end time (start time: {}, end time: {})",
181 validity_spec_xml.child_value("com:overallStartTime"),
182 validity_spec_xml.child_value("com:overallEndTime")));
183 return std::nullopt;
184 }
185 }
186
187 //---- Try to extract the location info
188
189 auto rc = std::make_shared<road_closure>(std::move(parent), validity);
190 add_location_from_xml(*rc, record_xml.child("sit:locationReference"));
191 return rc;
192 }
193
194 public:
195 [[nodiscard]] auto load_situation_publication(std::string const& filename) -> situation_publication {
196 auto doc = pugi::xml_document{};
197 if (auto result = doc.load_file(filename.c_str()); !result) {
198 throw std::runtime_error{result.description()};
199 }
200 auto payload_xml = doc.child("mc:messageContainer").child("mc:payload");
201 auto mpublication_time = parse_timestamp(payload_xml.child_value("com:publicationTime"));
202 if (!mpublication_time)
203 throw std::runtime_error{"provided publication does not name publication time"};
204
205 auto situations = std::vector<std::shared_ptr<situation>>{};
206 for (auto const sit_xml : payload_xml.children("sit:situation")) {
207 auto id = std::string_view{sit_xml.attribute("id").value()};
208
209 auto const sit = std::make_shared<situation>(std::string{id});
210 situations.push_back(sit);
211
212 auto const& header_info_xml = sit_xml.child("sit:headerInformation");
213 if (header_info_xml.child_value("com:informationStatus") != "real"sv)
214 continue;
215
216 for (auto const record_xml : sit_xml.children("sit:situationRecord")) {
217 auto const record_type = std::string_view{record_xml.attribute("xsi:type").value()};
218 auto const primary_record_types = std::unordered_set<std::string_view>{
219 "sit:Roadworks",
220 /* { */ "sit:MaintenanceWorks",
221 /* | */ "sit:ConstructionWorks",
222 /* } */
223 "sit:Obstruction",
224 /* { */ "sit:EnvironmentalObstruction",
225 /* | */ "sit:GeneralObstruction",
226 /* | */ "sit:InfrastructureDamageObstruction",
227 /* } */
228 "sit:Activity",
229 /* { */ "sit:PublicEvent",
230 /* } */
231 };
232
233 if (record_type == "sit:RoadOrCarriagewayOrLaneManagement") {
234 if (auto rc = handle_road_or_carriageway_or_lane_management(record_xml, sit)) {
235 sit->road_closures.push_back(*rc);
236 }
237 } else if (primary_record_types.contains(record_type)) {
238 for (auto const comment_xml : record_xml.children("sit:generalPublicComment")) {
239// if (comment_xml.child_value("sit:commentType") == "internalNote"sv) {
240 auto candidate = std::optional<std::pair<std::string_view, std::string_view>>{}; // (text, language)
241 for (auto const comment_value_xml : comment_xml.child("sit:comment").child("com:values").children("com:value")) {
242 if (!candidate ||
243 comment_value_xml.attribute("lang").value() == "nl"sv ||
244 (candidate->second != "nl"sv && comment_value_xml.attribute("lang").value() == "nl"sv)) {
245 candidate = std::make_pair(comment_value_xml.child_value(), comment_value_xml.attribute("lang").value());
246 }
247 }
248 if (candidate) {
249 auto already_present = false;
250 for (auto const& comment : sit->comments)
251 already_present = already_present || comment == candidate->first;
252 if (!already_present) {
253 sit->comments.emplace_back(candidate->first);
254 }
255 }
256// }
257 }
258
259 if (auto const location_ref_xml = record_xml.child("sit:locationReference")) {
260 if (location_ref_xml.attribute("xsi:type").value() == "loc:PointLocation"sv) {
261 if (auto const coords_xml = location_ref_xml.child("loc:pointByCoordinates").child("loc:pointCoordinates")) {
262 auto const mlat = util::parse_double(coords_xml.child_value("loc:latitude"));
263 auto const mlon = util::parse_double(coords_xml.child_value("loc:longitude"));
264 if (mlat && mlon) {
265 // Vaag genoeg zegt NDW dat het hier om WGS 84 gaat:
266 // https://docs.ndw.nu/en/dataformaten/datex2-v3/elementen/locationreferencing/pointCoordinates/
267 // maar heeft het UML-model van DATEX II v3 het over ETRS 89:
268 // https://docs.datex2.eu/_static/data/v3.7/umlmodel/html/EARoot/EA3/EA3/EA5/EA676.htm
269
270 auto const coords_etrs89 = geo::point{*mlon, *mlat};
271 auto coords_wgs84 = geo::point{};
272 etrs89_to_wgs84_.forward(coords_etrs89, coords_wgs84);
273
274 if (!sit->location) {
275 sit->location = coords_wgs84;
276 }
277 }
278 }
279 }
280 }
281 }
282 }
283 }
284
285 return {
286 .publication_time = *mpublication_time,
287 .situations = situations,
288 };
289 }
290
291 [[nodiscard]] auto warnings() const -> std::multiset<std::string> const& {
292 return warnings_;
293 }
294 };
295
296} // namespace routemon::datex2
diff --git a/server/src/geo.cppm b/server/src/geo.cppm
new file mode 100644
index 0000000..5cdbdd9
--- /dev/null
+++ b/server/src/geo.cppm
@@ -0,0 +1,40 @@
1module;
2
3#include <boost/geometry.hpp>
4
5export module routemon:geo;
6
7export namespace bgeo = boost::geometry;
8
9export namespace routemon::geo {
10
11 using point = bgeo::model::point<double, 2, bgeo::cs::spherical_equatorial<bgeo::degree>>;
12 using linestring = bgeo::model::linestring<point>;
13 using box = bgeo::model::box<point>;
14 using stype = bgeo::srs::spheroid<double>;
15 using vincenty_strategy = bgeo::strategy::distance::vincenty<stype>;
16
17 auto split_linestring_with_overlap_segments(linestring const& ls, double max_split_distance_m, std::vector<linestring>& append_to) -> void {
18 if (bgeo::is_empty(ls))
19 return;
20
21 auto current_ls = linestring{};
22 auto current_ls_length = 0.0;
23 auto previous = std::optional<point>{};
24 bgeo::for_each_point(ls, [&](point p) -> void {
25 bgeo::append(current_ls, p);
26 if (previous) {
27 auto d = bgeo::distance(*previous, p, vincenty_strategy());
28 current_ls_length += d;
29 if (current_ls_length > max_split_distance_m) {
30 append_to.push_back(std::move(current_ls));
31 current_ls = linestring{*previous, p};
32 current_ls_length = d;
33 }
34 }
35 previous = p;
36 });
37 append_to.emplace_back(std::move(current_ls));
38 }
39
40} // namespace routemon::geo
diff --git a/server/src/gpx.cpp b/server/src/gpx.cpp
new file mode 100644
index 0000000..62dccff
--- /dev/null
+++ b/server/src/gpx.cpp
@@ -0,0 +1,189 @@
1module;
2
3#include <boost/geometry/algorithms/append.hpp>
4
5module routemon:gpx$impl;
6
7import std;
8import :gpx;
9import :util;
10import :xml;
11
12using namespace std::literals::string_view_literals;
13
14namespace routemon::gpx {
15
16 namespace v10 {
17
18 constexpr auto xmlns = "http://www.topografix.com/GPX/1/0"sv;
19 auto qname(std::string_view local) -> xml::qname_view {
20 return {.ns_uri = xmlns, .local = local};
21 }
22
23 auto parse_wpt(xml::executor_ref e, xml::attribute_view attrs) -> xml::parser<geo::point> {
24 auto parse_xml_double = [](std::string_view sv) -> std::optional<double> {
25 return util::parse_double(sv, std::chars_format::fixed);
26 };
27 auto mlat = std::optional<double>{};
28 auto mlon = std::optional<double>{};
29 for (auto const& [name, value] : attrs) {
30 if (name == qname("lat")) {
31 mlat = parse_xml_double(value);
32 } else if (name == qname("lon")) {
33 mlon = parse_xml_double(value);
34 }
35 }
36 if (!mlat || !mlon)
37 throw std::runtime_error{"expected valid latitude and longitude for waypoint"};
38 co_await xml::ignore_contents(e);
39 co_return geo::point{*mlon, *mlat};
40 }
41
42 auto parse_trkseg(xml::executor_ref e, xml::attribute_view) -> xml::parser<track_segment> {
43 auto s = track_segment{};
44 while (auto mwpt = co_await allow_element(e, qname("trkpt"), xml::hohalo<parse_wpt>()))
45 bgeo::append(s.waypoints, *mwpt);
46 co_return std::move(s);
47 }
48
49 auto parse_trk(xml::executor_ref e, xml::attribute_view) -> xml::parser<track> {
50 auto t = track{};
51 t.name = co_await allow_element(e, qname("name"), xml::hohalo<xml::read_string_contents>());
52 co_await allow_element(e, qname("cmt"), xml::hohalo<xml::ignore_element_contents>());
53 t.desc = co_await allow_element(e, qname("desc"), xml::hohalo<xml::read_string_contents>());
54 co_await xml::ignore_contents(e, /* until */ qname("trkseg"));
55 while (auto mseg = co_await allow_element(e, qname("trkseg"), xml::hohalo<parse_trkseg>()))
56 t.segments.push_back(std::move(*mseg));
57 co_return std::move(t);
58 }
59
60 auto parse_gpx(xml::executor_ref e, xml::attribute_view attrs) -> xml::parser<file> {
61 auto f = file{};
62 if (attrs.lookup(qname("version")) != "1.0"sv)
63 throw std::runtime_error{"expected GPX version to be 1.0"};
64 if (auto mcreator = attrs.lookup(qname("creator")))
65 f.creator = *mcreator;
66 else
67 throw std::runtime_error{"expected GPX file to have creator"};
68
69 f.meta.name = co_await allow_element(e, qname("name"), xml::hohalo<xml::read_string_contents>());
70 f.meta.desc = co_await allow_element(e, qname("desc"), xml::hohalo<xml::read_string_contents>());
71
72 co_await xml::ignore_contents(e, /* until */ qname("trk"));
73 while (auto mtrk = co_await allow_element(e, qname("trk"), xml::hohalo<parse_trk>()))
74 f.tracks.push_back(std::move(*mtrk));
75 co_await xml::ignore_contents(e);
76
77 co_return std::move(f);
78 }
79
80 } // namespace v10
81
82 namespace v11 {
83
84 constexpr auto xmlns = "http://www.topografix.com/GPX/1/1"sv;
85 auto qname(std::string_view local) -> xml::qname_view {
86 return {.ns_uri = xmlns, .local = local};
87 }
88
89 auto parse_metadata(xml::executor_ref e, xml::attribute_view) -> xml::parser<metadata> {
90 auto meta = metadata{};
91 meta.name = co_await allow_element(e, qname("name"), xml::hohalo<xml::read_string_contents>());
92 meta.desc = co_await allow_element(e, qname("desc"), xml::hohalo<xml::read_string_contents>());
93 co_await xml::ignore_contents(e);
94 co_return meta;
95 }
96
97 auto parse_wpt(xml::executor_ref e, xml::attribute_view attrs) -> xml::parser<geo::point> {
98 auto parse_xml_double = [](std::string_view sv) -> std::optional<double> {
99 return util::parse_double(sv, std::chars_format::fixed);
100 };
101 auto mlat = std::optional<double>{};
102 auto mlon = std::optional<double>{};
103 for (auto const& [name, value] : attrs) {
104 if (name == qname("lat")) {
105 mlat = parse_xml_double(value);
106 } else if (name == qname("lon")) {
107 mlon = parse_xml_double(value);
108 }
109 }
110 if (!mlat || !mlon)
111 throw std::runtime_error{"expected valid latitude and longitude for waypoint"};
112 co_await xml::ignore_contents(e);
113 co_return geo::point{*mlon, *mlat};
114 }
115
116 auto parse_trkseg(xml::executor_ref e, xml::attribute_view) -> xml::parser<track_segment> {
117 auto s = track_segment{};
118 while (auto mwpt = co_await allow_element(e, qname("trkpt"), xml::hohalo<parse_wpt>()))
119 bgeo::append(s.waypoints, *mwpt);
120 co_await allow_element(e, qname("extensions"), xml::hohalo<xml::ignore_element_contents>());
121 co_return std::move(s);
122 }
123
124 auto parse_trk(xml::executor_ref e, xml::attribute_view) -> xml::parser<track> {
125 auto t = track{};
126 t.name = co_await allow_element(e, qname("name"), xml::hohalo<xml::read_string_contents>());
127 co_await allow_element(e, qname("cmt"), xml::hohalo<xml::ignore_element_contents>());
128 t.desc = co_await allow_element(e, qname("desc"), xml::hohalo<xml::read_string_contents>());
129 co_await xml::ignore_contents(e, /* until */ qname("trkseg"));
130 while (auto mseg = co_await allow_element(e, qname("trkseg"), xml::hohalo<parse_trkseg>()))
131 t.segments.push_back(std::move(*mseg));
132 co_return std::move(t);
133 }
134
135 auto parse_gpx(xml::executor_ref e, xml::attribute_view attrs) -> xml::parser<file> {
136 auto f = file{};
137 if (attrs.lookup(qname("version")) != "1.1"sv)
138 throw std::runtime_error{"expected GPX version to be 1.1"};
139 if (auto mcreator = attrs.lookup(qname("creator")))
140 f.creator = *mcreator;
141 else
142 throw std::runtime_error{"expected GPX file to have creator"};
143
144 if (auto mmeta = co_await allow_element(e, qname("metadata"), xml::hohalo<parse_metadata>()))
145 f.meta = *mmeta;
146 co_await xml::ignore_contents(e, /* until */ qname("trk"));
147 while (auto mtrk = co_await allow_element(e, qname("trk"), xml::hohalo<parse_trk>()))
148 f.tracks.push_back(std::move(*mtrk));
149 co_await allow_element(e, qname("extensions"), xml::hohalo<xml::ignore_element_contents>());
150
151 co_return std::move(f);
152 }
153
154 } // namespace v11
155
156 auto parse_file(xml::executor_ref e) -> xml::parser<file> {
157 auto decl = co_await expect_event<xml::xml_decl_event>(e);
158 if (decl.version != "1.0"sv)
159 throw std::runtime_error{std::format("unsupported XML version, got {}", std::string_view{decl.version})};
160 if (decl.encoding != "UTF-8"sv)
161 throw std::runtime_error{"unsupported encoding"};
162 if (auto mf = co_await allow_element(e, v10::qname("gpx"), xml::hohalo<v10::parse_gpx>()))
163 co_return std::move(*mf);
164 if (auto mf = co_await allow_element(e, v11::qname("gpx"), xml::hohalo<v11::parse_gpx>()))
165 co_return std::move(*mf);
166 throw std::runtime_error{"no supported GPX document found"};
167 }
168
169 reader::reader()
170 : p_{parse_file(util::not_null{&e_})}
171 { e_.set_continuation(p_.promise().base_handle()); }
172
173 auto reader::init() -> void {
174 e_.start();
175 }
176
177 auto reader::put(std::string_view buf) -> void {
178 e_.read(buf, false);
179 }
180
181 auto reader::finish() -> gpx::file {
182 e_.read(std::string_view{}, true);
183 e_.end();
184 // Promise is still alive since the last coroutine performs a
185 // symmetric transfer to std::noop_coroutine() in final_suspend().
186 return std::move(p_.promise().returned_value());
187 }
188
189} // namespace routemon::gpx
diff --git a/server/src/gpx.cppm b/server/src/gpx.cppm
new file mode 100644
index 0000000..20e6242
--- /dev/null
+++ b/server/src/gpx.cppm
@@ -0,0 +1,43 @@
1export module routemon:gpx;
2
3import std;
4import :geo;
5import :util;
6import :xml;
7
8namespace routemon::gpx {
9
10 struct metadata {
11 std::optional<std::string> name;
12 std::optional<std::string> desc;
13 };
14
15 struct track_segment {
16 geo::linestring waypoints;
17 };
18
19 struct track {
20 std::optional<std::string> name;
21 std::optional<std::string> desc;
22 std::vector<track_segment> segments;
23 };
24
25 struct file {
26 std::string creator;
27 metadata meta;
28 std::vector<track> tracks;
29 };
30
31 class reader {
32 xml::executor e_;
33 xml::parser<file> p_;
34
35 public:
36 explicit reader();
37
38 auto init() -> void;
39 auto put(std::string_view buf) -> void;
40 [[nodiscard]] auto finish() -> gpx::file;
41 };
42
43} // namespace routemon::gpx
diff --git a/server/src/http_client.cppm b/server/src/http_client.cppm
new file mode 100644
index 0000000..d5316d6
--- /dev/null
+++ b/server/src/http_client.cppm
@@ -0,0 +1,62 @@
1module;
2
3#include <boost/asio/connect.hpp>
4#include <boost/asio/ip/tcp.hpp>
5#include <boost/asio/ssl.hpp>
6#include <boost/beast/core.hpp>
7#include <boost/beast/http.hpp>
8
9export module routemon:http.client;
10
11export import :http.common;
12
13namespace net = boost::asio;
14namespace ssl = net::ssl;
15using tcp = net::ip::tcp;
16
17namespace routemon::http {
18
19 export class client {
20 net::io_context& ioc_;
21 ssl::context sslc_{ssl::context::tlsv12_client};
22 tcp::resolver resolver_;
23
24 public:
25 explicit client(net::io_context& ioc)
26 : ioc_{ioc}, resolver_{ioc}
27 {
28 sslc_.set_default_verify_paths();
29 sslc_.set_verify_mode(net::ssl::verify_peer | net::ssl::verify_fail_if_no_peer_cert);
30 }
31
32 template<class ReqBody>
33 auto do_request(bhttp::request<ReqBody>& req) -> bhttp::response<bhttp::dynamic_body> {
34 auto stream = ssl::stream<beast::tcp_stream>{ioc_, sslc_};
35
36 auto host = std::string{req.at(bhttp::field::host)};
37 if (!SSL_set_tlsext_host_name(stream.native_handle(), host.c_str())) {
38 throw beast::system_error(static_cast<int>(::ERR_get_error()),
39 net::error::get_ssl_category());
40 }
41 stream.set_verify_callback(ssl::host_name_verification(host));
42 auto const results = resolver_.resolve(host, "443");
43 beast::get_lowest_layer(stream).connect(results);
44 stream.handshake(ssl::stream_base::client);
45
46 req.set(bhttp::field::user_agent, "routemon/1.0");
47 bhttp::write(stream, req);
48
49 auto buffer = beast::flat_buffer{};
50 auto res = bhttp::response<bhttp::dynamic_body>{};
51 bhttp::read(stream, buffer, res);
52
53 auto ec = beast::error_code{};
54 stream.shutdown(ec);
55 if (ec != net::ssl::error::stream_truncated)
56 throw beast::system_error{ec};
57
58 return res;
59 }
60 };
61
62} // namespace routemon::http
diff --git a/server/src/http_common.cppm b/server/src/http_common.cppm
new file mode 100644
index 0000000..3c38da7
--- /dev/null
+++ b/server/src/http_common.cppm
@@ -0,0 +1,139 @@
1module;
2
3#include <boost/beast/core.hpp>
4#include <boost/beast/http.hpp>
5
6export module routemon:http.common;
7
8namespace beast = boost::beast;
9export namespace bhttp = beast::http;
10
11namespace boost::beast {
12
13 namespace concepts {
14
15 template<class T>
16 concept buffers_generator = beast::is_buffers_generator<T>::value;
17
18 template<class T>
19 concept const_buffer_sequence = beast::is_const_buffer_sequence<T>::value;
20
21 } // namespace concepts
22
23 namespace http::concepts {
24
25 template<class T>
26 concept fields = is_fields<T>::value;
27
28 template<class T>
29 concept body = is_body<T>::value;
30
31 template<class T>
32 concept body_reader = is_body_reader<T>::value;
33
34 } // namespace http::concepts
35
36} // namespace boost::beast
37
38namespace routemon::http {
39
40 struct supported_verb {
41 enum supported_verb_t : std::uint8_t {
42 options,
43 delete_,
44 get,
45 head,
46 post,
47 put,
48 };
49
50 supported_verb_t value;
51
52 supported_verb(supported_verb_t value) : value{value} {}
53
54 static auto from(bhttp::verb v) -> std::optional<supported_verb> {
55 switch (v) {
56 case bhttp::verb::options: return supported_verb::options;
57 case bhttp::verb::delete_: return supported_verb::delete_;
58 case bhttp::verb::get: return supported_verb::get;
59 case bhttp::verb::head: return supported_verb::head;
60 case bhttp::verb::post: return supported_verb::post;
61 case bhttp::verb::put: return supported_verb::put;
62 default: return std::nullopt;
63 }
64 }
65
66 operator bhttp::verb() const {
67 switch (value) {
68 case supported_verb::options: return bhttp::verb::options;
69 case supported_verb::delete_: return bhttp::verb::delete_;
70 case supported_verb::get: return bhttp::verb::get;
71 case supported_verb::head: return bhttp::verb::head;
72 case supported_verb::post: return bhttp::verb::post;
73 case supported_verb::put: return bhttp::verb::put;
74 }
75 }
76 };
77
78 export struct verb_set {
79 bool delete_ : 1 = false;
80 bool get : 1 = false;
81 bool head : 1 = false;
82 bool post : 1 = false;
83 bool put : 1 = false;
84 bool options : 1 = false;
85
86 auto enable(supported_verb v) -> void {
87 switch (v.value) {
88 case supported_verb::delete_:
89 delete_ = true;
90 break;
91 case supported_verb::get:
92 get = true;
93 break;
94 case supported_verb::head:
95 head = true;
96 break;
97 case supported_verb::post:
98 post = true;
99 break;
100 case supported_verb::put:
101 put = true;
102 break;
103 case supported_verb::options:
104 options = true;
105 break;
106 default:;
107 }
108 }
109
110 auto operator==(verb_set const& rhs) const noexcept -> bool = default;
111
112 auto empty() const -> bool {
113 return *this == verb_set{};
114 }
115
116 verb_set(std::initializer_list<supported_verb> vs) {
117 for (auto const v : vs) enable(v);
118 }
119
120 auto to_string() const -> std::string {
121 std::ostringstream ss;
122 bool wrote = false;
123 auto write = [&](bhttp::verb v) {
124 if (wrote)
125 ss << ", ";
126 ss << v;
127 wrote = true;
128 };
129 if (delete_) write(bhttp::verb::delete_);
130 if (get) write(bhttp::verb::get);
131 if (head) write(bhttp::verb::head);
132 if (post) write(bhttp::verb::post);
133 if (put) write(bhttp::verb::put);
134 if (options) write(bhttp::verb::options);
135 return ss.str();
136 }
137 };
138
139} // namespace routemon::http
diff --git a/server/src/http_server.cppm b/server/src/http_server.cppm
new file mode 100644
index 0000000..0770d97
--- /dev/null
+++ b/server/src/http_server.cppm
@@ -0,0 +1,661 @@
1module;
2
3#include <boost/config.hpp>
4#include <boost/asio/as_tuple.hpp>
5#include <boost/asio/awaitable.hpp>
6#include <boost/asio/co_spawn.hpp>
7#include <boost/asio/ip/tcp.hpp>
8#include <boost/beast/core.hpp>
9#include <boost/beast/http.hpp>
10#include <boost/json/serialize.hpp>
11#include <boost/url.hpp>
12
13export module routemon:http.server;
14
15import std;
16import :config;
17import :trace;
18export import :http.common;
19import :problem;
20
21namespace net = boost::asio;
22using tcp = net::ip::tcp;
23
24namespace routemon::http {
25
26 struct readable_request {
27 util::not_null<bhttp::request_parser<bhttp::empty_body>*> p;
28 util::not_null<beast::tcp_stream*> strm;
29 util::not_null<beast::flat_buffer*> buf;
30 };
31
32 class presponse {
33 public:
34 using const_buffers_type = beast::span<net::const_buffer>;
35
36 private:
37 struct impl_base {
38 virtual ~impl_base() = default;
39 virtual auto header() -> bhttp::response_header<bhttp::fields>& = 0;
40 virtual auto header() const -> bhttp::response_header<bhttp::fields> const& = 0;
41 virtual auto is_done() const -> bool = 0;
42 virtual auto prepare(beast::error_code&) -> const_buffers_type = 0;
43 virtual auto consume(std::size_t n) -> void = 0;
44 virtual auto keep_alive() const -> bool = 0;
45 };
46 std::unique_ptr<impl_base> impl_;
47
48 template<bhttp::concepts::body Body>
49 class impl : public impl_base {
50 // Initializes in the response state.
51 // At the first call to prepare, we switch to the message generator state.
52 // After that point, header may not be called anymore (it will throw).
53 std::variant<bhttp::response<Body>, bhttp::message_generator> state_;
54
55 auto ensure_message_generator() -> bhttp::message_generator& {
56 if (auto prsp = std::get_if<bhttp::response<Body>>(&state_)) {
57 auto rsp = bhttp::response<Body>{std::move(*prsp)};
58 state_.template emplace<bhttp::message_generator>(std::move(rsp));
59 }
60 return std::get<bhttp::message_generator>(state_);
61 }
62
63 public:
64 explicit impl(bhttp::response<Body>&& rsp) : state_{std::move(rsp)} {}
65
66 auto header() -> bhttp::response_header<bhttp::fields>& override {
67 if (auto prsp = std::get_if<bhttp::response<Body>>(&state_)) {
68 return prsp->base();
69 } else {
70 // TODO: define custom exception type presponse::bad_header_access
71 throw std::logic_error{"header() may not be called after prepare()"};
72 }
73 }
74 auto header() const -> bhttp::response_header<bhttp::fields> const& override {
75 if (auto prsp = std::get_if<bhttp::response<Body>>(&state_)) {
76 return prsp->base();
77 } else {
78 throw std::logic_error{"header() may not be called after prepare()"};
79 }
80 }
81
82 auto is_done() const -> bool override {
83 if (auto pgen = std::get_if<bhttp::message_generator>(&state_)) {
84 return pgen->is_done();
85 } else /* still in the response state */ {
86 return false;
87 }
88 }
89
90 auto prepare(beast::error_code& ec) -> const_buffers_type override {
91 return ensure_message_generator().prepare(ec);
92 }
93
94 auto consume(std::size_t n) -> void override {
95 ensure_message_generator().consume(n);
96 }
97
98 auto keep_alive() const noexcept -> bool override {
99 return state_.visit(util::overloaded{
100 [](bhttp::response<Body> const& rsp) -> bool {
101 return rsp.keep_alive();
102 },
103 [](bhttp::message_generator const& gen) -> bool {
104 return gen.keep_alive();
105 },
106 });
107 }
108 };
109
110 public:
111 template<bhttp::concepts::body Body>
112 explicit presponse(bhttp::response<Body>&& rsp)
113 : impl_{new impl{std::move(rsp)}}
114 {}
115
116 auto header() -> bhttp::response_header<bhttp::fields>& {
117 return impl_->header();
118 }
119 auto header() const -> bhttp::response_header<bhttp::fields> const& {
120 return impl_->header();
121 }
122
123 auto is_done() const -> bool {
124 return impl_->is_done();
125 }
126
127 auto prepare(beast::error_code& ec) -> const_buffers_type {
128 return impl_->prepare(ec);
129 }
130
131 auto consume(std::size_t n) -> void {
132 return impl_->consume(n);
133 }
134
135 auto keep_alive() const noexcept -> bool {
136 return impl_->keep_alive();
137 }
138 };
139 static_assert(beast::concepts::buffers_generator<presponse>);
140
141 template<class Ctx>
142 using next_handler_t = std::function<auto(Ctx) -> net::awaitable<presponse>>;
143
144 template<class OuterCtx, class InnerCtx>
145 using middleware_t = std::function<auto(OuterCtx, bhttp::request_header<bhttp::fields>&, next_handler_t<InnerCtx>) -> net::awaitable<presponse>>;
146
147 template<class Ctx>
148 auto lax_cors_middleware(Ctx ctx, bhttp::request_header<bhttp::fields>& req_hdr, next_handler_t<Ctx> next) -> net::awaitable<presponse> {
149 std::ignore = req_hdr;
150 auto prersp = co_await next(ctx);
151 prersp.header().set(bhttp::field::access_control_allow_origin, "*");
152 co_return std::move(prersp);
153 }
154
155 template<class InnerCtx>
156 struct trace_id_ctx : InnerCtx {
157 trace::id trace_id = {};
158 };
159
160 template<class OuterCtx>
161 auto trace_id_middleware(OuterCtx ctx0, bhttp::request_header<bhttp::fields>& req_hdr, next_handler_t<trace_id_ctx<OuterCtx>> next) -> net::awaitable<presponse> {
162 std::ignore = req_hdr;
163 auto ctx = trace_id_ctx{std::move(ctx0)};
164 auto prersp = co_await next(std::move(ctx));
165 prersp.header().set("X-Routemon-Trace-Id", std::string_view{ctx.trace_id.as_string()});
166 prersp.header().insert(bhttp::field::access_control_expose_headers, "X-Routemon-Trace-Id");
167 co_return std::move(prersp);
168 }
169
170 struct base_ctx {
171 std::locale locale;
172 };
173
174 template<class Ctx>
175 using basic_route_handler_fn_t = std::function<auto(Ctx, readable_request, std::vector<std::string> const& matches) -> net::awaitable<presponse>>;
176
177 struct keep_alive {
178 bool value;
179
180 explicit keep_alive(bool value) : value{value} {}
181 };
182
183 template<bhttp::concepts::body Body>
184 auto make_rsp(bhttp::status status, keep_alive ka) -> bhttp::response<Body> {
185 auto rsp = bhttp::response<Body>{}; // HTTP version gets set later
186 rsp.result(status);
187 rsp.keep_alive(ka.value);
188 return rsp;
189 }
190
191 auto problem_rsp(base_ctx const& ctx, problem::details const& problem, keep_alive ka) -> presponse {
192 auto rsp = make_rsp<bhttp::string_body>(problem.status, ka);
193 rsp.set(bhttp::field::content_type, "application/problem+json");
194 rsp.body() = json::serialize(json::value_from(problem, ctx.locale));
195 rsp.prepare_payload();
196 return presponse{std::move(rsp)};
197 }
198
199 struct preflight_response {
200 verb_set allow_methods;
201 std::vector<bhttp::field> allow_headers;
202 };
203 auto make_preflight_rsp(preflight_response res, keep_alive ka) -> bhttp::response<bhttp::empty_body> {
204 auto rsp = make_rsp<bhttp::empty_body>(bhttp::status::no_content, ka);
205 auto allow_headers_str = res.allow_headers
206 | std::views::transform([](auto const& field) -> std::string_view { return bhttp::to_string(field); })
207 | std::views::join_with(std::string_view{", "})
208 | std::ranges::to<std::string>();
209 rsp.set(bhttp::field::access_control_allow_methods, res.allow_methods.to_string());
210 rsp.set(bhttp::field::access_control_allow_headers, allow_headers_str);
211 rsp.prepare_payload();
212 return rsp;
213 }
214
215 // Using base_ctx instead of a template here since that saves you
216 // typing on invocation (and we do not care about the context type
217 // anyway, but all context types should derive from base_ctx).
218 template<bhttp::concepts::body_reader Body>
219 auto read_request(base_ctx const& ctx, readable_request&& r) -> net::awaitable<std::expected<bhttp::request<Body>, presponse>> {
220 std::ignore = ctx;
221 auto p = bhttp::request_parser<Body>{std::move(*r.p)};
222 co_await bhttp::async_read(*r.strm, *r.buf, p);
223 co_return std::move(p.release());
224 }
225
226 template<>
227 auto read_request<bhttp::empty_body>(base_ctx const& ctx, readable_request&& r) -> net::awaitable<std::expected<bhttp::request<bhttp::empty_body>, presponse>> {
228 auto [ec, _] = co_await bhttp::async_read(*r.strm, *r.buf, *r.p, net::as_tuple);
229 if (ec == bhttp::error::unexpected_body) {
230 auto tpl = problem::tpl{
231 .status = bhttp::status::bad_request,
232 .title = translate("No body expected for this request"),
233 .type_uri = "https://routemon.fautchen.eu/problems/unexpected-body",
234 };
235 co_return std::unexpected{problem_rsp(ctx, tpl.instantiate(), keep_alive{false})};
236 } else if (ec) {
237 throw boost::system::system_error{ec};
238 }
239 co_return r.p->release();
240 }
241
242 template<class InnerCtx>
243 struct routed_ctx : InnerCtx {
244 verb_set route_methods;
245 };
246
247 template<class Ctx>
248 requires requires(Ctx ctx) {
249 // Ctx must be derived from an instantiation of routed_ctx
250 []<class InnerCtx>(routed_ctx<InnerCtx> const&) {}(ctx);
251 }
252 auto default_options_handler(Ctx const& ctx, readable_request r, std::vector<std::string> const&) -> net::awaitable<presponse> {
253 auto mreq = co_await read_request<bhttp::empty_body>(ctx, std::move(r));
254 if (!mreq)
255 co_return std::move(mreq.error());
256
257 if (mreq->find(bhttp::field::access_control_request_method) != mreq->end()) {
258 // CORS preflight request
259 co_return make_preflight_rsp(preflight_response{
260 // TODO: should access-control-allow-methods contain OPTIONS?
261 .allow_methods = ctx.route_methods,
262 .allow_headers = {bhttp::field::content_type},
263 }, keep_alive{mreq->keep_alive()});
264 } else {
265 // Normal OPTIONS request
266 auto rsp = make_rsp<bhttp::empty_body>(bhttp::status::no_content, keep_alive{mreq->keep_alive()});
267 rsp.set(bhttp::field::allow, ctx.route_methods.to_string());
268 rsp.prepare_payload();
269 co_return std::move(rsp);
270 }
271 }
272
273 auto global_options_handler(base_ctx const& ctx, readable_request r) -> net::awaitable<presponse> {
274 // TODO: switch to "small (4KB) discarded" body type, similar to what Go does?
275 // Same goes for default_options_handler? Not sure.
276 if (auto res = co_await read_request<bhttp::empty_body>(ctx, std::move(r)); !res)
277 co_return std::move(res.error());
278 auto req = r.p->release();
279 auto rsp = make_rsp<bhttp::empty_body>(bhttp::status::no_content, keep_alive{req.keep_alive()});
280 rsp.prepare_payload();
281 co_return std::move(rsp);
282 }
283
284 template<class Ctx>
285 auto id_middleware(Ctx ctx, bhttp::request_header<bhttp::fields>&, next_handler_t<Ctx> next) -> net::awaitable<presponse> {
286 co_return co_await next(std::move(ctx));
287 }
288
289 template<class A, class B, class C>
290 auto middleware_compose(middleware_t<A, B> ab, middleware_t<B, C> bc) -> middleware_t<A, C> {
291 return [ab = std::move(ab), bc = std::move(bc)](A a, bhttp::request_header<bhttp::fields>& header, next_handler_t<C> next) -> net::awaitable<presponse> {
292 co_return co_await ab(std::move(a), header, [&](B b) -> net::awaitable<presponse> {
293 co_return co_await bc(std::move(b), header, next);
294 });
295 };
296 }
297
298 template<class A, class B>
299 auto middleware_wrap_fn(middleware_t<A, B> ab, basic_route_handler_fn_t<B> fn) -> basic_route_handler_fn_t<A> {
300 return [ab = std::move(ab), fn = std::move(fn)](A a_ctx, readable_request r, std::vector<std::string> const& matches) -> net::awaitable<presponse> {
301 co_return co_await ab(std::move(a_ctx), r.p->get().base(), [&](B b_ctx) -> net::awaitable<presponse> {
302 co_return co_await fn(std::move(b_ctx), r, matches);
303 });
304 };
305 }
306
307 template<std::default_initializable V>
308 requires requires(V v) {
309 { static_cast<bool>(v) };
310 }
311 struct handler_map {
312 V options = {};
313 V delete_ = {};
314 V get = {};
315 V head = {};
316 V post = {};
317 V put = {};
318
319 template<class Self>
320 auto lookup(this Self&& self, supported_verb v) -> auto&& {
321 switch (v.value) {
322 case supported_verb::options: return std::forward<Self>(self).options;
323 case supported_verb::delete_: return std::forward<Self>(self).delete_;
324 case supported_verb::get: return std::forward<Self>(self).get;
325 case supported_verb::head: return std::forward<Self>(self).head;
326 case supported_verb::post: return std::forward<Self>(self).post;
327 case supported_verb::put: return std::forward<Self>(self).put;
328 }
329 }
330
331 auto verbs() const -> verb_set {
332 auto set = verb_set{};
333 if (static_cast<bool>(options))
334 set.enable(supported_verb::options);
335 if (static_cast<bool>(delete_))
336 set.enable(supported_verb::delete_);
337 if (static_cast<bool>(get))
338 set.enable(supported_verb::get);
339 if (static_cast<bool>(head))
340 set.enable(supported_verb::head);
341 if (static_cast<bool>(post))
342 set.enable(supported_verb::post);
343 if (static_cast<bool>(put))
344 set.enable(supported_verb::put);
345 return set;
346 }
347
348 auto empty() const -> bool {
349 return verbs().empty();
350 }
351
352 template<std::default_initializable U>
353 auto map(std::invocable<V const&> auto f) const -> handler_map<U>
354 requires std::assignable_from<U&, std::invoke_result_t<decltype(f), V const&>>
355 {
356 return {
357 .options = static_cast<bool>(options) ? f(options) : U{},
358 .delete_ = static_cast<bool>(delete_) ? f(delete_) : U{},
359 .get = static_cast<bool>(get) ? f(get) : U{},
360 .head = static_cast<bool>(head) ? f(head) : U{},
361 .post = static_cast<bool>(post) ? f(post) : U{},
362 .put = static_cast<bool>(put) ? f(put) : U{},
363 };
364 }
365 };
366
367 template<class Ctx>
368 struct route_tree {
369 using leaves = handler_map<basic_route_handler_fn_t<Ctx>>;
370 using named_subtrees = std::unordered_map<std::string, route_tree>;
371 using wildcard_subtree = std::indirect<route_tree>;
372
373 leaves here;
374 // TODO: consider making the first alternative a radix tree
375 // Note: the map is the first variant here; the variant will be
376 // default-constructed with the default-constructed first
377 // alternative. The empty map denotes a lack of subtrees.
378 std::variant<named_subtrees, wildcard_subtree> sub;
379 };
380
381 template<class OuterCtx, class InnerCtx>
382 auto middleware_wrap_tree(middleware_t<OuterCtx, InnerCtx> mw, route_tree<InnerCtx> const& tree) -> route_tree<OuterCtx> {
383 auto new_leaves = tree.here.template map<basic_route_handler_fn_t<OuterCtx>>(std::bind_front(middleware_wrap_fn<OuterCtx, InnerCtx>, mw));
384 auto new_sub = tree.sub.visit(util::overloaded{
385 [&mw](route_tree<InnerCtx>::named_subtrees const& subtrees) -> decltype(route_tree<OuterCtx>::sub) {
386 auto new_subtrees = typename route_tree<OuterCtx>::named_subtrees{};
387 for (auto [seg, subtree] : subtrees)
388 new_subtrees[seg] = middleware_wrap_tree(mw, subtree);
389 return new_subtrees;
390 },
391 [&mw](route_tree<InnerCtx>::wildcard_subtree const& subtree) -> decltype(route_tree<OuterCtx>::sub) {
392 return typename route_tree<OuterCtx>::wildcard_subtree{middleware_wrap_tree(mw, *subtree)};
393 },
394 });
395 return {.here = new_leaves, .sub = new_sub};
396 }
397
398 template<class T>
399 concept match_arg = std::constructible_from<T, std::string const&>;
400
401 template<class Ctx, match_arg... MatchArgs>
402 using route_handler_fn_t = std::function<auto(Ctx, readable_request, MatchArgs...) -> net::awaitable<presponse>>;
403
404 template<class Ctx, match_arg... MatchArgs>
405 auto degen_route_handler(route_handler_fn_t<Ctx, MatchArgs...> fn) -> basic_route_handler_fn_t<Ctx> {
406 return [fn = std::move(fn)](Ctx ctx, readable_request r, std::vector<std::string> const& matches) -> net::awaitable<presponse> {
407 if (sizeof...(MatchArgs) != matches.size())
408 throw std::runtime_error{"got unexpected amount of matches"};
409 auto it = matches.begin();
410 co_return co_await fn(std::move(ctx), r, MatchArgs{static_cast<std::string const&>(*it++)}...);
411 };
412 }
413
414 template<class Ctx, match_arg... MatchArgs>
415 struct ctree : route_tree<Ctx> {
416 template<class OuterCtx>
417 auto wrap(middleware_t<OuterCtx, Ctx> mw) const -> ctree<OuterCtx, MatchArgs...> {
418 return {middleware_wrap_tree(std::move(mw), *this)};
419 }
420 };
421
422 template<class Ctx, match_arg... MatchArgs>
423 struct dtree : handler_map<route_handler_fn_t<Ctx, MatchArgs...>> {
424 [[nodiscard]] auto to_leaves() const -> typename route_tree<Ctx>::leaves {
425 auto here = this->template map<basic_route_handler_fn_t<Ctx>>(degen_route_handler<Ctx, MatchArgs...>);
426 if (!here.verbs().empty() && !static_cast<bool>(this->options))
427 here.options = default_options_handler<Ctx>;
428 return here;
429 }
430
431 [[nodiscard]] auto named_subtrees(std::initializer_list<std::pair<std::string, ctree<Ctx, MatchArgs...>>> subtrees) const -> ctree<Ctx, MatchArgs...> {
432 auto sub = typename route_tree<Ctx>::named_subtrees{
433 std::from_range,
434 subtrees | std::views::transform([](auto const& p) {
435 return std::make_pair(p.first, static_cast<route_tree<Ctx>>(p.second));
436 })
437 };
438 return {route_tree<Ctx>{.here = to_leaves(), .sub = sub}};
439 }
440
441 template<match_arg MatchArg>
442 [[nodiscard]] auto wildcard_subtree(ctree<Ctx, MatchArgs..., MatchArg> subtree) -> ctree<Ctx, MatchArgs...> {
443 return {route_tree<Ctx>{.here = to_leaves(), .sub = typename route_tree<Ctx>::wildcard_subtree{static_cast<route_tree<Ctx>>(subtree)}}};
444 }
445
446 [[nodiscard]] auto no_subtrees() const -> ctree<Ctx, MatchArgs...> {
447 return {route_tree<Ctx>{.here = to_leaves(), .sub = {}}};
448 }
449 };
450
451 template<std::derived_from<base_ctx> PreRouteCtx>
452 class server {
453 log::logger l_;
454 locale::selector lsel_;
455 middleware_t<base_ctx, PreRouteCtx> global_middleware_;
456 route_tree<routed_ctx<PreRouteCtx>> routes_;
457
458 public:
459 explicit server(log::logger const& l, locale::selector&& lsel, middleware_t<base_ctx, PreRouteCtx> global_middleware, route_tree<routed_ctx<PreRouteCtx>> routes)
460 : l_{l.sub("http_server")}, lsel_{std::move(lsel)}, global_middleware_{std::move(global_middleware)}, routes_{std::move(routes)}
461 {}
462
463 struct match_result {
464 util::not_null<handler_map<basic_route_handler_fn_t<routed_ctx<PreRouteCtx>>> const*> route_handlers;
465 std::vector<std::string> wildcard_matches;
466
467 auto allowed_methods() const -> verb_set {
468 return route_handlers->verbs();
469 }
470 };
471
472 auto match(boost::urls::segments_view segments) const -> std::optional<match_result> {
473 auto const* tree = &routes_;
474 auto wildcard_matches = std::vector<std::string>{};
475 for (auto const& seg : segments) {
476 tree->sub.visit(util::overloaded{
477 [&](route_tree<routed_ctx<PreRouteCtx>>::named_subtrees const& subtrees) {
478 auto it = subtrees.find(seg);
479 tree = it == subtrees.end() ? nullptr : &it->second;
480 },
481 [&](route_tree<routed_ctx<PreRouteCtx>>::wildcard_subtree const& wildcard_subtree) {
482 wildcard_matches.push_back(seg);
483 tree = &*wildcard_subtree;
484 },
485 });
486 if (!tree) return std::nullopt;
487 }
488 if (tree->here.empty()) return std::nullopt;
489 return match_result{
490 .route_handlers = util::not_null{&tree->here},
491 .wildcard_matches = wildcard_matches,
492 };
493 }
494
495 auto route_request(PreRouteCtx ctx, readable_request r) const -> net::awaitable<presponse> {
496 auto req_base = r.p->get().base();
497
498 auto const bad_request_tpl = problem::tpl{
499 .status = bhttp::status::bad_request,
500 .title = translate("Bad request"),
501 .type_uri = "https://routemon.fautchen.eu/problems/bad-request",
502 };
503
504 if (req_base.target() == "*") {
505 // request-target is in asterisk-form (RFC 9112, § 3.2.4),
506 // so the request must be a server-wide OPTIONS request.
507
508 if (req_base.method() != bhttp::verb::options) {
509 auto tpl = problem::tpl{
510 .status = bhttp::status::method_not_allowed,
511 .title = translate("Method not allowed"),
512 .type_uri = "https://routemon.fautchen.eu/problems/method-not-allowed",
513 };
514 co_return problem_rsp(ctx, tpl.instantiate(), keep_alive{false});
515 }
516
517 co_return co_await global_options_handler(ctx, r);
518 } else if (auto mreq_url0 = boost::urls::parse_origin_form(req_base.target())) {
519 // request-target is in origin-form (RFC 9112, § 3.2.1),
520 // so it must be a normal request (not a CONNECT or
521 // server-wide OPTIONS request).
522
523 auto req_url = boost::urls::url{*mreq_url0};
524 req_url.normalize();
525 if (!req_url.is_path_absolute()) {
526 auto problem = bad_request_tpl.instantiate().
527 set_detail(translate("Path of normalized (RFC 3986, § 6) "
528 "origin-form request-target (RFC "
529 "9112, § 3.2.1) should be "
530 "absolute"));
531 co_return problem_rsp(ctx, problem, keep_alive{false});
532 }
533
534 auto mres = match(req_url.segments());
535 if (!mres) {
536 auto tpl = problem::tpl{
537 .status = bhttp::status::not_found,
538 .title = translate("Not found"),
539 .type_uri = "https://routemon.fautchen.eu/problems/not-found",
540 };
541 co_return problem_rsp(ctx, tpl.instantiate(), keep_alive{false});
542 }
543
544 auto mverb = supported_verb::from(req_base.method());
545 if (!mverb) {
546 // Method not implemented.
547 auto tpl = problem::tpl{
548 .status = bhttp::status::not_implemented,
549 .title = translate("Method not implemented"),
550 .type_uri = "https://routemon.fautchen.eu/problems/method-not-implemented",
551 };
552 co_return problem_rsp(ctx, tpl.instantiate(), keep_alive{false});
553 }
554
555 if (auto mhdl = mres->route_handlers->lookup(*mverb)) {
556 auto new_ctx = routed_ctx<PreRouteCtx>{std::move(ctx), mres->allowed_methods()};
557 co_return co_await mhdl(std::move(new_ctx), r, mres->wildcard_matches);
558 } else {
559 // Path recognized, but method not allowed.
560 auto tpl = problem::tpl{
561 .status = bhttp::status::method_not_allowed,
562 .title = translate("Method not allowed"),
563 .type_uri = "https://routemon.fautchen.eu/problems/method-not-allowed",
564 };
565 auto rsp = problem_rsp(ctx, tpl.instantiate(), keep_alive{false});
566 rsp.header().set(bhttp::field::allow, mres->allowed_methods().to_string());
567 co_return std::move(rsp);
568 }
569 } else {
570 // We do not accept any other request-target forms.
571
572 auto problem = bad_request_tpl.instantiate().
573 set_detail(translate("Invalid request-target, expected "
574 "asterisk-form or origin-form "
575 "(see RFC 9112, § 3.2)"));
576 co_return problem_rsp(ctx, problem, keep_alive{false});
577 }
578 }
579
580 auto handle_request(readable_request r) const -> net::awaitable<presponse> {
581 auto header = r.p->get().base();
582 auto locale = lsel_.select(header[bhttp::field::accept_language]);
583 auto ctx0 = base_ctx{.locale = locale};
584
585 co_return co_await global_middleware_(std::move(ctx0), header, [&](PreRouteCtx ctx) -> net::awaitable<presponse> {
586 co_return co_await route_request(std::move(ctx), std::move(r));
587 });
588 }
589
590 auto do_session(beast::tcp_stream strm) -> net::awaitable<void> {
591 auto buf = beast::flat_buffer{};
592
593 while (true) {
594 auto p0 = bhttp::request_parser<bhttp::empty_body>{};
595 p0.body_limit(boost::none);
596 auto [ec, _] = co_await bhttp::async_read_header(strm, buf, p0, net::as_tuple);
597 if (ec == bhttp::error::end_of_stream) {
598 break;
599 } else if (ec) {
600 throw boost::system::system_error{ec};
601 }
602
603 auto http_version = p0.get().version();
604 auto&& rsp = co_await handle_request(readable_request{
605 .p = util::not_null{&p0},
606 .strm = util::not_null{&strm},
607 .buf = util::not_null{&buf},
608 });
609 rsp.header().version(http_version);
610 bool keep_alive = rsp.keep_alive();
611 co_await beast::async_write(strm, std::move(rsp));
612 if (!keep_alive) {
613 break;
614 }
615 }
616
617 strm.socket().shutdown(tcp::socket::shutdown_send);
618 }
619
620 auto do_listen(tcp::endpoint endpoint) -> net::awaitable<void> {
621 auto executor = co_await net::this_coro::executor;
622 auto acceptor = tcp::acceptor{executor, endpoint};
623
624 l_.with("endpoint", endpoint.address().to_string()).
625 with("port", std::to_string(endpoint.port())).
626 info("Serving");
627 while (true) {
628 net::co_spawn(executor,
629 do_session(beast::tcp_stream{co_await acceptor.async_accept()}),
630 [this](std::exception_ptr e) {
631 if (e) {
632 try {
633 std::rethrow_exception(e);
634 } catch (std::exception const& e) {
635 l_.error("Error in session: {}", e.what());
636 }
637 }
638 });
639 }
640 }
641
642 auto spawn(net::io_context& ioc) -> void {
643 auto const addr = net::ip::make_address("0.0.0.0");
644 auto const endpoint = tcp::endpoint{addr, 8284};
645
646 // TODO: make exception handling as nice as in srv.cpp
647 net::co_spawn(ioc,
648 do_listen(endpoint),
649 [this](std::exception_ptr e) {
650 if (e) {
651 try {
652 std::rethrow_exception(e);
653 } catch (std::exception const& e) {
654 l_.error("Error: {}", e.what());
655 }
656 }
657 });
658 }
659 };
660
661} // namespace routemon::http
diff --git a/server/src/locale.cppm b/server/src/locale.cppm
new file mode 100644
index 0000000..65ae2ea
--- /dev/null
+++ b/server/src/locale.cppm
@@ -0,0 +1,245 @@
1module;
2
3#include <boost/locale.hpp>
4#include <unicode/localematcher.h>
5
6export module routemon:locale;
7
8import std;
9import :util;
10
11export namespace blocale = boost::locale;
12
13export namespace routemon {
14 using lformat = blocale::format;
15 using blocale::translate;
16 using blocale::gettext;
17} // namespace routemon
18
19namespace routemon::locale {
20
21 struct locale_priority {
22 float weight;
23 std::size_t original_index;
24 };
25
26 auto operator<(locale_priority const& lhs, locale_priority const& rhs) -> bool {
27 if (lhs.weight != rhs.weight)
28 return lhs.weight > rhs.weight;
29 return lhs.original_index < rhs.original_index;
30 }
31
32 struct icu_locale_hash {
33 std::size_t operator()(icu::Locale const& l) const noexcept {
34 static_assert(sizeof(std::int32_t) < sizeof(std::size_t));
35 std::int32_t hash = l.hashCode();
36 if (hash < 0) {
37 return static_cast<std::size_t>(std::numeric_limits<int>::max()) + static_cast<std::size_t>(-hash) + 1;
38 } else {
39 return static_cast<std::size_t>(hash);
40 }
41 }
42 };
43
44 using icu_locale_priority_map = std::unordered_map<icu::Locale, locale_priority, icu_locale_hash>;
45 using icu_priority_locale = std::pair<icu::Locale, locale_priority>;
46
47 auto operator<(icu_priority_locale const& lhs, icu_priority_locale const& rhs) -> bool {
48 return lhs.second < rhs.second;
49 }
50
51 class icu_priority_locale_vec_iterator : public icu::Locale::Iterator {
52 std::size_t i_ = 0uz;
53 std::vector<icu_priority_locale> ls_;
54
55 public:
56 explicit icu_priority_locale_vec_iterator(std::vector<icu_priority_locale>&& ls)
57 : ls_(std::move(ls))
58 {}
59
60 auto hasNext() const -> UBool override {
61 return i_ < ls_.size();
62 }
63
64 auto next() -> icu::Locale const& override {
65 return ls_[i_++].first;
66 }
67
68 ~icu_priority_locale_vec_iterator() override = default;
69 };
70
71 export template<class T>
72 concept locale_input_range =
73 std::ranges::input_range<T> &&
74 std::same_as<std::locale const&, std::ranges::range_const_reference_t<T>>;
75
76 // Helps select a locale based on the Accept-Language header in an
77 // HTTP request.
78 export class selector {
79 std::locale default_;
80 icu::LocaleMatcher matcher_;
81 std::shared_ptr<blocale::generator const> lgen_;
82
83 auto make_matcher(locale_input_range auto supported_locales, std::locale default_locale) {
84 auto builder = icu::LocaleMatcher::Builder{};
85 for (auto const& supported_locale : supported_locales) {
86 auto const& supported_locale_info = std::use_facet<blocale::info>(supported_locale);
87 auto supported_icu_locale = icu::Locale{supported_locale_info.name().c_str()};
88 if (supported_icu_locale.isBogus())
89 throw std::runtime_error{"supported locale gives rise to bogus ICU locale"};
90 builder.addSupportedLocale(supported_icu_locale);
91 }
92 auto const& default_locale_info = std::use_facet<blocale::info>(default_locale);
93 auto default_icu_locale = icu::Locale{default_locale_info.name().c_str()};
94 if (default_icu_locale.isBogus())
95 throw std::runtime_error{"default locale gives rise to bogus ICU locale"};
96 builder.setDefaultLocale(&default_icu_locale);
97 auto ec = UErrorCode::U_ZERO_ERROR;
98 auto matcher = builder.build(ec);
99 if (U_FAILURE(ec))
100 throw std::runtime_error{"failed to build icu::LocaleMatcher"};
101 return matcher;
102 }
103
104 // Trimming optional whitespace as defined in RFC 9110, § 12.4.2.
105 static auto ltrim_ows(std::string_view s) -> std::string_view {
106 if (auto i = s.find_first_not_of(" \t"); i != std::string_view::npos)
107 s.remove_prefix(i);
108 return s;
109 }
110 static auto rtrim_ows(std::string_view s) -> std::string_view {
111 if (auto i = s.find_last_not_of(" \t"); i != std::string_view::npos)
112 return s.substr(0, i + 1);
113 return s;
114 }
115 static auto trim_ows(std::string_view s) -> std::string_view {
116 return rtrim_ows(ltrim_ows(s));
117 }
118
119 auto from_icu_locale(icu::Locale const& l) const -> std::locale {
120 auto posix_name = std::string{l.getLanguage()};
121 if (l.getScript() && std::strlen(l.getScript()) > 0) {
122 posix_name += "_";
123 posix_name += l.getScript();
124 }
125 if (l.getCountry() && std::strlen(l.getCountry()) > 0) {
126 posix_name += "_";
127 posix_name += l.getCountry();
128 }
129 posix_name += ".UTF-8";
130 auto added_at = false;
131 if (l.getVariant() && std::strlen(l.getVariant()) > 0) {
132 added_at = true;
133 posix_name += "@";
134 posix_name += l.getVariant();
135 }
136 auto ec = UErrorCode::U_ZERO_ERROR;
137 auto* keywords = l.createKeywords(ec);
138 if (U_FAILURE(ec))
139 throw std::runtime_error{"failed to create keywords"};
140 if (keywords) {
141 std::int32_t kw_len = 0;
142 char const* kw = nullptr;
143 while (kw = keywords->next(&kw_len, ec), !U_FAILURE(ec) && kw) {
144 auto value = l.getKeywordValue<std::string>(icu::StringPiece(kw, kw_len), ec);
145 if (!added_at) {
146 posix_name += "@";
147 added_at = true;
148 } else {
149 posix_name += ";";
150 }
151 posix_name += kw;
152 posix_name += "=";
153 posix_name += value;
154 }
155 if (U_FAILURE(ec))
156 throw std::runtime_error{"failed to iterate over keywords"};
157 delete keywords;
158 }
159 return lgen_->generate(posix_name);
160 }
161
162 public:
163 // Note: lgen must live at least as long as the selector constructed here!
164 // It is unfortunately not possible to copy/move a blocale::generator.
165 explicit selector(locale_input_range auto locales, std::locale default_, std::shared_ptr<blocale::generator const> lgen)
166 : default_{default_}, matcher_{make_matcher(locales, default_)}, lgen_{lgen}
167 {}
168
169 auto select(std::string_view accept_language) const -> std::locale {
170 using namespace std::literals::string_view_literals;
171 // NOTE: can also contain a *;q=0.1
172 // q should have at most 3 digits after period
173 auto dlpm = icu_locale_priority_map{};
174 for (auto const [i, lang_prio] : accept_language | std::views::split(","sv) | std::views::enumerate) {
175 auto [lang_range_ut, mweight_ut] = util::split_on(std::string_view{lang_prio}, ';');
176 auto lang_range_str = trim_ows(lang_range_ut);
177 auto mweight_str = mweight_ut.transform(trim_ows);
178 if (lang_range_str == "*")
179 break;
180
181 auto ec = UErrorCode::U_ZERO_ERROR;
182 auto icu_locale = icu::Locale::forLanguageTag(lang_range_str, ec);
183 if (U_FAILURE(ec) || icu_locale.isBogus())
184 continue; // ignore this locale
185
186 auto weight = 1.0f;
187 if (mweight_str && mweight_str->starts_with("q=")) {
188 auto weight_str = mweight_str->substr(2, 4);
189 if (auto mweight = util::parse_float(weight_str, std::chars_format::fixed);
190 mweight && 0.0f < *mweight && *mweight < 1.0f) {
191 weight = *mweight;
192 }
193 }
194
195 if (weight > 0.0f) {
196 dlpm[icu_locale] = {
197 .weight = weight,
198 .original_index = static_cast<std::size_t>(i),
199 };
200 } else {
201 dlpm.erase(icu_locale);
202 }
203 }
204
205 auto desired_locales = std::vector<icu_priority_locale>{dlpm.begin(), dlpm.end()};
206 std::sort(desired_locales.begin(), desired_locales.end());
207 auto it = icu_priority_locale_vec_iterator{std::move(desired_locales)};
208 auto ec = UErrorCode::U_ZERO_ERROR;
209 auto res = matcher_.getBestMatchResult(it, ec);
210 if (U_FAILURE(ec))
211 return default_;
212 auto resolved = res.makeResolvedLocale(ec); // TODO: maybe don't?
213 if (U_FAILURE(ec))
214 return from_icu_locale(*res.getSupportedLocale());
215 return from_icu_locale(resolved);
216 }
217 };
218
219 export auto to_bcp47_lang_tag(std::locale locale) -> std::optional<std::string> {
220 auto const& locale_info = std::use_facet<blocale::info>(locale);
221 auto ec = UErrorCode::U_ZERO_ERROR;
222 auto bcp47_lang_tag = icu::Locale{locale_info.name().c_str()}.toLanguageTag<std::string>(ec);
223 if (U_FAILURE(ec))
224 return std::nullopt;
225 return bcp47_lang_tag;
226 }
227
228#ifdef LOCALEDIR
229# define LOCALEDIR_AUX_XSTR(s) LOCALEDIR_AUX_STR(s)
230# define LOCALEDIR_AUX_STR(s) #s
231 constexpr auto messages_path = std::string_view{LOCALEDIR_AUX_XSTR(LOCALEDIR)};
232# undef LOCALEDIR_AUX_STR
233# undef LOCALEDIR_AUX_XSTR
234#else // ifdef LOCALEDIR
235 constexpr auto messages_path = std::string_view{"locale/dev"};
236#endif // ifdef LOCALEDIR
237
238 export auto make_generator() -> std::shared_ptr<blocale::generator const> {
239 auto lgen = std::make_shared<blocale::generator>();
240 lgen->add_messages_path(std::string{messages_path});
241 lgen->add_messages_domain("routemon");
242 return std::static_pointer_cast<blocale::generator const>(lgen);
243 }
244
245} // namespace routemon::locale
diff --git a/server/src/log.cppm b/server/src/log.cppm
new file mode 100644
index 0000000..d7e2bff
--- /dev/null
+++ b/server/src/log.cppm
@@ -0,0 +1,148 @@
1module;
2
3// Seems like ADL for std::quoted is broken with
4// import std;
5// Might be because the _Quoted_string object is defined in
6// std::__detail, which is not exported by the module.
7#include <iomanip>
8
9export module routemon:log;
10
11import std;
12
13namespace routemon::log {
14
15 export enum class level : std::uint8_t {
16 debug,
17 info,
18 warn,
19 error,
20 };
21
22 namespace {
23
24 auto operator<<(std::ostream& os, level lvl) -> std::ostream& {
25 switch (lvl) {
26 case level::debug: os << "dbg"; break;
27 case level::info: os << "inf"; break;
28 case level::warn: os << "wrn"; break;
29 case level::error: os << "err"; break;
30 }
31 return os;
32 }
33
34 } // namespace (unique)
35
36 export class sink {
37 std::atomic<enum level> lvl_;
38 std::ostream& os_ = std::cout;
39
40 struct tmp_message {
41 level lvl;
42 std::string_view component;
43 std::string_view txt;
44 std::map<std::string, std::string> const& attrs;
45 };
46
47 auto write(tmp_message msg) -> void {
48 auto sos = std::osyncstream{os_};
49 sos << "[" << msg.lvl;
50 if (!msg.component.empty())
51 sos << " " << msg.component;
52 sos << "] " << msg.txt;
53 for (auto const& [k, v] : msg.attrs) {
54 sos << " " << k << "=" << std::quoted(v);
55 }
56 sos << '\n';
57 }
58
59 explicit sink(level lvl)
60 : lvl_{lvl}
61 {}
62
63 friend auto make_sink(level lvl) -> std::shared_ptr<sink>;
64 friend class logger;
65
66 public:
67 [[nodiscard]] auto level() const -> enum level {
68 return lvl_;
69 }
70
71 auto set_level(enum level lvl) -> void {
72 lvl_ = lvl;
73 }
74 };
75
76 export auto make_sink(level lvl) -> std::shared_ptr<sink> {
77 return std::shared_ptr<sink>{new sink{lvl}};
78 }
79
80 export class logger {
81 std::shared_ptr<sink> sink_;
82 std::string component_;
83 std::map<std::string, std::string> attrs_;
84
85 template<log::level lvl>
86 auto log_at(std::string_view fmt, std::format_args args) -> logger& {
87 if (sink_->level() <= lvl)
88 sink_->write(sink::tmp_message{
89 .lvl = lvl,
90 .component = component_,
91 .txt = std::vformat(fmt, args),
92 .attrs = attrs_,
93 });
94 return *this;
95 }
96
97 public:
98 explicit logger(std::shared_ptr<sink> const& sink)
99 : sink_{sink}
100 {
101 if (!sink) {
102 throw std::invalid_argument{"logger sink may not be null"};
103 }
104 }
105
106 [[nodiscard]] auto sub(std::string_view component) const -> logger {
107 auto l = *this;
108 if (l.component_.empty()) {
109 l.component_ = component;
110 } else {
111 l.component_ += ".";
112 l.component_ += component;
113 }
114 return l;
115 }
116
117 [[nodiscard]] auto with(std::string const& k, std::string&& v) const -> logger {
118 auto l = *this;
119 l.attrs_[k] = std::move(v);
120 return l;
121 }
122
123 [[nodiscard]] auto with(std::string const& k, std::string_view v) const -> logger {
124 return with(k, std::string{v});
125 }
126
127 template<class... Args>
128 auto debug(std::format_string<Args...> fmt, Args&&... args) -> logger& {
129 return log_at<level::debug>(fmt.get(), std::make_format_args(args...));
130 }
131
132 template<class... Args>
133 auto info(std::format_string<Args...> fmt, Args&&... args) -> logger& {
134 return log_at<level::info>(fmt.get(), std::make_format_args(args...));
135 }
136
137 template<class... Args>
138 auto warn(std::format_string<Args...> fmt, Args&&... args) -> logger& {
139 return log_at<level::warn>(fmt.get(), std::make_format_args(args...));
140 }
141
142 template<class... Args>
143 auto error(std::format_string<Args...> fmt, Args&&... args) -> logger& {
144 return log_at<level::error>(fmt.get(), std::make_format_args(args...));
145 }
146 };
147
148} // namespace routemon::log
diff --git a/server/src/main.cpp b/server/src/main.cpp
new file mode 100644
index 0000000..a40b0b0
--- /dev/null
+++ b/server/src/main.cpp
@@ -0,0 +1,109 @@
1#include <malloc.h> // for malloc_trim(3)
2#include <boost/asio.hpp>
3
4import std;
5import routemon;
6
7namespace chrono = std::chrono;
8namespace net = boost::asio;
9
10enum class exit_status {
11 failure,
12 bad_usage,
13};
14
15auto real_main(std::span<char const*> args) -> exit_status {
16 auto sink = routemon::log::make_sink(routemon::log::level::info);
17 auto l = routemon::log::logger{sink};
18
19 if (args.size() != 2) {
20 l.error("Fatal: expected exactly one argument (the configuration file location), got {}", args.size() - 1);
21 return exit_status::bad_usage;
22 }
23 auto const* config_filename = args[1];
24
25 auto lgen = routemon::locale::make_generator();
26 auto default_locale = lgen->generate("en_US.UTF-8");
27 auto locales = {
28 default_locale,
29 lgen->generate("nl_NL.UTF-8"),
30 lgen->generate("de_DE.UTF-8"),
31 lgen->generate("en_GB.UTF-8"),
32 };
33 auto lsel = routemon::locale::selector{locales, default_locale, lgen};
34
35 auto ioc = net::io_context{1 /* concurrency hint */};
36
37 auto config = routemon::config::app{};
38 try {
39 config = routemon::config::load_file(config_filename);
40 } catch (std::exception const& e) {
41 l.with("filename", std::string_view{config_filename}).
42 error("Failed to load configuration: {}", e.what());
43 return exit_status::failure;
44 }
45 sink->set_level(config.logger.level);
46 // auto rwgps_client = routemon::rwgps::client{ioc, l, config.rwgps.api_key, config.rwgps.auth_token};
47 // for (auto route : rwgps_client.get_all_routes()) {
48 // l.info("Route {} (user {}): {} @ {}", route.id, route.user_id, route.name, route.url);
49 // }
50
51 auto dbc = std::shared_ptr<routemon::database::connection>{};
52 try {
53 dbc = routemon::database::open(config.database.sqlite3_filename);
54 } catch (std::exception const& e) {
55 l.with("filename", config.database.sqlite3_filename).
56 error("Failed to open database: {}", e.what());
57 return exit_status::failure;
58 }
59
60 l.with("filename", config.situations.datex2_filename).
61 info("Loading situations");
62 auto const before_load = chrono::steady_clock::now();
63 auto d2loader = routemon::datex2::loader{};
64 auto pub = routemon::datex2::situation_publication{};
65 try {
66 pub = d2loader.load_situation_publication(config.situations.datex2_filename);
67 } catch (std::exception const& e) {
68 l.error("Failed to load DATEX II situations publication: {}", e.what());
69 return exit_status::failure;
70 }
71 if (!d2loader.warnings().empty()) {
72 auto const& warns = d2loader.warnings();
73 l.warn("Encountered {} unique warnings while loading DATEX II situations publication", warns.size());
74 auto i = 0uz;
75 for (auto it = warns.begin(); it != warns.end(); it = warns.upper_bound(*it)) {
76 l.warn("Warning {} (appeared {}×): {}", ++i, warns.count(*it), *it);
77 }
78 }
79 // Processing the feed is by far the most memory-intensive operation
80 // during the run time of this application (at the moment), the
81 // resident set will likely never be this big again. So we ask libc
82 // to return as much memory as possible to the OS.
83 malloc_trim(0);
84 auto const after_load = chrono::steady_clock::now();
85 auto const dur_load = chrono::duration_cast<chrono::milliseconds>(after_load - before_load);
86 l.info("Loading situations finished in {}", dur_load);
87
88 auto handler = routemon::api::handler{l, std::move(pub)};
89 auto http_server = routemon::srv::server{l, std::move(lsel), std::move(handler)};
90 http_server.spawn(ioc);
91 ioc.run();
92
93 l.error("I/O context stopped");
94 return exit_status::failure;
95}
96
97auto main(int argc, char* argv[]) -> int {
98 if (argc < 0) {
99 std::cout << "Fatal: argument count below zero" << std::endl;
100 return EXIT_FAILURE;
101 }
102 auto res = real_main(std::span{const_cast<char const**>(argv), static_cast<std::size_t>(argc)});
103 switch (res) {
104 case exit_status::failure:
105 return EXIT_FAILURE;
106 case exit_status::bad_usage:
107 return 2;
108 }
109}
diff --git a/server/src/problem.cppm b/server/src/problem.cppm
new file mode 100644
index 0000000..8764962
--- /dev/null
+++ b/server/src/problem.cppm
@@ -0,0 +1,60 @@
1module;
2
3#include <boost/beast/http/message.hpp>
4#include <boost/json.hpp>
5#include <boost/locale/message.hpp>
6
7export module routemon:problem;
8
9import std;
10import :locale;
11
12namespace http = boost::beast::http;
13namespace json = boost::json;
14
15namespace routemon::problem {
16
17 export struct details {
18 http::status status;
19 blocale::message title;
20 std::string_view type_uri;
21 std::optional<blocale::message> detail = std::nullopt;
22 std::optional<std::string> instance = std::nullopt;
23
24 auto set_detail(blocale::message detail) -> details& {
25 this->detail = detail;
26 return *this;
27 }
28
29 auto set_instance(std::string&& instance) -> details& {
30 this->instance = instance;
31 return *this;
32 }
33 auto set_instance(std::string_view instance) -> details& {
34 this->instance = std::string{instance};
35 return *this;
36 }
37 };
38
39 export auto tag_invoke(json::value_from_tag, json::value& jv, details const& details, std::locale locale) -> void {
40 auto obj = json::object{
41 {"type", details.type_uri},
42 {"title", details.title.str(locale)},
43 {"status", static_cast<unsigned>(details.status)},
44 };
45 if (details.detail) obj["detail"] = details.detail->str(locale);
46 if (details.instance) obj["instance"] = *details.instance;
47 jv = obj;
48 }
49
50 export struct tpl {
51 http::status status;
52 blocale::message title;
53 std::string_view type_uri;
54
55 auto instantiate() const -> details {
56 return details{status, title, type_uri};
57 }
58 };
59
60}
diff --git a/server/src/req_ctx.cppm b/server/src/req_ctx.cppm
new file mode 100644
index 0000000..797c51d
--- /dev/null
+++ b/server/src/req_ctx.cppm
@@ -0,0 +1,51 @@
1module;
2
3#include <boost/beast/http/message.hpp>
4#include <boost/beast/http/verb.hpp>
5
6export module routemon:req_ctx;
7
8import :http.common;
9import :trace;
10
11namespace routemon {
12
13 export class req_ctx {
14 trace::id tid_;
15 std::locale locale_;
16 http::verb_set route_verbs_;
17 bool keep_alive_;
18 bhttp::request_header<bhttp::fields> const& req_header_;
19
20 public:
21 explicit req_ctx(trace::id tid, std::locale locale, http::verb_set route_verbs, bool keep_alive, bhttp::request_header<bhttp::fields> const& req_header)
22 : tid_{tid}, locale_{locale}, route_verbs_{route_verbs}, keep_alive_{keep_alive}, req_header_{req_header}
23 {}
24
25 template<typename ReqBody>
26 explicit req_ctx(trace::id tid, std::locale locale, http::verb_set route_verbs, bhttp::request<ReqBody> const& req)
27 : req_ctx{tid, locale, route_verbs, req.keep_alive(), req.base()}
28 {}
29
30 auto trace_id() const -> trace::id {
31 return tid_;
32 }
33
34 auto locale() const -> std::locale {
35 return locale_;
36 }
37
38 auto route_verbs() const -> http::verb_set {
39 return route_verbs_;
40 }
41
42 auto keep_alive() const -> bool {
43 return keep_alive_;
44 }
45
46 auto req_header() const -> bhttp::request_header<bhttp::fields> const& {
47 return req_header_;
48 }
49 };
50
51} // namespace routemon
diff --git a/server/src/routemon.cppm b/server/src/routemon.cppm
new file mode 100644
index 0000000..62db02a
--- /dev/null
+++ b/server/src/routemon.cppm
@@ -0,0 +1,11 @@
1export module routemon;
2export import :api;
3export import :config;
4export import :database;
5export import :datex2;
6export import :gpx;
7export import :locale;
8export import :log;
9export import :srv;
10export import :rwgps;
11export import :util;
diff --git a/server/src/rwgps.cppm b/server/src/rwgps.cppm
new file mode 100644
index 0000000..7ad6605
--- /dev/null
+++ b/server/src/rwgps.cppm
@@ -0,0 +1,137 @@
1module;
2
3#include <boost/beast/core.hpp>
4#include <boost/beast/http.hpp>
5#include <boost/json.hpp>
6
7export module routemon:rwgps;
8
9import std;
10import :http.client;
11import :log;
12
13namespace beast = boost::beast;
14namespace bhttp = beast::http;
15namespace net = boost::asio;
16namespace json = boost::json;
17
18namespace routemon::rwgps {
19
20 export struct route_summary {
21 std::int64_t id;
22 std::int64_t user_id;
23 std::string url;
24 std::string name;
25 std::string description;
26 };
27
28 struct pagination {
29 std::size_t record_count;
30 std::size_t page_count;
31 std::size_t page_size;
32 std::optional<std::string> next_page_url;
33 };
34
35 struct get_routes_meta {
36 pagination pagination;
37 };
38
39 struct get_routes_response {
40 std::vector<route_summary> routes;
41 get_routes_meta meta;
42 };
43
44 auto tag_invoke(json::value_to_tag<route_summary> const&, json::value const& jv) -> route_summary {
45 return {
46 .id = json::value_to<std::int64_t>(jv.at("id")),
47 .user_id = json::value_to<std::int64_t>(jv.at("user_id")),
48 .url = json::value_to<std::string>(jv.at("url")),
49 .name = json::value_to<std::string>(jv.at("name")),
50 .description = json::value_to<std::string>(jv.at("description")),
51 };
52 }
53
54 auto tag_invoke(json::value_to_tag<pagination> const&, json::value const& jv) -> pagination {
55 return {
56 .record_count = json::value_to<std::size_t>(jv.at("record_count")),
57 .page_count = json::value_to<std::size_t>(jv.at("page_count")),
58 .page_size = json::value_to<std::size_t>(jv.at("page_size")),
59 .next_page_url = json::value_to<std::optional<std::string>>(jv.at("next_page_url")),
60 };
61 }
62
63 auto tag_invoke(json::value_to_tag<get_routes_meta> const&, json::value const& jv) -> get_routes_meta {
64 return {
65 .pagination = json::value_to<pagination>(jv.at("pagination")),
66 };
67 }
68
69 auto tag_invoke(json::value_to_tag<get_routes_response> const&, json::value const& jv) -> get_routes_response {
70 return {
71 .routes = json::value_to<std::vector<route_summary>>(jv.at("routes")),
72 .meta = json::value_to<get_routes_meta>(jv.at("meta")),
73 };
74 }
75
76 auto json_value_to_get_routes_response(json::value const& jv) -> get_routes_response {
77 return json::value_to<get_routes_response>(jv);
78 }
79
80 export class client {
81 log::logger l_;
82 http::client hc_;
83 std::string api_key_;
84 std::string auth_token_;
85
86 static constexpr std::string host = "ridewithgps.com";
87
88 // TODO: handle failure appropriately
89 auto get_routes_page(std::size_t page) -> get_routes_response {
90 auto req = bhttp::request<bhttp::string_body>{
91 bhttp::verb::get,
92 std::format("/api/v1/routes.json?page_size=200?page={}", page),
93 11, // HTTP 1.1
94 };
95 req.set(bhttp::field::host, host);
96 req.set("x-rwgps-api-key", api_key_);
97 req.set("x-rwgps-auth-token", auth_token_);
98
99 auto rsp = hc_.do_request(req);
100 auto p = json::stream_parser{};
101 for (auto const frag : rsp.body().cdata()) {
102 p.write(static_cast<char const*>(frag.data()), frag.size());
103 }
104 assert(p.done());
105 return json_value_to_get_routes_response(p.release());
106 }
107
108 public:
109 explicit client(net::io_context& ioc, log::logger const& l, std::string api_key, std::string auth_token)
110 : l_{l.sub("rwgps-client")}, hc_{ioc}, api_key_{std::move(api_key)}, auth_token_{std::move(auth_token)}
111 {}
112
113 auto get_all_routes() -> std::vector<route_summary> {
114 // TODO: make sure that there are no duplicates here.
115 // What does RWGPS sort on, by default?
116 // Consider using an associative container instead of a vector.
117 auto record_count = 0uz;
118 auto current_page = 0uz;
119 auto routes = std::vector<route_summary>{};
120
121 while (true) {
122 auto rsp = get_routes_page(current_page);
123 if (rsp.meta.pagination.next_page_url)
124 l_.debug("Next page URL: {}", *rsp.meta.pagination.next_page_url);
125 routes.append_range(rsp.routes);
126 if (rsp.meta.pagination.record_count > 0)
127 record_count = rsp.meta.pagination.record_count;
128 if (rsp.routes.empty() || routes.size() >= record_count) {
129 break;
130 }
131 }
132
133 return routes;
134 }
135 };
136
137} // namespace routemon::rwgps
diff --git a/server/src/sqlite3.cppm b/server/src/sqlite3.cppm
new file mode 100644
index 0000000..f226c6b
--- /dev/null
+++ b/server/src/sqlite3.cppm
@@ -0,0 +1,257 @@
1module;
2
3#include <sqlite3.h>
4
5export module routemon:sqlite3;
6
7import std;
8import :util;
9
10namespace routemon::sqlite3 {
11
12 class mutex_guard {
13 explicit mutex_guard(::sqlite3_mutex* mut) noexcept : mut_{mut} {
14 ::sqlite3_mutex_enter(mut_);
15 }
16
17 friend auto do_guarded(::sqlite3_mutex* mut, std::invocable<mutex_guard const&> auto f) -> decltype(f(std::declval<mutex_guard const&>()));
18
19 public:
20 mutex_guard(mutex_guard const&) = delete;
21 ~mutex_guard() {
22 ::sqlite3_mutex_leave(mut_);
23 }
24
25 private:
26 ::sqlite3_mutex* mut_;
27 };
28
29 auto do_guarded(::sqlite3_mutex* mut, std::invocable<mutex_guard const&> auto f) -> decltype(f(std::declval<mutex_guard const&>())) {
30 return f(mutex_guard{mut});
31 }
32
33 auto do_guarded(::sqlite3* dbc, std::invocable<mutex_guard const&> auto f) -> decltype(f(std::declval<mutex_guard const&>())) {
34 return do_guarded(::sqlite3_db_mutex(dbc), f);
35 }
36
37 class error : public std::exception {
38 int code_;
39 std::string message_;
40
41 public:
42 explicit error(mutex_guard const&, int code, ::sqlite3* dbc)
43 : code_{code}, message_{::sqlite3_errmsg(dbc)}
44 {}
45
46 explicit error(int code)
47 : code_{code}, message_{::sqlite3_errstr(code)}
48 {}
49
50 [[nodiscard]] auto what() const noexcept -> char const* override {
51 return message_.c_str();
52 }
53
54 [[nodiscard]] auto code() const noexcept -> int {
55 return code_;
56 }
57 };
58
59 template<class T, template<class U> concept C>
60 concept optional_of = requires {
61 typename T::value_type;
62 requires std::same_as<T, std::optional<typename T::value_type>>;
63 requires C<typename T::value_type>;
64 };
65
66 template<class T>
67 concept scannable_prim =
68 std::same_as<T, std::string> ||
69 std::same_as<T, double> ||
70 std::same_as<T, std::int64_t>;
71
72 template<class T>
73 concept scannable = scannable_prim<T> || optional_of<T, scannable_prim>;
74
75 class statement {
76 ::sqlite3_stmt* stmt_;
77
78 public:
79 explicit statement(::sqlite3_stmt* stmt) : stmt_{stmt} {}
80 statement(statement const&) = delete;
81 statement(statement&& s) noexcept {
82 stmt_ = s.stmt_;
83 s.stmt_ = nullptr;
84 }
85 ~statement() {
86 ::sqlite3_finalize(stmt_);
87 }
88 auto get() -> ::sqlite3_stmt* {
89 return stmt_;
90 }
91 };
92
93 class row_reader {
94 statement stmt_;
95
96 explicit row_reader(statement stmt) : stmt_{std::move(stmt)} {}
97
98 friend class connection;
99
100 void scan(int col, std::string& s) {
101 if (::sqlite3_column_type(stmt_.get(), col) != SQLITE_TEXT)
102 throw std::invalid_argument{"invalid type for scan"};
103 unsigned char const* chs = ::sqlite3_column_text(stmt_.get(), col);
104 auto size = util::size_from_int(::sqlite3_column_bytes(stmt_.get(), col));
105 if (!size.has_value())
106 throw std::logic_error{"unexpected negative amount of bytes in column"};
107 s = std::string{reinterpret_cast<char const*>(chs), *size};
108 }
109
110 void scan(int col, double& v) {
111 if (::sqlite3_column_type(stmt_.get(), col) != SQLITE_FLOAT)
112 throw std::invalid_argument{"invalid type for scan"};
113 v = ::sqlite3_column_double(stmt_.get(), col);
114 }
115
116 void scan(int col, std::int64_t& v) {
117 if (::sqlite3_column_type(stmt_.get(), col) != SQLITE_INTEGER)
118 throw std::invalid_argument{"invalid type for scan"};
119 v = ::sqlite3_column_int64(stmt_.get(), col);
120 }
121
122 void scan(int col, optional_of<scannable> auto& v) {
123 if (::sqlite3_column_type(stmt_.get(), col) == SQLITE_NULL) {
124 v.reset();
125 } else {
126 typename std::remove_cvref_t<decltype(v)>::value_type tmp;
127 scan(col, tmp);
128 v = std::move(tmp);
129 }
130 }
131
132 public:
133 auto next() -> bool {
134 ::sqlite3* dbc = ::sqlite3_db_handle(stmt_.get());
135 return do_guarded(dbc, [&](auto const& guard) -> bool {
136 auto const s = ::sqlite3_step(stmt_.get());
137 if (s == SQLITE_ROW)
138 return true;
139 if (s == SQLITE_DONE)
140 return false;
141 throw error{guard, s, dbc};
142 });
143 }
144
145 auto scan(scannable auto&... args) -> void {
146 auto const ncols = util::size_from_int(::sqlite3_data_count(stmt_.get()));
147 if (!ncols.has_value())
148 throw std::logic_error{"got unexpected negative amount of columns"};
149 if (sizeof...(args) > *ncols)
150 throw std::invalid_argument{"more scanning arguments provided than columns in result set"};
151 auto col = 0; (..., scan(col++, args));
152 }
153
154 auto scan_single(scannable auto&... args) -> void {
155 if (!next())
156 throw std::logic_error{"no row in result set"};
157 scan(args...);
158 if (next()) {
159 throw std::logic_error{"more than one row in result set"};
160 }
161 }
162 };
163
164 class binder {
165 statement& stmt_;
166
167 explicit binder(statement& stmt) : stmt_{stmt} {}
168
169 friend class connection;
170
171 public:
172 auto text(std::string const& param_name, std::string_view str) -> void {
173 int const i = ::sqlite3_bind_parameter_index(stmt_.get(), param_name.c_str());
174 if (i == 0)
175 throw std::invalid_argument{std::format("bind: no parameter with name {} found", param_name)};
176 auto str_size = util::int_from_size(str.size());
177 if (!str_size.has_value())
178 throw std::invalid_argument{"bind: provided text is too long"};
179 if (auto s = ::sqlite3_bind_text(stmt_.get(), i, str.data(), *str_size, SQLITE_TRANSIENT); s != SQLITE_OK) {
180 throw error{s};
181 }
182 }
183
184 static auto noop(binder&) -> void {}
185 };
186
187 export class connection {
188 ::sqlite3* dbc_;
189 ::sqlite3_mutex* mut_;
190
191 explicit connection(::sqlite3* dbc) : dbc_{dbc}, mut_{::sqlite3_db_mutex(dbc)} {}
192
193 friend auto open(std::string const& filename) -> connection;
194
195 public:
196 connection(connection const&) = delete;
197 connection(connection&& c) noexcept {
198 dbc_ = c.dbc_;
199 mut_ = c.mut_;
200 c.dbc_ = nullptr;
201 c.mut_ = nullptr;
202 }
203
204 [[nodiscard]] auto query(std::string const& sql, std::function<void(binder&)> const& bf = binder::noop) -> row_reader {
205 ::sqlite3_stmt* pstmt = nullptr;
206 char const* sql_tail = nullptr;
207 auto sql_size = util::int_from_size(sql.size());
208 if (!sql_size.has_value() || *sql_size >= std::numeric_limits<int>::max() - 1)
209 throw std::invalid_argument{"provided input text too large"};
210 do_guarded(mut_, [&](auto const& guard) -> void {
211 if (auto s = ::sqlite3_prepare_v2(dbc_, sql.data(), *sql_size + 1, &pstmt, &sql_tail); s != SQLITE_OK) {
212 if (pstmt != nullptr) {
213 // Use contract_assert when having a compiler with contracts available
214 ::sqlite3_finalize(pstmt);
215 throw std::logic_error{"expected stmt to be null after failed preparation"};
216 }
217 throw error{guard, s, dbc_};
218 }
219 });
220 if (!pstmt)
221 throw std::invalid_argument{"provided input text contains no SQL"};
222 auto stmt = statement{pstmt};
223 if (sql_tail && std::strlen(sql_tail) > 0)
224 throw std::invalid_argument{"provided input text contains more than one SQL statement"};
225 auto b = binder{stmt}; bf(b);
226 return row_reader{std::move(stmt)};
227 }
228
229 auto exec(std::string const& sql, std::function<void(binder&)> const& bf = binder::noop) -> void {
230 auto reader = query(sql, bf);
231 while (reader.next());
232 }
233
234 ~connection() {
235 std::ignore = ::sqlite3_close(std::exchange(dbc_, nullptr));
236 }
237 };
238
239 export auto open(std::string const& filename) -> connection {
240 ::sqlite3* dbc = nullptr;
241 auto s = ::sqlite3_open_v2(filename.c_str(), &dbc,
242 SQLITE_OPEN_READWRITE | SQLITE_OPEN_CREATE |
243 SQLITE_OPEN_FULLMUTEX | SQLITE_OPEN_EXRESCODE,
244 nullptr);
245 if (s != SQLITE_OK) {
246 if (dbc) {
247 do_guarded(dbc, [&](auto const& guard) -> void {
248 throw error{guard, s, dbc};
249 });
250 } else {
251 throw error{s};
252 }
253 }
254 return connection{dbc};
255 }
256
257} // namespace routemon::sqlite3
diff --git a/server/src/srv.cppm b/server/src/srv.cppm
new file mode 100644
index 0000000..2ca48c6
--- /dev/null
+++ b/server/src/srv.cppm
@@ -0,0 +1,221 @@
1module;
2
3#include <boost/config.hpp>
4#include <boost/asio/ip/tcp.hpp>
5#include <boost/asio/as_tuple.hpp>
6#include <boost/asio/awaitable.hpp>
7#include <boost/asio/co_spawn.hpp>
8#include <boost/beast/core.hpp>
9#include <boost/beast/http.hpp>
10#include <boost/json.hpp>
11#include <boost/locale/generator.hpp>
12
13#include <expat.h>
14
15export module routemon:srv;
16
17import std;
18import :api;
19import :config;
20import :gpx;
21import :http.server;
22import :locale;
23import :log;
24import :problem;
25import :req_ctx;
26import :util;
27
28namespace beast = boost::beast;
29namespace json = boost::json;
30namespace net = boost::asio;
31using tcp = boost::asio::ip::tcp;
32
33namespace routemon::srv {
34
35 class gpx_parse_error_category_impl : public std::error_category {
36 public:
37 char const* name() const noexcept override { return "gpx_parse"; }
38 auto message(int condition) const noexcept -> std::string override {
39 std::ignore = condition;
40 return "failed to parse GPX file";
41 }
42 };
43 auto gpx_parse_error_category() noexcept -> gpx_parse_error_category_impl const& {
44 static auto const inst = gpx_parse_error_category_impl{};
45 return inst;
46 }
47 auto gpx_parse_error() noexcept -> std::error_code {
48 return std::error_code{1, gpx_parse_error_category()};
49 }
50
51 class gpx_parse_result {
52 std::variant<std::exception_ptr, gpx::file> res_;
53
54 public:
55 auto set_exception(std::exception_ptr ex) noexcept {
56 res_ = ex;
57 }
58 auto set_gpx_file(gpx::file&& f) noexcept {
59 res_ = std::move(f);
60 }
61
62 auto unwrap() -> gpx::file&& {
63 return std::visit(util::overloaded{
64 [](std::exception_ptr ex) -> gpx::file&& {
65 if (ex) std::rethrow_exception(ex);
66 else throw std::runtime_error{"no GPX file parse result available"};
67 },
68 [](gpx::file&& f) -> gpx::file&& { return std::move(f); },
69 }, std::move(res_));
70 }
71 };
72
73 struct readable_gpx_body {
74 using value_type = gpx_parse_result;
75
76 class reader {
77 gpx::reader r_;
78 util::not_null<value_type*> res_;
79
80 public:
81 template<bool isRequest, bhttp::concepts::fields Fields>
82 explicit reader(bhttp::header<isRequest, Fields>&, value_type& v)
83 : res_{&v}
84 {}
85
86 // The following methods (which are called by Beast) are marked
87 // noexcept, since Beast does not ensure that exceptions thrown
88 // here are appropriately directed to the caller of
89 // (async_)read(_some), so throwing here might cause the program
90 // to crash.
91
92 auto init(boost::optional<std::uint64_t> /* n */, beast::error_code& ec) noexcept -> void {
93 try {
94 r_.init();
95 ec = {};
96 } catch (std::exception& ex) {
97 res_->set_exception(std::current_exception());
98 ec = gpx_parse_error();
99 }
100 }
101
102 auto put(beast::concepts::const_buffer_sequence auto b, beast::error_code& ec) noexcept -> std::size_t {
103 auto total = 0uz;
104 try {
105 for (auto it = net::buffer_sequence_begin(b); it != net::buffer_sequence_end(b); it++) {
106 r_.put(std::string_view{static_cast<char const*>(it->data()), it->size()});
107 total += it->size();
108 }
109 ec = {};
110 } catch (std::exception& ex) {
111 res_->set_exception(std::current_exception());
112 ec = gpx_parse_error();
113 }
114 return total;
115 }
116
117 auto finish(beast::error_code& ec) noexcept {
118 try {
119 res_->set_gpx_file(r_.finish());
120 ec = {};
121 } catch (std::exception& ex) {
122 res_->set_exception(std::current_exception());
123 ec = gpx_parse_error();
124 }
125 }
126 };
127 };
128 static_assert(bhttp::concepts::body<readable_gpx_body>);
129 static_assert(bhttp::concepts::body_reader<readable_gpx_body>);
130
131 class handler {
132 api::handler inner_;
133
134 public:
135 using outer_ctx = http::trace_id_ctx<http::base_ctx>;
136 using l0_ctx = http::routed_ctx<outer_ctx>;
137
138 private:
139 auto handle_process_gpx(l0_ctx ctx, http::readable_request r) -> net::awaitable<http::presponse> {
140 auto gpx_file = gpx::file{};
141 try {
142 auto req = co_await http::read_request<readable_gpx_body>(ctx, std::move(r));
143 gpx_file = std::move(req->body().unwrap());
144 } catch (std::exception& ex) {
145 // TODO: more detailed problem reporting
146 auto tpl = problem::tpl{
147 .status = bhttp::status::bad_request,
148 .title = translate("Failed to parse GPX file"),
149 .type_uri = "https://routemon.fautchen.eu/problems/gpx-parse-failed",
150 };
151 co_return http::problem_rsp(ctx, tpl.instantiate(), http::keep_alive{false});
152 }
153
154 // TODO: catch handler exceptions and return 500 when raised?
155 // (keep-alive depends on whether whole request was read)
156 auto mres = inner_.process_gpx(std::move(gpx_file));
157 if (!mres) {
158 auto tpl = problem::tpl{
159 .status = bhttp::status::internal_server_error,
160 .title = translate("Internal server error"),
161 .type_uri = "https://routemon.fautchen.eu/problems/internal-server-error",
162 };
163 co_return http::problem_rsp(ctx, tpl.instantiate(), http::keep_alive{true});
164 }
165
166 auto rsp = http::make_rsp<bhttp::string_body>(bhttp::status::ok, http::keep_alive{true});
167 rsp.set(bhttp::field::content_type, "application/json");
168 rsp.body() = json::serialize(json::value_from(*mres));
169 rsp.prepare_payload();
170 co_return rsp;
171 }
172
173 auto handle_sysinfo(l0_ctx ctx, http::readable_request r) -> net::awaitable<http::presponse> {
174 auto req = co_await http::read_request<bhttp::empty_body>(ctx, std::move(r));
175 auto info = inner_.sysinfo();
176
177 auto rsp = http::make_rsp<bhttp::string_body>(bhttp::status::ok, http::keep_alive{true});
178 rsp.set(bhttp::field::content_type, "application/json");
179 rsp.body() = json::serialize(json::value_from(info));
180 rsp.prepare_payload();
181 co_return rsp;
182 }
183
184 public:
185 handler(api::handler&& inner) : inner_{std::move(inner)} {}
186
187 auto make_routes() -> http::route_tree<http::routed_ctx<outer_ctx>> {
188 auto handler = [this]<class MemFn>(MemFn member) {
189 return std::bind_front(member, this);
190 };
191
192 return http::dtree<http::routed_ctx<outer_ctx>>{}.named_subtrees({
193 {"gpx", http::dtree<l0_ctx>{{
194 .post = handler(&handler::handle_process_gpx),
195 }}.no_subtrees()},
196 {"sysinfo", http::dtree<l0_ctx>{{
197 .get = handler(&handler::handle_sysinfo),
198 }}.no_subtrees()},
199 });
200 }
201 };
202
203 export class server {
204 handler handler_;
205 http::server<handler::outer_ctx> srv_;
206
207 static auto make_global_middleware() -> http::middleware_t<http::base_ctx, handler::outer_ctx> {
208 return http::middleware_compose<http::base_ctx, http::trace_id_ctx<http::base_ctx>, http::trace_id_ctx<http::base_ctx>>(http::trace_id_middleware<http::base_ctx>, http::lax_cors_middleware<http::trace_id_ctx<http::base_ctx>>);
209 }
210
211 public:
212 server(log::logger const& l, locale::selector&& lsel, api::handler&& inner)
213 : handler_{std::move(inner)}, srv_{l, std::move(lsel), make_global_middleware(), handler_.make_routes()}
214 {}
215
216 auto spawn(net::io_context& ioc) -> void {
217 srv_.spawn(ioc);
218 }
219 };
220
221} // namespace routemon::srv
diff --git a/server/src/time.cppm b/server/src/time.cppm
new file mode 100644
index 0000000..767883c
--- /dev/null
+++ b/server/src/time.cppm
@@ -0,0 +1,205 @@
1export module routemon:time;
2
3import std;
4
5export namespace routemon::time {
6
7 using timestamp = std::chrono::time_point<std::chrono::utc_clock>;
8
9 class period {
10 // Assuming [start, end). Unfortunately the DATEX II model is not
11 // clear about this.
12 timestamp start_;
13 timestamp end_;
14
15 public:
16 explicit period(timestamp start, timestamp end)
17 : start_{start}, end_{end}
18 {
19 if (start >= end) {
20 throw std::invalid_argument("period: start should be before end");
21 }
22 }
23
24 [[nodiscard]] auto intersect(period other) const -> std::optional<period> {
25 auto const new_start = start_ < other.start() ? other.start() : start_;
26 auto const new_end = other.end() < end_ ? other.end() : end_;
27 return new_start < new_end ? std::make_optional(period{new_start, new_end}) : std::nullopt;
28 }
29
30 [[nodiscard]] auto except(period other) const -> std::pair<std::optional<period>, std::optional<period>> {
31 auto const before_start = start_;
32 auto const before_end = other.start();
33 auto const after_start = end_;
34 auto const after_end = other.end();
35 std::optional<period> before, after;
36 if (before_start < before_end)
37 before = period{before_start, before_end};
38 if (after_start < after_end)
39 after = period{after_end, after_start};
40 return std::make_pair(before, after);
41 }
42
43 [[nodiscard]] auto start() const -> timestamp { return start_; }
44 [[nodiscard]] auto end() const -> timestamp { return end_; }
45 };
46
47 class period_seq {
48 std::vector<period> periods_;
49
50 // The way lt and ge are ordered makes a difference for how the sorting
51 // (insertion based on lower_bound) works. Do not carelessly reorder this.
52 enum lt_ge : std::uint8_t {
53 ge, // >=
54 lt, // <
55 };
56
57 // O(n log n)
58 template<std::input_iterator I, std::sentinel_for<I> S>
59 requires std::same_as<std::iter_value_t<I>, period>
60 static auto consolidate(I begin, S end) -> std::vector<period> {
61 auto periods = std::vector<period>{};
62 auto preds = std::vector<std::pair<timestamp, lt_ge>>{};
63
64 for (auto it = begin; it != end; it++) {
65 auto const& period = *it;
66
67 auto const a = std::make_pair(period.start(), ge);
68 auto const b = std::make_pair(period.end(), lt);
69 preds.insert(std::lower_bound(preds.begin(), preds.end(), a), a);
70 preds.insert(std::lower_bound(preds.begin(), preds.end(), b), b);
71 }
72
73 if (preds.empty())
74 return periods;
75
76 if (preds.size() < 2)
77 throw std::logic_error{"period_seq::consolidate: amount of predicates should be >= 2"};
78 if (preds.front().second != ge)
79 throw std::logic_error{"period_seq::consolidate: first element of preds should be a ge-element"};
80 if (preds.back().second != lt)
81 throw std::logic_error{"period_seq::consolidate: last element of preds should be an lt-element"};
82
83 auto period_start = preds[0].first;
84 for (std::size_t i = 1; i < preds.size(); i++) {
85 if (preds[i].second == lt && (i + 1 == preds.size() || preds[i + 1].second == ge)) {
86 auto const period_end = preds[i].first;
87 if (!periods.empty() && periods.back().start() == period_start)
88 periods.back() = period{periods.back().end(), period_end};
89 else
90 periods.emplace_back(period_start, period_end);
91 if (i + 1 != preds.size()) {
92 period_start = preds[i + 1].first;
93 i++;
94 }
95 }
96 }
97
98 return periods;
99 }
100
101 explicit period_seq(std::vector<period> periods)
102 : periods_{std::move(periods)}
103 {
104 for (auto i = 0uz; i < periods_.size(); i++) {
105 if (i + 1 < periods_.size()) {
106 if (periods_[i].end() >= periods_[i + 1].start()) {
107 throw std::logic_error{"period_seq: vector provided to private constructor not ordered properly"};
108 }
109 }
110 }
111 }
112
113 public:
114 template<std::input_iterator I, std::sentinel_for<I> S>
115 requires std::same_as<std::iter_value_t<I>, period>
116 explicit period_seq(I begin, S end)
117 : periods_{consolidate(begin, end)}
118 {}
119
120 explicit period_seq(period singleton)
121 : periods_{singleton}
122 {}
123
124 [[nodiscard]] auto intersect(period_seq const& other) const -> period_seq {
125 auto it1 = periods_.begin(); auto end1 = periods_.end();
126 auto it2 = other.periods_.begin(); auto end2 = other.periods_.end();
127
128 auto res = std::vector<period>{};
129 while (it1 != end1 && it2 != end2) {
130 auto overlap = it1->intersect(*it2);
131 if (overlap) {
132 res.push_back(*overlap);
133 if (it1->end() < it2->end()) {
134 it1++;
135 } else {
136 it2++;
137 }
138 } else {
139 if (it1->end() < it2->start()) {
140 it1++;
141 } else {
142 it2++;
143 }
144 }
145 }
146
147 return period_seq{res};
148 }
149
150 [[nodiscard]] auto except(period_seq const& other) const -> period_seq {
151 // This code was pretty tricky to write, I wouldn't be surprised if it has some bugs in it.
152
153 auto it1 = periods_.begin(); auto end1 = periods_.end();
154 auto it2 = other.periods_.begin(); auto end2 = other.periods_.end();
155
156 auto res = std::vector<period>{};
157 if (it1 == end1)
158 return period_seq{res};
159 if (it2 == end2)
160 return period_seq{periods_};
161 auto period1 = period{*it1++};
162
163 while (it1 != end1 && it2 != end2) {
164 if (period1.end() <= it2->start()) {
165 res.push_back(period1);
166 period1 = *it1++;
167 } else if (it2->end() <= period1.start()) {
168 it2++;
169 } else /* period1.begin() < it2->end() && it2->begin() < period1.end() */ {
170 auto const [mbefore, mafter] = period1.except(*it2);
171 if (mbefore)
172 res.push_back(*mbefore);
173 if (mafter) {
174 period1 = *mafter;
175 } else {
176 period1 = *it1++;
177 }
178 }
179 }
180
181 return period_seq{res};
182 }
183
184 [[nodiscard]] auto periods() const -> std::vector<period> const& {
185 return periods_;
186 }
187 };
188
189 auto operator<<(std::ostream& os, period const& p) -> std::ostream& {
190 return os << "[" << p.start() << ", " << p.end() << ")";
191 }
192
193 auto operator<<(std::ostream &os, period_seq const& ps) -> std::ostream& {
194 os << "{";
195 auto it = ps.periods().begin();
196 while (it != ps.periods().end()) {
197 os << " " << *it;
198 if (++it != ps.periods().end()) {
199 os << ",";
200 }
201 }
202 return os << " }";
203 }
204
205} // namespace routemon::time
diff --git a/server/src/trace.cppm b/server/src/trace.cppm
new file mode 100644
index 0000000..00ecd05
--- /dev/null
+++ b/server/src/trace.cppm
@@ -0,0 +1,79 @@
1module;
2
3// Might as well since we're using OpenSSL
4#include <openssl/err.h>
5#include <openssl/rand.h>
6
7export module routemon:trace;
8
9import std;
10import :util;
11
12namespace routemon::trace {
13
14 class uuid7 {
15 std::uint64_t high_ = 0;
16 std::uint64_t low_ = 0;
17
18 public:
19 uuid7() {
20 namespace chrono = std::chrono;
21 auto const unix_time_ms_signed = static_cast<std::int64_t>(chrono::duration_cast<chrono::milliseconds>(chrono::system_clock::now().time_since_epoch()).count());
22 if (unix_time_ms_signed < 0)
23 throw std::runtime_error{"system time before UNIX epoch"};
24 auto const unix_time_ms = static_cast<std::uint64_t>(unix_time_ms_signed);
25 if (std::countl_zero(unix_time_ms) < 16)
26 throw std::runtime_error{"system time too great"};
27
28 auto rand = std::array<unsigned char, 10>{};
29 int s = RAND_bytes(rand.data(), static_cast<int>(rand.size()));
30 if (s != 1) {
31 unsigned long e = ERR_get_error();
32 throw std::runtime_error{std::format("failed to generate UUID(v7): {} ({}, code {})", ERR_reason_error_string(e), ERR_lib_error_string(e), e)};
33 }
34
35 auto version = std::uint64_t{0b0111};
36 auto variant = std::uint64_t{0b10};
37
38 high_ |= unix_time_ms << 16;
39 high_ |= version << 12;
40 high_ |= std::uint64_t{rand[0]} << 4;
41 high_ |= std::uint64_t{rand[1]};
42 low_ |= variant << 62;
43 low_ |= std::uint64_t{rand[2]} << 54;
44 low_ |= std::uint64_t{rand[3]} << 48;
45 low_ |= std::uint64_t{rand[4]} << 40;
46 low_ |= std::uint64_t{rand[5]} << 32;
47 low_ |= std::uint64_t{rand[6]} << 24;
48 low_ |= std::uint64_t{rand[7]} << 16;
49 low_ |= std::uint64_t{rand[8]} << 8;
50 low_ |= std::uint64_t{rand[9]};
51 }
52
53 auto format(std::array<char, 37>& target) -> void {
54 auto high_high = (high_ & 0xffff'ffff'0000'0000) >> 32;
55 auto high_low_high = (high_ & 0x0000'0000'ffff'0000) >> 16;
56 auto low_low_high = (high_ & 0x0000'0000'0000'ffff) >> 0;
57 auto high_low = (low_ & 0xffff'0000'0000'0000) >> 48;
58 auto low_low = (low_ & 0x0000'ffff'ffff'ffff) >> 0;
59
60 std::format_to(target.begin(), "{:0>8x}-{:0>4x}-{:0>4x}-{:0>4x}-{:0>12x}",
61 high_high, high_low_high, low_low_high, high_low, low_low);
62 target.back() = '\0';
63 }
64 };
65
66 export class id {
67 std::array<char, 37> chars_;
68
69 public:
70 id() {
71 uuid7{}.format(chars_);
72 }
73
74 auto as_string() const -> util::zstring_view {
75 return util::zstring_view{chars_.data(), chars_.size() - 1};
76 }
77 };
78
79} // namespace routemon::trace
diff --git a/server/src/util.cppm b/server/src/util.cppm
new file mode 100644
index 0000000..65f4d67
--- /dev/null
+++ b/server/src/util.cppm
@@ -0,0 +1,254 @@
1// Stuff that doesn't really have a place right now, but that is
2// broadly useful.
3export module routemon:util;
4
5import std;
6
7namespace routemon::util {
8
9 // For use with e.g. std::visit (on std::variant).
10 template<class... Ts>
11 struct overloaded : Ts... {
12 using Ts::operator()...;
13 };
14
15 export constexpr auto parse_double(std::string_view s, std::chars_format fmt = std::chars_format::general) noexcept -> std::optional<double> {
16 auto x = 0.0;
17 auto [_, ec] = std::from_chars(s.data(), s.data() + s.size(), x, fmt);
18 if (ec == std::errc{}) {
19 return x;
20 } else {
21 return std::nullopt;
22 }
23 }
24
25 export constexpr auto parse_float(std::string_view s, std::chars_format fmt = std::chars_format::general) noexcept -> std::optional<float> {
26 auto x = 0.0;
27 auto [_, ec] = std::from_chars(s.data(), s.data() + s.size(), x, fmt);
28 if (ec == std::errc{}) {
29 return x;
30 } else {
31 return std::nullopt;
32 }
33 }
34
35 export template<class T>
36 class aolist : public std::enable_shared_from_this<aolist<T>> {
37 T v_;
38 std::shared_ptr<aolist<T> const> next_;
39
40 explicit aolist(T v, std::shared_ptr<aolist<T> const> next)
41 : v_{v}, next_{next}
42 {}
43
44 public:
45 static auto nil() -> std::shared_ptr<aolist<T>> {
46 return nullptr;
47 }
48
49 static auto cons(T v, std::shared_ptr<aolist<T> const> l) -> std::shared_ptr<aolist<T>> {
50 return std::shared_ptr<aolist<T>>{new aolist<T>{v, l}};
51 }
52
53 auto next() const -> std::shared_ptr<aolist<T> const> {
54 return next_;
55 }
56
57 auto value() const noexcept -> T const& {
58 return v_;
59 }
60 };
61
62 export constexpr auto size_from_int(int x) -> std::optional<std::size_t> {
63 static_assert(sizeof(int) <= sizeof(std::size_t), "cannot cast int to smaller size_t type");
64 if (x < 0)
65 return std::nullopt;
66 return static_cast<std::size_t>(x);
67 }
68
69 export constexpr auto int_from_size(std::size_t x) -> std::optional<int> {
70 constexpr auto int_max = size_from_int(std::numeric_limits<int>::max());
71 static_assert(int_max.has_value());
72 if (x > *int_max)
73 return std::nullopt;
74 return static_cast<int>(x);
75 }
76
77 export class zstring_view {
78 char const* s_;
79 std::size_t length_;
80
81 public:
82 constexpr explicit zstring_view(char const* s, std::size_t length) :
83 s_{s}, length_{length}
84 {}
85
86 constexpr zstring_view(char const* s) :
87 zstring_view{s, std::char_traits<char>::length(s)}
88 {}
89
90 auto length() const -> std::size_t {
91 return length_;
92 }
93
94 auto c_str() const -> char const* {
95 return s_;
96 }
97
98 operator std::string_view() const {
99 return std::string_view{s_, length_};
100 }
101
102 operator char const*() const {
103 return s_;
104 }
105 };
106
107 // View for null-terminated strings for which we might not
108 // necessarily be interested in the length. String length is only
109 // calculated on demand, at most once on each thread (on more than
110 // one thread when racing). May be null.
111 //
112 // It is undefined behavior to assign to a lazy_zstring_view when
113 // it is in use by other threads.
114 export class lazy_zstring_view {
115 static constexpr auto unset_length = std::numeric_limits<std::size_t>::max();
116
117 char const* s_; // nullable
118 mutable std::atomic<std::size_t> length_;
119 static_assert(decltype(length_)::is_always_lock_free);
120
121 public:
122 constexpr explicit lazy_zstring_view(char const* s) :
123 s_{s}, length_{s ? unset_length : 0}
124 {}
125 ~lazy_zstring_view() = default;
126
127 lazy_zstring_view(lazy_zstring_view const& sv) noexcept
128 : s_{sv.s_}, length_{sv.length_.load(std::memory_order_acquire)}
129 {}
130 lazy_zstring_view(lazy_zstring_view&& sv) noexcept
131 : s_{sv.s_}, length_{sv.length_.load(std::memory_order_acquire)}
132 {}
133 auto operator=(lazy_zstring_view const& rhs) noexcept -> lazy_zstring_view& {
134 if (this != &rhs) {
135 s_ = rhs.s_;
136 length_.store(rhs.length_.load(std::memory_order_acquire), std::memory_order_release);
137 }
138 return *this;
139 }
140 auto operator=(lazy_zstring_view&& rhs) noexcept -> lazy_zstring_view& {
141 return *this = rhs; // use the copy assignment operator
142 }
143
144 auto length() const noexcept -> std::size_t {
145 if (auto v = length_.load(std::memory_order_acquire); v != unset_length)
146 return v;
147 auto l = std::char_traits<char>::length(s_);
148 length_.store(l, std::memory_order_release);
149 return l;
150 }
151
152 auto c_str() const noexcept -> char const* {
153 return s_;
154 }
155
156 operator std::string_view() const noexcept {
157 return std::string_view{s_, length()};
158 }
159
160 operator char const*() const noexcept {
161 return s_;
162 }
163
164 auto operator==(std::string_view sv) const noexcept -> bool {
165 if (auto v = length_.load(std::memory_order_acquire); v != unset_length)
166 if (sv.length() != v)
167 return false;
168 auto res = std::char_traits<char>::compare(s_, sv.data(), sv.length());
169 if (res != 0)
170 return false;
171 // Strings are equal for sv.length() characters.
172 if (s_[sv.length()] != '\0')
173 return false;
174 // Strings are actually equal, and we have just found out the
175 // length of this string, so we might as well set it.
176 length_.store(sv.length(), std::memory_order_release);
177 return true;
178 }
179 };
180
181 constexpr auto operator""_zsv(char const* s, std::size_t length) noexcept -> zstring_view {
182 return zstring_view{s, length};
183 }
184
185 auto operator==(zstring_view lhs, zstring_view rhs) -> bool {
186 return std::string_view{lhs} == std::string_view{rhs};
187 }
188
189 export constexpr auto split_on(std::string_view s, char c) -> std::pair<std::string_view, std::optional<std::string_view>> {
190 if (auto i = s.find(c); i != std::string_view::npos)
191 return std::make_pair(s.substr(0, i), s.substr(i + 1));
192 return std::make_pair(s, std::nullopt);
193 }
194
195 export template<class T>
196 class not_null;
197
198 export template<class T>
199 class not_null<T*> {
200 T* p_;
201
202 struct guaranteed_not_null_t {};
203 explicit not_null(T* p, guaranteed_not_null_t) noexcept : p_{p} {}
204
205 public:
206 explicit not_null(T* p)
207 : p_{p}
208 { if (!p_) throw std::runtime_error{"not_null constructed with null pointer"}; }
209 ~not_null() = default;
210
211 not_null(not_null const& other) = default;
212 not_null(not_null&& other) noexcept = default;
213 auto operator=(not_null const& rhs) noexcept -> not_null& = default;
214 auto operator=(not_null&& rhs) noexcept -> not_null& = default;
215
216 friend auto make_not_null(T* p) noexcept -> std::optional<not_null> {
217 if (p) return not_null(p, guaranteed_not_null_t{});
218 else return std::nullopt;
219 }
220
221 [[nodiscard]] auto get() const noexcept -> T* {
222 return p_;
223 }
224
225 auto operator*() const noexcept -> std::add_lvalue_reference_t<T> {
226 return *p_;
227 }
228
229 auto operator->() const noexcept -> T* {
230 return p_;
231 }
232 };
233 export template<class T> explicit not_null(T*) -> not_null<T*>;
234
235 export template<>
236 class not_null<lazy_zstring_view> {
237 lazy_zstring_view s_;
238
239 public:
240 explicit not_null(lazy_zstring_view s)
241 : s_{std::move(s)}
242 { if (!s_) throw std::runtime_error{"not_null constructed with null pointer"}; }
243
244 [[nodiscard]] auto get() const noexcept -> lazy_zstring_view {
245 return s_;
246 }
247
248 operator lazy_zstring_view() const noexcept { return s_; }
249 operator std::string_view() const noexcept { return s_; }
250 operator char const*() const noexcept { return s_; }
251 };
252 export explicit not_null(lazy_zstring_view s) -> not_null<lazy_zstring_view>;
253
254} // namespace routemon::util
diff --git a/server/src/xml.cpp b/server/src/xml.cpp
new file mode 100644
index 0000000..cad42d1
--- /dev/null
+++ b/server/src/xml.cpp
@@ -0,0 +1,61 @@
1module;
2
3#include <cassert>
4#include <expat.h>
5
6module routemon:xml$impl;
7
8import :xml;
9
10namespace routemon::xml {
11
12 auto qname_view::operator==(qname_view const& rhs) const -> bool {
13 return ns_uri == rhs.ns_uri && local == rhs.local;
14 }
15
16 executor::executor() :
17 p_{XML_ParserCreateNS("UTF-8", detail::qname_sep)}
18 {
19 XML_SetUserData(p_, this);
20 XML_SetElementHandler(p_, handle_start_element, handle_end_element);
21 XML_SetCharacterDataHandler(p_, handle_character_data);
22 XML_SetProcessingInstructionHandler(p_, handle_processing_instructions);
23 XML_SetExternalEntityRefHandler(p_, handle_external_entity_ref);
24 XML_SetNamespaceDeclHandler(p_, handle_start_namespace_decl, handle_end_namespace_decl);
25 XML_SetXmlDeclHandler(p_, handle_xml_decl);
26 }
27
28 executor::~executor() {
29 XML_ParserFree(p_);
30 }
31
32 auto executor::start() -> void {
33 continuation_.resume();
34 if (ex_) std::rethrow_exception(ex_);
35 }
36
37 auto executor::read(std::string_view xml, bool is_final) -> void {
38 if (ex_)
39 throw std::runtime_error{"refusing to restart parser that was thrown in"};
40 // TODO: narrow_cast
41 if (auto s = XML_Parse(p_, xml.data(), static_cast<int>(xml.size()), is_final); s != XML_STATUS_OK) {
42 auto errc = XML_GetErrorCode(p_);
43 if (errc == XML_ERROR_ABORTED) {
44 assert(ex_);
45 std::rethrow_exception(ex_);
46 } else {
47 throw std::runtime_error{std::format("failed to parse XML: {}", XML_ErrorString(errc))};
48 }
49 }
50 }
51
52 auto executor::end() -> void {
53 if (ex_)
54 throw std::runtime_error{"refusing to restart parser that was thrown in"};
55 ev_ = eof_event{};
56 advance_ = false;
57 while (continuation_) continuation_.resume();
58 if (ex_) std::rethrow_exception(ex_);
59 }
60
61} // namespace routemon::xml
diff --git a/server/src/xml.cppm b/server/src/xml.cppm
new file mode 100644
index 0000000..957f149
--- /dev/null
+++ b/server/src/xml.cppm
@@ -0,0 +1,632 @@
1module;
2
3#include <cassert>
4#include <expat.h>
5
6export module routemon:xml;
7
8import std;
9import :util;
10
11// XML parsing module.
12//
13// Makes heavy use of C++20 coroutines. Provides combinators to build
14// XML (data format) parsers with. To keep overhead low (and allow for
15// HALO/CoroElide), many non-polymorphic definitions are marked inline
16// (which is not the default in module units). This also has the added
17// benefit of allowing HALO across TU boundaries, which is practically
18// necessary to reduce unnecessary allocations when building parsers
19// using the provided combinators.
20
21// Ensure that Expat is speaking UTF-8
22static_assert(std::is_same_v<XML_Char, char>);
23
24namespace routemon::xml {
25
26 struct qname_view {
27 std::string_view ns_uri;
28 std::string_view local;
29
30 auto operator==(qname_view const& rhs) const -> bool;
31 };
32
33 namespace detail {
34
35 constexpr auto qname_sep = '\xFF';
36 auto split_name(char const* name) noexcept -> qname_view {
37 auto [l, r] = util::split_on(name, qname_sep);
38 if (r) return { .ns_uri = l, .local = *r };
39 else return { .ns_uri = std::string_view{}, .local = l };
40 }
41
42 } // namespace detail
43
44 class attribute_view_iterator {
45 std::string_view default_ns_uri_;
46 char const* const* attrs_;
47
48 auto advance() -> void {
49 attrs_ += 2;
50 }
51
52 public:
53 using difference_type = std::ptrdiff_t;
54 using value_type = std::pair<qname_view, char const*>;
55
56 struct sentinel {
57 friend constexpr auto operator==(attribute_view_iterator const& it, sentinel) noexcept -> bool {
58 return !*it.attrs_;
59 }
60 };
61
62 inline explicit attribute_view_iterator(std::string_view default_ns_uri, char const* const* attrs)
63 : default_ns_uri_{default_ns_uri}, attrs_{attrs}
64 {}
65
66 inline auto operator*() const -> std::pair<qname_view, char const*> {
67 if (!*attrs_)
68 throw std::runtime_error{"end of attribute list"};
69 auto qname = detail::split_name(attrs_[0]);
70 if (qname.ns_uri.empty())
71 qname.ns_uri = default_ns_uri_;
72 return std::make_pair(qname, attrs_[1]);
73 }
74
75 // Pre-increment
76 inline auto operator++() -> attribute_view_iterator& {
77 advance();
78 return *this;
79 }
80
81 // Post-increment
82 inline auto operator++(int) -> attribute_view_iterator {
83 auto pre = *this;
84 advance();
85 return pre;
86 }
87 };
88 static_assert(std::input_iterator<attribute_view_iterator>);
89
90 class attribute_view : std::ranges::view_base {
91 std::string_view default_ns_uri_;
92 char const* const* attrs_;
93
94 public:
95 inline explicit attribute_view(std::string_view default_ns_uri, char const** attrs)
96 : default_ns_uri_{default_ns_uri}, attrs_{const_cast<char const* const*>(attrs)}
97 {}
98
99 [[nodiscard]] inline auto begin() const -> attribute_view_iterator {
100 return attribute_view_iterator{default_ns_uri_, attrs_};
101 }
102
103 [[nodiscard]] inline auto end() const -> attribute_view_iterator::sentinel {
104 return {};
105 }
106
107 inline auto lookup(qname_view want) -> std::optional<util::not_null<util::lazy_zstring_view>> {
108 for (auto const& [name, v] : *this) {
109 if (name == want) {
110 return util::not_null{util::lazy_zstring_view{v}};
111 }
112 }
113 return std::nullopt;
114 }
115 };
116 static_assert(std::ranges::input_range<attribute_view>);
117
118 template<class T> class promise;
119
120 template<class T>
121 struct [[clang::coro_await_elidable, clang::coro_return_type]] parser {
122 using promise_type = promise<T>;
123 using result_type = promise_type::result_type;
124 using handle_type = std::coroutine_handle<promise_type>;
125
126 private:
127 handle_type h_;
128
129 public:
130 explicit parser(handle_type h)
131 : h_{h}
132 { assert(h); }
133
134 parser(const parser&) = delete;
135 parser(parser&& c) noexcept
136 : h_{std::exchange(c.h_, nullptr)}
137 {}
138 auto operator=(const parser&) -> parser& = delete;
139 auto operator=(parser&&) -> parser& = delete;
140
141 [[nodiscard]] auto promise() const -> promise_type& {
142 return h_.promise();
143 }
144
145 ~parser() {
146 if (h_) h_.destroy();
147 }
148 };
149
150 struct start_element_event {
151 qname_view name;
152 attribute_view attrs;
153 };
154 struct end_element_event {
155 qname_view name;
156 };
157 struct character_data_event {
158 std::string_view data;
159 };
160 struct processing_instructions_event {
161 util::lazy_zstring_view target;
162 util::lazy_zstring_view data;
163 };
164 struct xml_decl_event {
165 util::lazy_zstring_view version;
166 util::lazy_zstring_view encoding;
167 std::optional<bool> standalone;
168 };
169 struct eof_event {};
170 using event = std::variant<start_element_event,
171 end_element_event,
172 character_data_event,
173 processing_instructions_event,
174 xml_decl_event,
175 eof_event>;
176 template<class T>
177 concept event_type = requires(event ev) { std::get<T>(ev); };
178
179 class executor;
180 using executor_ref = util::not_null<executor*>;
181
182 struct current_event_t {
183 executor_ref executor;
184 };
185 auto current_event(executor_ref executor) -> current_event_t {
186 return current_event_t{executor};
187 }
188
189 class promise_base {
190 executor_ref executor_;
191 std::coroutine_handle<promise_base> continuation_ = nullptr;
192
193 public:
194 // Not having this constructor marked inline messes with coroutine
195 // HALO. (Hours 'wasted': many)
196 inline explicit promise_base(executor_ref executor)
197 : executor_{executor}
198 {}
199
200 [[nodiscard]] inline auto executor() const -> executor& {
201 return *executor_;
202 }
203
204 inline auto base_handle() -> std::coroutine_handle<promise_base> {
205 return std::coroutine_handle<promise_base>::from_promise(*this);
206 }
207
208 [[nodiscard]] inline auto continuation() const -> std::coroutine_handle<promise_base> {
209 return continuation_;
210 }
211 inline auto set_continuation(std::coroutine_handle<promise_base> c) -> void {
212 continuation_ = c;
213 }
214 };
215
216 struct position {
217 std::size_t line;
218 std::size_t col;
219 };
220
221 class executor {
222 XML_Parser p_;
223 std::exception_ptr ex_ = nullptr;
224 std::coroutine_handle<promise_base> continuation_ = nullptr;
225 std::vector<std::optional<std::string>> default_namespace_;
226 std::unordered_map<std::string_view, std::vector<std::string>> namespaces_;
227 std::optional<event> ev_;
228 bool advance_ = true;
229
230 inline auto try_handle_event(event ev) noexcept -> void {
231 assert(!ex_);
232
233 try {
234 ev_ = std::move(ev);
235 } catch (...) {
236 ex_ = std::current_exception();
237 return;
238 }
239 advance_ = false;
240 if (!continuation_) {
241 // Parser returned (all subparsers are done) and has set the continuation to nullptr.
242 if (auto s = XML_StopParser(p_, /* resumable */ false); s != XML_STATUS_OK) {
243 ex_ = std::make_exception_ptr(std::runtime_error{"unexpected error when stopping XML parser"});
244 return;
245 }
246 ex_ = std::make_exception_ptr(std::runtime_error{"parser did not consume entire XML document"});
247 return;
248 }
249 continuation_.resume();
250 if (ex_) {
251 // Not sure if it's useful to report this error.
252 std::ignore = XML_StopParser(p_, /* resumable */ false);
253 }
254 }
255
256 static auto handle_start_element(void* ctx, char const* name, char const** attrs) noexcept -> void {
257 auto qname = detail::split_name(name);
258 static_cast<executor*>(ctx)->try_handle_event(start_element_event{
259 .name = qname,
260 .attrs = attribute_view{qname.ns_uri, attrs},
261 });
262 }
263 static auto handle_end_element(void* ctx, char const* name) noexcept -> void {
264 static_cast<executor*>(ctx)->try_handle_event(end_element_event{
265 .name = detail::split_name(name),
266 });
267 }
268 static auto handle_character_data(void* ctx, char const* s, int len) noexcept -> void {
269 static_cast<executor*>(ctx)->try_handle_event(character_data_event{
270 .data = std::string_view{s, static_cast<std::size_t>(len)},
271 });
272 }
273 static auto handle_processing_instructions(void* ctx, char const* target, char const* data) noexcept -> void {
274 static_cast<executor*>(ctx)->try_handle_event(processing_instructions_event{
275 .target = util::lazy_zstring_view{target},
276 .data = util::lazy_zstring_view{data},
277 });
278 }
279 static auto handle_external_entity_ref(XML_Parser, char const* /* context */, char const* /* base */, char const* /* system_id */, char const* /* public_id */) noexcept -> int {
280 return XML_STATUS_ERROR;
281 }
282 static auto handle_start_namespace_decl(void* ctx, char const* prefix, char const* uri) noexcept -> void {
283 if (prefix) {
284 static_cast<executor*>(ctx)->namespaces_[std::string_view{prefix}].emplace_back(uri);
285 } else {
286 static_cast<executor*>(ctx)->default_namespace_.push_back(uri ? std::make_optional<std::string>(uri) : std::nullopt);
287 }
288 }
289 static auto handle_end_namespace_decl(void* ctx, char const* prefix) noexcept -> void {
290 if (prefix) {
291 static_cast<executor*>(ctx)->namespaces_[std::string_view{prefix}].pop_back();
292 } else {
293 static_cast<executor*>(ctx)->default_namespace_.pop_back();
294 }
295 }
296 static auto handle_xml_decl(void * ctx, char const* version, char const* encoding, int standalone) noexcept -> void {
297 static_cast<executor*>(ctx)->try_handle_event(xml_decl_event{
298 .version = util::lazy_zstring_view{version},
299 .encoding = util::lazy_zstring_view{encoding},
300 .standalone = standalone < 0 ? std::nullopt : std::make_optional(standalone > 0),
301 });
302 }
303
304 inline auto advance_flag() -> bool {
305 return advance_;
306 }
307 inline auto set_exception(std::exception_ptr ex) -> void {
308 ex_ = std::move(ex);
309 }
310 [[nodiscard]] inline auto take_exception() -> std::exception_ptr {
311 return std::exchange(ex_, nullptr);
312 }
313
314 template<class T> friend class promise;
315
316 public:
317 executor();
318
319 executor(executor const&) = delete;
320 executor(executor&&) = delete;
321 auto operator=(executor const&) -> executor& = delete;
322 auto operator=(executor&&) -> executor& = delete;
323
324 ~executor();
325
326 inline auto set_continuation(std::coroutine_handle<promise_base> c) -> void {
327 continuation_ = c;
328 }
329 inline auto set_advance_flag() -> void {
330 if (!ev_ || !std::holds_alternative<eof_event>(ev_.value())) {
331 advance_ = true;
332 }
333 }
334 inline auto event() const -> std::optional<event> const& {
335 return ev_;
336 }
337 inline auto resolve_namespace(std::string_view prefix) -> std::optional<std::string_view> {
338 if (auto it = namespaces_.find(prefix); it != namespaces_.end() && !it->second.empty())
339 return it->second.back();
340 return std::nullopt;
341 }
342 [[nodiscard]] inline auto position() -> position {
343 return {
344 .line = XML_GetCurrentLineNumber(p_),
345 .col = XML_GetCurrentColumnNumber(p_),
346 };
347 }
348
349 auto start() -> void;
350 auto read(std::string_view xml, bool is_final) -> void;
351 auto end() -> void;
352 };
353
354 template<class T>
355 class promise_returnable : public promise_base {
356 std::optional<T> returned_value_;
357
358 public:
359 using result_type = T;
360 using promise_base::promise_base;
361
362 template<class U>
363 auto return_value(U&& v) -> void {
364 returned_value_.emplace(std::forward<U>(v));
365 }
366 auto returned_value() -> T&& {
367 if (!returned_value_)
368 throw std::runtime_error{"XML coroutine did not return"};
369 return std::forward<T>(returned_value_.value());
370 }
371 };
372
373 template<>
374 class promise_returnable<void> : public promise_base {
375 public:
376 using result_type = void;
377 using promise_base::promise_base;
378
379 auto return_void() -> void {}
380 };
381
382 template<class T>
383 class promise : public promise_returnable<T> {
384 public:
385 // Called with all the coroutine's arguments.
386 // Ignoring all but the first argument, which should be the executor.
387 template<class... Args>
388 explicit promise(executor_ref executor, Args&&...)
389 : promise_returnable<T>{executor}
390 {}
391
392 auto handle() -> std::coroutine_handle<promise<T>> {
393 return {parser<T>::handle_type::from_promise(*this)};
394 }
395
396 auto get_return_object() -> parser<T> {
397 return parser<T>{handle()};
398 }
399
400 auto initial_suspend() {
401 return std::suspend_always{};
402 }
403 auto final_suspend() noexcept {
404 struct awaiter {
405 std::coroutine_handle<> h_;
406
407 [[nodiscard]] constexpr auto await_ready() const noexcept -> bool { return false; }
408 auto await_suspend(std::coroutine_handle<>) -> std::coroutine_handle<> { return h_; }
409 constexpr auto await_resume() const noexcept -> void { return; }
410 };
411 if (this->continuation()) {
412 return awaiter{this->continuation()};
413 } else {
414 this->executor().set_continuation(nullptr);
415 return awaiter{std::noop_coroutine()};
416 }
417 }
418
419 auto unhandled_exception() -> void {
420 this->executor().set_exception(std::current_exception());
421 }
422
423 auto await_transform(current_event_t const& req) {
424 struct awaiter {
425 executor_ref executor_;
426
427 [[nodiscard]] constexpr auto await_ready() const noexcept -> bool {
428 return !executor_->advance_flag();
429 }
430 auto await_suspend(std::coroutine_handle<promise<T>> h) -> void {
431 executor_->set_continuation(h.promise().base_handle());
432 }
433 [[nodiscard]] auto await_resume() const -> event {
434 assert(executor_->event());
435 return executor_->event().value();
436 }
437 };
438 return awaiter{req.executor};
439 }
440
441 template<class U>
442 auto await_transform(parser<U> const& coro) {
443 struct [[clang::coro_await_elidable]] awaiter {
444 util::not_null<promise<U>*> next_;
445
446 [[nodiscard]] constexpr auto await_ready() const noexcept -> bool { return false; }
447 auto await_suspend(std::coroutine_handle<promise<T>> h) -> std::coroutine_handle<> {
448 // Passed coroutine handle will be the same as parser<T>::handle_type::from_promise(*this)
449 next_->set_continuation(h.promise().base_handle());
450 return next_->handle();
451 }
452 auto await_resume() -> U {
453 // Promise is still valid since coroutine frame is still alive (and suspended):
454 // control was transferred back to this coroutine via symmetric transfer in
455 // final_suspend(). Assuming that the destructor for coro still needs to run.
456 if (auto ex = next_->executor().take_exception()) {
457 std::rethrow_exception(ex);
458 } else {
459 if constexpr (!std::is_void_v<U>) {
460 return std::move(next_->returned_value());
461 }
462 }
463 }
464 };
465 return awaiter{util::not_null{&coro.promise()}};
466 }
467 };
468
469 // Helpers for handling XML documents. Non-polymorphic functions
470 // should be marked inline to allow HALO across TU boundaries.
471
472 template<class T>
473 concept unconstrained = true;
474
475 template<class T, template<class U> concept C>
476 concept parser_of = requires {
477 typename T::result_type;
478 requires std::same_as<parser<typename T::result_type>, T>;
479 requires C<typename T::result_type>;
480 };
481
482 template<parser_of<unconstrained> T>
483 using parser_result_t = T::result_type;
484
485 template<class T, class... Args>
486 concept parser_invocable = std::invocable<T, Args...> && parser_of<std::invoke_result_t<T, Args...>, unconstrained>;
487
488 template<class Fn, class... Args>
489 requires parser_invocable<Fn, Args...>
490 using parser_invoke_result_t = parser_result_t<std::invoke_result_t<Fn, Args...>>;
491
492 template<event_type T> auto expect_event(executor_ref e) -> parser<T> {
493 auto ev = co_await current_event(e);
494 if (!std::holds_alternative<T>(ev)) {
495 auto pos = e->position();
496 throw std::runtime_error{std::format("at {}:{}: unexpected event type, have {}", pos.line, pos.col, ev.index())};
497 }
498 e->set_advance_flag();
499 co_return std::get<T>(ev);
500 }
501
502 inline auto expect_start_element(executor_ref e, qname_view want) -> parser<attribute_view> {
503 auto ev = co_await expect_event<start_element_event>(e);
504 if (ev.name != want) {
505 auto pos = e->position();
506 throw std::runtime_error{std::format("at {}:{}: unexpected element started", pos.line, pos.col)};
507 }
508 co_return ev.attrs;
509 }
510
511 inline auto allow_start_element(executor_ref e, qname_view want) -> parser<std::optional<attribute_view>> {
512 auto ev = co_await current_event(e);
513 if (auto const* pev = std::get_if<start_element_event>(&ev)) {
514 if (pev->name == want) {
515 e->set_advance_flag();
516 co_return pev->attrs;
517 }
518 }
519 co_return std::nullopt;
520 }
521
522 inline auto expect_end_element(executor_ref e, qname_view want) -> parser<void> {
523 auto ev = co_await expect_event<end_element_event>(e);
524 if (ev.name != want) {
525 throw std::runtime_error{"unexpected element ended"};
526 }
527 }
528
529 inline auto ignore_whitespace(executor_ref e) -> parser<void> {
530 auto all_whitespace = [](std::string_view s) -> bool {
531 for (auto c : s)
532 if (c != ' ' && c != '\r' && c != '\n' && c != '\t')
533 return false;
534 return true;
535 };
536
537 while (true) {
538 auto ev = co_await current_event(e);
539 if (auto const* pev = std::get_if<character_data_event>(&ev); pev && all_whitespace(pev->data)) {
540 e->set_advance_flag();
541 } else {
542 co_return;
543 }
544 }
545 }
546
547 auto expect_element(executor_ref e, qname_view want, parser_invocable<executor_ref, attribute_view> auto p)
548 -> parser<parser_invoke_result_t<decltype(p), executor_ref, attribute_view>>
549 {
550 co_await ignore_whitespace(e);
551 auto attrs = co_await expect_start_element(e, want);
552 auto&& res = co_await p(e, attrs);
553 co_await expect_end_element(e, want);
554 co_await ignore_whitespace(e);
555 co_return std::forward<parser_invoke_result_t<decltype(p), executor_ref, attribute_view>>(res);
556 }
557
558 auto allow_element(executor_ref e, qname_view want, parser_invocable<executor_ref, attribute_view> auto p)
559 -> parser<std::optional<parser_invoke_result_t<decltype(p), executor_ref, attribute_view>>>
560 {
561 co_await ignore_whitespace(e);
562 if (auto mattrs = co_await allow_start_element(e, want)) {
563 auto&& res = co_await p(e, *mattrs);
564 co_await expect_end_element(e, want);
565 co_await ignore_whitespace(e);
566 co_return std::make_optional(std::forward<parser_invoke_result_t<decltype(p), executor_ref, attribute_view>>(res));
567 }
568 co_return std::nullopt;
569 }
570
571 auto allow_element(executor_ref e, qname_view want, parser_invocable<executor_ref, attribute_view> auto p)
572 -> parser<bool>
573 requires std::is_void_v<parser_invoke_result_t<decltype(p), executor_ref, attribute_view>>
574 {
575 co_await ignore_whitespace(e);
576 if (auto mattrs = co_await allow_start_element(e, want)) {
577 co_await p(e, *mattrs);
578 co_await expect_end_element(e, want);
579 co_await ignore_whitespace(e);
580 co_return true;
581 }
582 co_return false;
583 }
584
585 inline auto ignore_contents(executor_ref e, std::optional<qname_view> muntil = std::nullopt) -> parser<void> {
586 std::size_t depth = 0;
587 while (true) {
588 auto ev = co_await current_event(e);
589 if (auto* pev = std::get_if<start_element_event>(&ev)) {
590 if (depth == 0 && muntil && pev->name == *muntil) {
591 co_return;
592 } else {
593 depth++;
594 }
595 } else if (std::holds_alternative<end_element_event>(ev)) {
596 if (depth == 0) {
597 co_return;
598 } else {
599 depth--;
600 }
601 }
602 e->set_advance_flag();
603 }
604 }
605 inline auto ignore_element_contents(executor_ref e, attribute_view) -> parser<void> {
606 co_await ignore_contents(e);
607 }
608
609 inline auto read_string(executor_ref e) -> parser<std::string> {
610 std::string s;
611 while (true) {
612 auto ev = co_await current_event(e);
613 if (auto* pev = std::get_if<character_data_event>(&ev)) {
614 e->set_advance_flag();
615 s += pev->data;
616 } else {
617 co_return s;
618 }
619 }
620 }
621 inline auto read_string_contents(executor_ref e, attribute_view) -> parser<std::string> {
622 co_return co_await read_string(e);
623 }
624
625 template<auto f>
626 auto hohalo() {
627 return []<class... Args>(Args&&... args) -> std::invoke_result_t<decltype(f), Args...> {
628 co_return co_await f(std::forward<Args>(args)...);
629 };
630 }
631
632} // namespace routemon::xml
generated by cgit v1.3 (git 2.53.0) at 2026-09-10 12:22:47 +0000