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