add getKeys to json lib

HOL-Theorem-Prover · Oct 16, 2024 · 5c95ae6 · 5c95ae6
1 parent 29bcfcf
commit 5c95ae6
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 0 deletions.
diff --git a/examples/json/Json.sig b/examples/json/Json.sig
@@ -26,6 +26,9 @@ sig
   val getObject      : json -> string -> json option
   val getObject'     : json -> string -> json
 
+  val getKeys        : json -> (string list) option
+  val getKeys'       : json -> string list
+
   val getBool        : json -> bool option
   val getBool'       : json -> bool
 

diff --git a/examples/json/Json.sml b/examples/json/Json.sml
@@ -290,6 +290,17 @@ fun getObject' json k =
         SOME v => v
      | NONE => raise ERR "getObject'" "expects object."
 
+
+fun getKeys json =
+    case json of
+        AList l => SOME (map #1 l)
+      | _ => NONE
+
+fun getKeys' json =
+    case json of
+        AList l => map #1 l
+      | _ =>  raise ERR "getKeys'" "expects object."
+
 fun getBool json =
   case json of
       Boolean b => SOME b
@@ -349,6 +360,8 @@ fun foldArray' json (f: json -> 'a) =
       | NONE => raise ERR "foldArray'" "expects value."
 
 (* val json = hd (#1 (parse ([],Substring.full "{\"foo\" : [1, 23, 4], \"bar\" : 2}"))) *)
+(* val keys = getKeys json *)
+(* val keys' = getKeys' json *)
 (* val foo = getObject json "foo" *)
 (* val foo' = getObject' json "foo" *)
 (* val foo_ints = foldlArray foo' getInt *)