20200703 src/util.sml (timestamp à la RFC3339 einlesen; Date.toTime: richtige Zeitzonenvorzeicheninterpretation hängt von der SML/NJ Version ab)

src/Makefile.in

@@ -13,7 +13,7 @@ promconfig.sml: promconfig.sml.in
 nodes2prom: nodes2prom.%%HEAP_SUFFIX%%
 	heap2exec nodes2prom.%%HEAP_SUFFIX%% nodes2prom || { ../conf/substitute.sh runheap.in $@ && chmod +x $@ ; }
 
-nodes2prom.%%HEAP_SUFFIX%%: promconfig.sml nodes2prom.cm nodes2prom.sml json_lib
+nodes2prom.%%HEAP_SUFFIX%%: promconfig.sml nodes2prom.cm nodes2prom.sml util.cm util.sml json_lib
 	ml-build nodes2prom.cm Main.main nodes2prom
 
 graph2prom: graph2prom.%%HEAP_SUFFIX%%

src/nodes2prom.cm

@@ -4,5 +4,6 @@ is
 	$/basis.cm
 	$/smlnj-lib.cm
 	JSON/json-lib.cm
+	util.cm
 	promconfig.sml
 	nodes2prom.sml

src/nodes2prom.sml

@@ -14,6 +14,7 @@ struct
 	val stats_prefix = PC.stats_prefix
 
 	val timestamp = ref (LargeInt.toString (Time.toMilliseconds (Time.now ())))
+	val timeFromRFC3339 = Util.timeFromRFC3339
 
 	val newline = String.str #"\n"
 	val summary_header = [
@@ -85,33 +86,11 @@ struct
 		      0
 		      (String.tokens (fn c => c = #".") firmware)
 
-	fun timestring2time ts = (* "timestamp" : "2017-10-01T18:49:11+02:00" *)
-		let val tsfields = String.tokens (fn c => c = #"-" orelse c = #"T" orelse c = #":" orelse c = #"+") ts
-		    val tsints = map (valOf o Int.fromString) tsfields
-		    fun int2month i =
-			let open Date
-			    val months = [ Jan, Feb, Mar, Apr, May, Jun, Jul, Aug, Sep, Oct, Nov, Dec ]
-			in List.nth (months, i - 1)
-			end
-		    val tsdate =
-			Date.date {
-				year = List.nth (tsints, 0),
-				month = int2month (List.nth (tsints, 1)),
-				day = List.nth (tsints, 2),
-				hour = List.nth (tsints, 3),
-				minute = List.nth (tsints, 4),
-				second = List.nth (tsints, 5),
-				(* Basis/date.html:
-				   ... offset reports time zone information as the amount of time west [sic!] of UTC. *)
-				offset = SOME (Time.fromSeconds (~1 * 60 * Int.toLarge ((60 * List.nth (tsints, 6) + List.nth (tsints, 7))))) }
-		in Date.toTime tsdate
-		end
-
 	fun get_version obj = JU.asInt (JU.lookupField obj "version")
 
 	fun get_timestamp obj =
 		let val tsstring = JU.asString (JU.lookupField obj "timestamp")
-		    val tstime = timestring2time tsstring
+		    val tstime = timeFromRFC3339 tsstring
 		in timestamp := LargeInt.toString (Time.toMilliseconds tstime)
 		end
 		handle exn => json_handler ("get_timestamp") exn
@@ -170,8 +149,8 @@ struct
 		    val flags = JU.lookupField node "flags"
 		    val online = JU.asBool (JU.lookupField flags "online")
 		    val uplink = JU.asBool (JU.lookupField flags "uplink")
-		    val lastseen = timestring2time (JU.asString (JU.lookupField node "lastseen"))
-		    val firstseen = timestring2time (JU.asString (JU.lookupField node "firstseen"))
+		    val lastseen = timeFromRFC3339 (JU.asString (JU.lookupField node "lastseen"))
+		    val firstseen = timeFromRFC3339 (JU.asString (JU.lookupField node "firstseen"))
 		in SOME
 		   ({	clients = clients,
 			online = online,

src/util.cm

@@ -0,0 +1,6 @@
+library
+	structure Util
+is
+	$/basis.cm
+	$smlnj/internal/smlnj-version.cm
+	util.sml

src/util.sml

@@ -0,0 +1,189 @@
+structure Util = struct
+
+(* <https://tools.ietf.org/html/rfc3339> *)
+
+(* e.g. "2017-10-01T18:49:11+02:00", or your own timestamp: *)
+(* date "+%FT%T`date +%z | sed -E -e 's/(...)(..)/\1:\2/'`" *)
+
+
+fun cmpList cmp ([], []) = EQUAL
+  | cmpList cmp ([], y :: r) = LESS
+  | cmpList cmp (x :: r, []) = GREATER
+  | cmpList cmp (x :: r1, y :: r2) =
+	case cmp (x, y)
+	  of EQUAL => cmpList cmp (r1, r2)
+	   | unequal => unequal
+
+fun fixOffset offset =
+	let val smlnj_version = SMLNJVersion.version
+	in case cmpList Int.compare
+			(#version_id smlnj_version,
+			 [110, 90])
+	   of LESS => ~ offset
+	    | _ => offset
+	end
+
+fun dateFromRFC3339 rfc3339 =
+	if size rfc3339 < 20
+	then raise Fail (
+		"fromRFC3339: expecting at least 20 characters, got " ^
+		(Int.toString (size rfc3339)))
+	else
+	let
+	val sz = size rfc3339
+	fun get_seperator name seplist pos =
+		let val c = String.sub (rfc3339, pos)
+		in	if List.exists (fn s => c = s) seplist
+			then c
+		   	else raise Fail (
+				"fromRFC3339: error parsing " ^ name ^
+				" at position " ^ (Int.toString pos) ^
+				", expecting one of the characters '" ^
+				(implode seplist) ^ "', got '" ^
+				(Char.toString c) ^ "'")
+		end
+	fun get_digits name from to =
+		let val sz = to - from + 1
+		    val s = substring (rfc3339, from, sz)
+		in if List.all Char.isDigit (explode s)
+			then valOf (Int.fromString s)
+			else raise Fail (
+				"fromRFC3339: Format error at position " ^
+				(Int.toString from) ^ ", expecting " ^
+				(Int.toString sz) ^ " digits, got \"" ^ s ^ "\"")
+		end
+	fun skip_fraction from =
+		if sz <= from
+		then raise Fail (
+			"fromRFC3339: expecting fraction, got end of string")
+		else
+		let val rest = String.extract (rfc3339, from, NONE)
+		    val (_, sum, count) =
+			foldl	(fn (c , dsc as (done, sum, count)) =>
+					if done
+					then dsc
+					else 	if Char.isDigit c
+						then	(false,
+							 10 * sum + (ord c - ord #"0"),
+							 count + 1)
+						else (true, sum, count))
+				(false, 0, 0)
+				(String.explode rest)
+		in if count > 0
+		   then from + count
+		   else raise Fail (
+				"fromRFC3339: Format error at position " ^
+				(Int.toString from) ^ ", expecting fraction digits, " ^
+				"got \"" ^ rest ^ "\"")
+		end
+	fun int2month i =
+		let open Date
+		    val months = #[ Jan, Feb, Mar, Apr, May, Jun, Jul, Aug, Sep, Oct, Nov, Dec ]
+		in Vector.sub (months, i - 1)
+		end
+
+	val year = get_digits "year" 0 3
+	val _ = get_seperator "month" [#"-"] 4
+	val monthint = get_digits "month" 5 6
+	val month = int2month monthint
+	val _ = get_seperator "day" [#"-"] 7
+	val day = get_digits "day" 8 9
+	val _ = get_seperator "hour" [#"T", #"t"] 10
+	val hour = get_digits "hour" 11 12
+	val _ = get_seperator "minute" [#":"] 13
+	val minute = get_digits "minute" 14 15
+	val _ = get_seperator "second" [#":"] 16
+	val second = get_digits "second" 17 18
+	val offsetpos =
+		case String.sub (rfc3339, 19)
+		  of #"Z" => 19
+		   | #"z" => 19
+		   | #"+" => 19
+		   | #"-" => 19
+		   | #"." => skip_fraction 20
+		   | c => raise Fail (
+			"rfc3339: mission impossible at position 19, got '" ^
+			(Char.toString c) ^ "'")
+	val offsettype =
+		if sz <= offsetpos
+		then raise Fail (
+			"fromRFC3339: expecting offsettype, got end of string")
+		else get_seperator "offsettype" [#"Z", #"z", #"+", #"-"] offsetpos
+	val offsettime =
+		if offsettype = #"Z" orelse offsettype = #"z"
+		then if sz = offsetpos + 1
+		     then Time.zeroTime
+		     else raise Fail (
+			"fromRFC3339: expecting end of string, got \"" ^
+			(String.extract (rfc3339, offsetpos + 1, NONE)) ^ "\"")
+		else if sz = offsetpos + 6
+		     then
+			let val offsethour = get_digits "offsethour" (offsetpos + 1) (offsetpos + 2)
+			    val _ = get_seperator "offsetminute" [#":"] (offsetpos + 3)
+			    val offsetminute = get_digits "offsetminute" (offsetpos + 4) (offsetpos + 5)
+			    val offsetseconds' = 60 * (60 * offsethour + offsetminute)
+			    val offsetseconds = fixOffset (
+					if offsettype = #"+"
+			   		then offsetseconds'
+					else ~ offsetseconds')
+			in Time.fromSeconds (Int.toLarge offsetseconds)
+			end
+		     else raise Fail (
+			"fromRFC3339: expecting hh:mm, got \"" ^
+			(String.extract (rfc3339, offsetpos + 1, NONE)) ^ "\"")
+
+	in Date.date
+		{ year = year, month = month, day = day,
+	   	  hour = hour, minute = minute, second = second,
+		  offset = SOME offsettime }
+	end
+
+	val timeFromRFC3339 = Date.toTime o dateFromRFC3339
+
+end (* structure Util *)
+
+(*
+Control.Print.printDepth := 23;
+
+fromRFC3339 "2017-10-01T18:49:11+02:00";
+fromRFC3339 "2017-10-01T16:49:11Z";
+fromRFC3339 "2017-10-01T18:49:11.123-05:00";
+
+fromRFC3339 "2017-10-01T18:49:11.666+02:00";
+fromRFC3339 "2017-10-01T18:49:11.+02:00";
+fromRFC3339 "2017-10-01T16:49:11Z+02:00";
+fromRFC3339 "2017-10-01T16:49:11+0200";
+
+val d = fromRFC3339 "2017-10-01T18:49:11+02:00";
+val t = Date.toTime d;
+TIME {usec=1506876551000000} : Time.time
+% date -r 1506876551
+So.  1 Okt. 2017 18:49:11 CEST
+timestring2time "2017-10-01T18:49:11+02:00";
+TIME {usec=1506862151000000} : Time.time
+% date -r 1506862151
+So.  1 Okt. 2017 14:49:11 CEST
+
+*)
+
+(* RFC3339, 5.6:
+
+   date-fullyear   = 4DIGIT
+   date-month      = 2DIGIT  ; 01-12
+   date-mday       = 2DIGIT  ; 01-28, 01-29, 01-30, 01-31 based on
+                             ; month/year
+   time-hour       = 2DIGIT  ; 00-23
+   time-minute     = 2DIGIT  ; 00-59
+   time-second     = 2DIGIT  ; 00-58, 00-59, 00-60 based on leap second
+                             ; rules
+   time-secfrac    = "." 1*DIGIT
+   time-numoffset  = ("+" / "-") time-hour ":" time-minute
+   time-offset     = "Z" / time-numoffset
+
+   partial-time    = time-hour ":" time-minute ":" time-second
+                     [time-secfrac]
+   full-date       = date-fullyear "-" date-month "-" date-mday
+   full-time       = partial-time time-offset
+
+   date-time       = full-date "T" full-time
+*)