1structure HOLsexp :> HOLsexp =
2struct
3
4
5  open HOLsexp_dtype
6
7  type 'a encoder = 'a -> t
8  type 'a decoder = t -> 'a option
9
10  val Nil = Symbol "nil"
11  val Quote = Symbol "quote"
12
13  val List = List.foldr Cons Nil
14
15  val scan = HOLsexp_parser.scan
16  val fromString = StringCvt.scanString scan
17  val fromFile = HOLsexp_parser.raw_read_file
18  val fromStream = HOLsexp_parser.raw_read_stream
19
20  fun r3_to_p12 (x,y,z) = (x, (y, z))
21  fun p12_to_r3 (x,(y,z)) = (x,y,z)
22  fun pair_encode (a,b) (x,y) = Cons(a x, b y)
23  fun pair_decode (a, b) (Cons(t1,t2)) =
24      (case a t1 of
25           NONE => NONE
26         | SOME v1 => Option.map (fn v2 => (v1,v2)) (b t2))
27    | pair_decode _ _ = NONE
28
29  fun tagged_encode s enc v = Cons(Symbol s, enc v)
30  fun dest_tagged s t =
31      case t of
32          Cons(Symbol s', rest) => if s = s' then SOME rest
33                                   else NONE
34        | _ => NONE
35  fun tagged_decode s dec t = Option.mapPartial dec (dest_tagged s t)
36
37  fun list_encode enc els = List (map enc els)
38  fun break_list s =
39      let
40        fun recurse A s =
41            case s of
42                Cons(s1, s2) => recurse (s1::A) s2
43              | _ => (List.rev A, s)
44      in
45        recurse [] s
46      end
47  fun strip_list s =
48      let val(sexps, last) = break_list s
49      in
50        if last = Nil then (sexps, NONE)
51        else (sexps, SOME last)
52      end
53  fun list_decode dec t =
54      let
55        fun recurse A els =
56            case els of
57                [] => SOME (List.rev A)
58              | h::t => Option.mapPartial (fn v => recurse (v::A) t) (dec h)
59      in
60        case strip_list t of
61            (els, NONE) => recurse [] els
62          | _ => NONE
63      end
64
65  fun singencode a v = List[a v]
66  fun pair3_encode (a,b,c) =
67      pair_encode(a,pair_encode(b,singencode c)) o r3_to_p12
68  fun pair4_encode (a,b,c,d) =
69      pair_encode(a,pair_encode(b,pair_encode(c,singencode d))) o
70      (fn (u,v,w,x) => (u,(v,(w,x))))
71  fun singleton [a] = SOME a
72    | singleton _ = NONE
73  fun sing_decode d =
74      Option.mapPartial singleton o list_decode d
75  fun pair3_decode (a,b,c) =
76      Option.map p12_to_r3 o pair_decode(a, pair_decode(b,sing_decode c))
77  fun pair4_decode (a,b,c,d) =
78      Option.map (fn (u,(v,(w,x))) => (u,v,w,x)) o
79      pair_decode(a,pair_decode(b,pair_decode(c,sing_decode d)))
80
81  fun is_list s =
82      case s of
83          Cons(_, s') => is_list s'
84        | Symbol "nil" => true
85        | _ => false
86
87  fun int_decode (Integer i) = SOME i
88    | int_decode _ = NONE
89
90  fun symbol_decode (Symbol s) = SOME s
91    | symbol_decode _ = NONE
92  fun string_decode (String s) = SOME s
93    | string_decode _ = NONE
94
95
96
97  fun mem x s = CharVector.exists (fn c => c = x) s
98  fun printer t =
99      let
100        open HOLPP
101        fun symok c = mem c "-+_#!"
102      in
103        case t of
104            Symbol s =>
105            if size s > 0 andalso
106               (CharVector.all (fn c => Char.isAlpha c orelse symok c) s orelse
107                not (Char.isDigit (String.sub(s,0))) andalso
108                CharVector.all (fn c => Char.isAlpha c orelse Char.isDigit c) s)
109            then
110              add_string s
111            else
112              add_string ("|" ^ String.translate
113                            (fn #"|" => "\\|" | #"\n" => "\\n" | c => str c)
114                            s ^ "|")
115          | Integer i => add_string (if i < 0 then "-" ^ Int.toString (~i)
116                                     else Int.toString i)
117          | String s => add_string (Portable.mlquote s)
118          | Cons _ =>
119            (let val (els, last) = break_list t
120             in
121               block INCONSISTENT 1 (
122                 add_string "(" ::
123                 pr_list printer [add_break(1,0)] els @
124                 (case last of
125                      Symbol "nil" => [add_string ")"]
126                    | t => [add_string " .", add_break(1,0), printer t,
127                            add_string ")"])
128               )
129             end)
130      end
131
132end
133