Add map/bind functions for s-expression decoders

src/portableML/HOLsexp.sig

@@ -30,6 +30,8 @@ sig
                      ('a * 'b * 'c * 'd) decoder
   val list_decode : 'a decoder -> 'a list decoder
   val tagged_decode : string -> 'a decoder -> 'a decoder
+  val map_decode : ('a -> 'b) -> 'a decoder -> 'b decoder
+  val bind_decode : 'a decoder -> ('a -> 'b option) -> 'b decoder
 
 
   val printer : t HOLPP.pprinter

src/portableML/HOLsexp.sml

@@ -17,6 +17,11 @@ struct
   val fromFile = HOLsexp_parser.raw_read_file
   val fromStream = HOLsexp_parser.raw_read_stream
 
+  fun map_decode f d = Option.map f o d
+  fun bind_decode d f x =
+      case d x of
+          NONE => NONE
+        | SOME y => f y
   fun r3_to_p12 (x,y,z) = (x, (y, z))
   fun p12_to_r3 (x,(y,z)) = (x,y,z)
   fun pair_encode (a,b) (x,y) = Cons(a x, b y)
@@ -32,7 +37,7 @@ struct
           Cons(Symbol s', rest) => if s = s' then SOME rest
                                    else NONE
         | _ => NONE
-  fun tagged_decode s dec t = Option.mapPartial dec (dest_tagged s t)
+  fun tagged_decode s dec = bind_decode (dest_tagged s) dec
 
   fun list_encode enc els = List (map enc els)
   fun break_list s =
@@ -70,13 +75,12 @@ struct
       (fn (u,v,w,x) => (u,(v,(w,x))))
   fun singleton [a] = SOME a
     | singleton _ = NONE
-  fun sing_decode d =
-      Option.mapPartial singleton o list_decode d
+  fun sing_decode d = bind_decode (list_decode d) singleton
   fun pair3_decode (a,b,c) =
-      Option.map p12_to_r3 o pair_decode(a, pair_decode(b,sing_decode c))
+      map_decode p12_to_r3 (pair_decode(a, pair_decode(b,sing_decode c)))
   fun pair4_decode (a,b,c,d) =
-      Option.map (fn (u,(v,(w,x))) => (u,v,w,x)) o
-      pair_decode(a,pair_decode(b,pair_decode(c,sing_decode d)))
+      map_decode (fn (u,(v,(w,x))) => (u,v,w,x))
+                 (pair_decode(a,pair_decode(b,pair_decode(c,sing_decode d))))
 
   fun is_list s =
       case s of

src/postkernel/TheoryReader.sml

@@ -41,8 +41,9 @@ val dep_decode = let
         | (n,[i]) :: rest => SOME{head = (n,i), deps = rest}
         | _ => NONE
 in
-  Option.mapPartial depmunge o
-  list_decode (pair_decode(string_decode, list_decode int_decode))
+  bind_decode (
+    list_decode (pair_decode(string_decode, list_decode int_decode))
+  ) depmunge
 end
 val deptag_decode = let open HOLsexp in
                       pair_decode(dep_decode, list_decode string_decode)
@@ -53,8 +54,9 @@ val thm_decode =
       fun thmmunge(s,(di,tags),tms) =
           {name = s, depinfo = di, tagnames = tags, encoded_hypscon = tms}
     in
-      Option.map thmmunge o
-      pair3_decode (string_decode, deptag_decode, list_decode string_decode)
+      map_decode thmmunge (
+        pair3_decode (string_decode, deptag_decode, list_decode string_decode)
+      )
     end
 
 exception TheoryReader of string
@@ -101,8 +103,9 @@ fun string_to_class "A" = SOME DB.Axm
   | string_to_class _ = NONE
 
 fun class_decode c =
-    Option.map (List.map (fn i => (i, c))) o
-    HOLsexp.list_decode HOLsexp.int_decode
+    HOLsexp.map_decode (List.map (fn i => (i, c))) (
+      HOLsexp.list_decode HOLsexp.int_decode
+    )
 
 fun load_thydata thyname path =
   let

src/postkernel/ThyDataSexp.sig

@@ -71,6 +71,7 @@ val tag_encode : string -> ('a -> t) -> ('a -> t)
 val tag_decode : string -> 'a dec -> 'a dec
 
 val || : 'a dec * 'a dec -> 'a dec
+val >> : 'a dec * ('a -> 'b) -> 'b dec
 val first : 'a dec list -> 'a dec
 
 end