A Collection of Isabelle Programming Hacks
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 

764 lines
31 KiB

  1. (***********************************************************************************
  2. * Copyright (c) 2019 Achim D. Brucker
  3. *
  4. * All rights reserved.
  5. *
  6. * Redistribution and use in source and binary forms, with or without
  7. * modification, are permitted provided that the following conditions are met:
  8. *
  9. * * Redistributions of source code must retain the above copyright notice, this
  10. *
  11. * * Redistributions in binary form must reproduce the above copyright notice,
  12. * this list of conditions and the following disclaimer in the documentation
  13. * and/or other materials provided with the distribution.
  14. *
  15. * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
  16. * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
  17. * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
  18. * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
  19. * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
  20. * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
  21. * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  22. * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
  23. * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
  24. * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  25. *
  26. * SPDX-License-Identifier: BSD-2-Clause
  27. * Repository: https://git.logicalhacking.com/adbrucker/isabelle-hacks/
  28. * Dependencies: None (assert.thy is used for testing the theory but it is
  29. * not required for providing the functionality of this hack)
  30. ***********************************************************************************)
  31. (***********************************************************************************
  32. # Changelog
  33. This comment documents all notable changes to this file in a format inspired by
  34. [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres
  35. to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
  36. ## [Unreleased]
  37. - Improved representation of IEEE reals
  38. - Fixed serializer for definitions using equality from Pure
  39. ## [1.0.0] - 2019-01-21
  40. - Initial release
  41. ***********************************************************************************)
  42. chapter\<open>An Import/Export of JSON-like Formats for Isabelle/HOL\<close>
  43. theory
  44. "Nano_JSON"
  45. imports
  46. Complex_Main (* required for type real *)
  47. keywords
  48. "import_JSON" :: thy_decl
  49. and "definition_JSON" :: thy_decl
  50. and "serialize_JSON" :: thy_decl
  51. begin
  52. text\<open>
  53. This theory implements an import/export format for Isabelle/HOL that is inspired by
  54. JSON (JavaScript Object Notation). While the format defined in this theory is inspired
  55. by the JSON standard (@{url "https://www.json.org"}), it is not fully compliant. Most
  56. notably,
  57. \<^item> only basic support for Unicode characters
  58. \<^item> numbers are mapped to @{type "real"}, which is not a faithful representation of IEEE floating
  59. point numbers, moreover, we extended the abstract syntax to allow for representing integers as
  60. @{type "int"}.
  61. Still, our JSON-like import/expert should work with most real-world JSON files, i.e., simplifying
  62. the data exchange between Isabelle/HOL and tools that can read/write JSON.
  63. Overall, this theory should enable you to work with JSON encoded data in Isabelle/HOL without
  64. the need of implementing parsers or serialization in Isabelle/ML. You should be able to implement
  65. mapping from the Nano JSON HOL data types to your own data types on the level of Isabelle/HOL (i.e.,
  66. as executable HOL functions). Nevertheless, the provided ML routine that converts between the
  67. ML representation and the HOL representation of Nano JSON can also serve as a starting point
  68. for converting the ML representation to your own, domain-specific, HOL encoding.
  69. \<close>
  70. section\<open>Defining a JSON-like Data Structure\<close>
  71. text\<open>
  72. In this section
  73. \<close>
  74. datatype number = INTEGER int | REAL real
  75. datatype json = OBJECT "(string * json) list"
  76. | ARRAY "json list"
  77. | NUMBER "number"
  78. | STRING "string"
  79. | BOOL "bool"
  80. | NULL
  81. text\<open>
  82. Using the data type @{typ "json"}, we can now represent JSON encoded data easily in HOL:
  83. \<close>
  84. subsection\<open>Example\<close>
  85. definition example01::json where
  86. "example01 =
  87. OBJECT [(''menu'', OBJECT [(''id'', STRING ''file''), (''value'', STRING ''File''),
  88. (''popup'', OBJECT [(''menuitem'', ARRAY
  89. [OBJECT [(''value'', STRING ''New''), (''onclick'', STRING ''CreateNewDoc()'')],
  90. OBJECT [(''value'', STRING ''Open''), (''onclick'', STRING ''OpenDoc()'')],
  91. OBJECT [(''value'', STRING ''Close''), (''onclick'', STRING ''CloseDoc()'')]
  92. ])]
  93. )])]"
  94. text\<open>
  95. The translation of the data type @{typ "json"} to ML is straight forward. In addition, we also
  96. provide methods for converting JSON instances between the representation as Isabelle terms and
  97. the representation as ML data structure.
  98. \<close>
  99. subsection\<open>ML Implementation\<close>
  100. ML\<open>
  101. signature NANO_JSON_TYPE = sig
  102. datatype number = INTEGER of int | REAL of IEEEReal.decimal_approx
  103. datatype json = OBJECT of (string * json) list
  104. | ARRAY of json list
  105. | NUMBER of number
  106. | STRING of string
  107. | BOOL of bool
  108. | NULL
  109. val term_of_json: json -> term
  110. val json_of_term: term -> json
  111. end
  112. structure Nano_Json_Type : NANO_JSON_TYPE = struct
  113. datatype number = INTEGER of int | REAL of IEEEReal.decimal_approx
  114. datatype json = OBJECT of (string * json) list
  115. | ARRAY of json list
  116. | NUMBER of number
  117. | STRING of string
  118. | BOOL of bool
  119. | NULL
  120. fun ieee_real_to_rat_approx rat = let
  121. val _ = warning ("Conversion of (real) numbers is not JSON compliant.")
  122. (* val rat = Real.toDecimal r *)
  123. fun pow (_, 0) = 1
  124. | pow (x, n) = if n mod 2 = 0 then pow (x*x, n div 2)
  125. else x * pow (x*x, n div 2);
  126. fun rat_of_dec rat = let
  127. val sign = #sign rat
  128. val digits = #digits rat
  129. val exp = #exp rat
  130. fun numerator_of _ [] = 0
  131. | numerator_of c (x::xs) = x*pow(10,c) + (numerator_of (c+1) xs)
  132. val numerator_abs = numerator_of 0 (rev digits)
  133. val denominator = pow(10, (List.length digits - exp))
  134. in
  135. (if sign then ~ numerator_abs else numerator_abs, denominator)
  136. end
  137. in
  138. case #class rat of
  139. IEEEReal.ZERO => (0,0)
  140. | IEEEReal.SUBNORMAL => rat_of_dec rat
  141. | IEEEReal.NORMAL => rat_of_dec rat
  142. | IEEEReal.INF => error "Real is INF, not yet supported."
  143. | IEEEReal.NAN => error "Real is NaN, not yet supported."
  144. end
  145. fun mk_divide t1 t2 = @{const Rings.divide_class.divide (real)} $ t1 $ t2
  146. fun mk_real_num i = HOLogic.mk_number @{typ "Real.real"} i
  147. fun mk_real (p,q) = if q = 1 then mk_real_num p else mk_divide (mk_real_num p) (mk_real_num q)
  148. fun dest_real (@{const Rings.divide_class.divide (real)} $a$b) =
  149. Real.toDecimal(Real.fromInt(HOLogic.dest_number a |> snd)
  150. / Real.fromInt(HOLogic.dest_number b |> snd))
  151. | dest_real t = Real.toDecimal (Real.fromInt (HOLogic.dest_number t |> snd))
  152. fun term_of_json (OBJECT l) = @{const "OBJECT"}
  153. $(HOLogic.mk_list ((HOLogic.mk_prodT (HOLogic.stringT,@{typ "json"})))
  154. (map (fn (s,j) => HOLogic.mk_tuple[HOLogic.mk_string s, term_of_json j]) l))
  155. | term_of_json (ARRAY l) = @{const "ARRAY"}
  156. $(HOLogic.mk_list ( @{typ "json"}) (map term_of_json l))
  157. | term_of_json (NUMBER (INTEGER i)) = @{const "NUMBER"}
  158. $(@{const "INTEGER"}$(HOLogic.mk_number @{typ "int"} i))
  159. | term_of_json (NUMBER (REAL r)) = @{const "NUMBER"}
  160. $(@{const "REAL"}$(mk_real (ieee_real_to_rat_approx r)))
  161. | term_of_json (STRING s) = @{const "STRING"}$(HOLogic.mk_string s)
  162. | term_of_json (BOOL v) = @{const "BOOL"}$(if v then @{const "True"} else @{const "False"})
  163. | term_of_json (NULL) = @{const "NULL"}
  164. fun json_of_term t = let
  165. fun dest_key_value [string, json] = (HOLogic.dest_string string, json_of json)
  166. | dest_key_value _ = error "dest_key_value: not a key-value pair."
  167. and json_of (@{const "OBJECT"} $ l) = OBJECT (map (dest_key_value o HOLogic.strip_tuple) (HOLogic.dest_list l))
  168. | json_of (@{const "ARRAY"} $ l) = ARRAY (map json_of (HOLogic.dest_list l))
  169. | json_of (@{const "NUMBER"} $ @{const "INTEGER"} $ i) = (NUMBER (INTEGER (HOLogic.dest_numeral i)))
  170. | json_of (@{const "NUMBER"} $ @{const "REAL"} $ r) = (NUMBER (REAL (dest_real r)))
  171. | json_of (@{const "STRING"} $ s) = STRING (HOLogic.dest_string s)
  172. | json_of (@{const "BOOL"} $ @{const "True"}) = BOOL true
  173. | json_of (@{const "BOOL"} $ @{const "False"}) = BOOL true
  174. | json_of @{const "NULL"} = NULL
  175. | json_of _ = error "Term not supported in json_of_term."
  176. in
  177. if type_of t = @{typ "json"} then json_of t
  178. else error "Term not of type json."
  179. end
  180. end
  181. \<close>
  182. section\<open>Parsing Nano JSON\<close>
  183. text\<open>
  184. In this section, we define the infrastructure for parsing JSON-like data structures as
  185. well as for importing them into Isabelle/HOL. This implementation was inspired by the
  186. ``Simple Standard ML JSON parser'' from Chris Cannam.
  187. \<close>
  188. subsection\<open>ML Implementation\<close>
  189. subsubsection\<open>Lexer\<close>
  190. ML\<open>
  191. signature NANO_JSON_LEXER = sig
  192. structure T : sig
  193. datatype token = NUMBER of char list
  194. | STRING of string
  195. | BOOL of bool
  196. | NULL
  197. | CURLY_L
  198. | CURLY_R
  199. | SQUARE_L
  200. | SQUARE_R
  201. | COLON
  202. | COMMA
  203. val string_of_T : token -> string
  204. end
  205. val tokenize_string: string -> T.token list
  206. end
  207. structure Nano_Json_Lexer : NANO_JSON_LEXER = struct
  208. structure T = struct
  209. datatype token = NUMBER of char list
  210. | STRING of string
  211. | BOOL of bool
  212. | NULL
  213. | CURLY_L
  214. | CURLY_R
  215. | SQUARE_L
  216. | SQUARE_R
  217. | COLON
  218. | COMMA
  219. fun string_of_T t =
  220. case t of NUMBER digits => String.implode digits
  221. | STRING s => s
  222. | BOOL b => Bool.toString b
  223. | NULL => "null"
  224. | CURLY_L => "{"
  225. | CURLY_R => "}"
  226. | SQUARE_L => "["
  227. | SQUARE_R => "]"
  228. | COLON => ":"
  229. | COMMA => ","
  230. end
  231. fun lexer_error pos text = error (text ^ " at character position " ^
  232. Int.toString (pos - 1))
  233. fun token_error pos = lexer_error pos ("Unexpected token")
  234. fun bmp_to_utf8 cp = map (Char.chr o Word.toInt)
  235. (if cp < 0wx80
  236. then [cp]
  237. else if cp < 0wx800
  238. then [Word.orb(0wxc0, Word.>>(cp,0w6)),
  239. Word.orb(0wx8, Word.andb (cp, 0wx3f))]
  240. else if cp < 0wx10000
  241. then [Word.orb(0wxe0,Word.>>(cp, 0w12)),
  242. Word.orb(0wx80, Word.andb(Word.>>(cp,0w6), 0wx3f)),
  243. Word.orb(0wx80,Word.andb(cp, 0wx3f))]
  244. else error ("Invalid BMP point in bmp_to_utf8 " ^ (Word.toString cp)))
  245. fun lexNull pos acc (#"u" :: #"l" :: #"l" :: xs) =
  246. lex (pos + 3) (T.NULL :: acc) xs
  247. | lexNull pos _ _ = token_error pos
  248. and lexTrue pos acc (#"r" :: #"u" :: #"e" :: xs) =
  249. lex (pos + 3) (T.BOOL true :: acc) xs
  250. | lexTrue pos _ _ = token_error pos
  251. and lexFalse pos acc (#"a" :: #"l" :: #"s" :: #"e" :: xs) =
  252. lex (pos + 4) (T.BOOL false :: acc) xs
  253. | lexFalse pos _ _ = token_error pos
  254. and lexChar tok pos acc xs =
  255. lex pos (tok :: acc) xs
  256. and lexString pos acc cc =
  257. let datatype escaped = ESCAPED | NORMAL
  258. fun lexString' pos _ ESCAPED [] =
  259. lexer_error pos "End of input during escape sequence"
  260. | lexString' pos _ NORMAL [] =
  261. lexer_error pos "End of input during string"
  262. | lexString' pos text ESCAPED (x :: xs) =
  263. let fun esc c = lexString' (pos + 1) (c :: text) NORMAL xs
  264. in case x of
  265. #"\"" => esc x
  266. | #"\\" => esc x
  267. | #"/" => esc x
  268. | #"b" => esc #"\b"
  269. | #"f" => esc #"\f"
  270. | #"n" => esc #"\n"
  271. | #"r" => esc #"\r"
  272. | #"t" => esc #"\t"
  273. | _ => lexer_error pos ("Invalid escape \\" ^
  274. Char.toString x)
  275. end
  276. | lexString' pos text NORMAL (#"\\" :: #"u" ::a::b::c::d:: xs) =
  277. if List.all Char.isHexDigit [a,b,c,d]
  278. then case Word.fromString ("0wx" ^ (String.implode [a,b,c,d])) of
  279. SOME w => (let val utf = rev (bmp_to_utf8 w) in
  280. lexString' (pos + 6) (utf @ text)
  281. NORMAL xs
  282. end
  283. handle Fail err => lexer_error pos err)
  284. | NONE => lexer_error pos "Invalid Unicode BMP escape sequence"
  285. else lexer_error pos "Invalid Unicode BMP escape sequence"
  286. | lexString' pos text NORMAL (x :: xs) =
  287. if Char.ord x < 0x20
  288. then lexer_error pos "Invalid unescaped control character"
  289. else
  290. case x of
  291. #"\"" => (rev text, xs, pos + 1)
  292. | #"\\" => lexString' (pos + 1) text ESCAPED xs
  293. | _ => lexString' (pos + 1) (x :: text) NORMAL xs
  294. val (text, rest, newpos) = lexString' pos [] NORMAL cc
  295. in
  296. lex newpos (T.STRING (String.implode text) :: acc) rest
  297. end
  298. and lexNumber firstChar pos acc cc =
  299. let val valid = String.explode ".+-e"
  300. fun lexNumber' pos digits [] = (rev digits, [], pos)
  301. | lexNumber' pos digits (x :: xs) =
  302. if x = #"E" then lexNumber' (pos + 1) (#"e" :: digits) xs
  303. else if Char.isDigit x orelse List.exists (fn c => x = c) valid
  304. then lexNumber' (pos + 1) (x :: digits) xs
  305. else (rev digits, x :: xs, pos)
  306. val (digits, rest, newpos) =
  307. lexNumber' (pos - 1) [] (firstChar :: cc)
  308. in
  309. case digits of
  310. [] => token_error pos
  311. | _ => lex newpos (T.NUMBER digits :: acc) rest
  312. end
  313. and lex _ acc [] = rev acc
  314. | lex pos acc (x::xs) =
  315. (case x of
  316. #" " => lex
  317. | #"\t" => lex
  318. | #"\n" => lex
  319. | #"\r" => lex
  320. | #"{" => lexChar T.CURLY_L
  321. | #"}" => lexChar T.CURLY_R
  322. | #"[" => lexChar T.SQUARE_L
  323. | #"]" => lexChar T.SQUARE_R
  324. | #":" => lexChar T.COLON
  325. | #"," => lexChar T.COMMA
  326. | #"\"" => lexString
  327. | #"t" => lexTrue
  328. | #"f" => lexFalse
  329. | #"n" => lexNull
  330. | x => lexNumber x) (pos + 1) acc xs
  331. fun tokenize_string str = lex 1 [] (String.explode str)
  332. end
  333. \<close>
  334. subsubsection\<open>Parser\<close>
  335. ML\<open>
  336. signature NANO_JSON_PARSER = sig
  337. val json_of_string : string -> Nano_Json_Type.json
  338. val term_of_json_string : string -> term
  339. end
  340. structure Nano_Json_Parser : NANO_JSON_PARSER = struct
  341. open Nano_Json_Type
  342. open Nano_Json_Lexer
  343. fun show [] = "end of input"
  344. | show (tok :: _) = T.string_of_T tok
  345. val parse_error = error
  346. fun parseNumber digits =
  347. let open Char
  348. fun okExpDigits [] = false
  349. | okExpDigits (c :: []) = isDigit c
  350. | okExpDigits (c :: cs) = isDigit c andalso okExpDigits cs
  351. fun okExponent [] = false
  352. | okExponent (#"+" :: cs) = okExpDigits cs
  353. | okExponent (#"-" :: cs) = okExpDigits cs
  354. | okExponent cc = okExpDigits cc
  355. fun okFracTrailing [] = true
  356. | okFracTrailing (c :: cs) =
  357. (isDigit c andalso okFracTrailing cs) orelse
  358. (c = #"e" andalso okExponent cs)
  359. fun okFraction [] = false
  360. | okFraction (c :: cs) =
  361. isDigit c andalso okFracTrailing cs
  362. fun okPosTrailing [] = true
  363. | okPosTrailing (#"." :: cs) = okFraction cs
  364. | okPosTrailing (#"e" :: cs) = okExponent cs
  365. | okPosTrailing (c :: cs) =
  366. isDigit c andalso okPosTrailing cs
  367. fun okPositive [] = false
  368. | okPositive (#"0" :: []) = true
  369. | okPositive (#"0" :: #"." :: cs) = okFraction cs
  370. | okPositive (#"0" :: #"e" :: cs) = okExponent cs
  371. | okPositive (#"0" :: _) = false
  372. | okPositive (c :: cs) = isDigit c andalso okPosTrailing cs
  373. fun okNumber (#"-" :: cs) = okPositive cs
  374. | okNumber cc = okPositive cc
  375. in
  376. if okNumber digits then let
  377. val number = String.implode digits
  378. in
  379. if List.all (Char.isDigit) (String.explode number)
  380. then (case Int.fromString (String.implode digits) of
  381. NONE => parse_error "Number out of range"
  382. | SOME r => INTEGER r)
  383. else (case IEEEReal.fromString (String.implode digits) of
  384. NONE => parse_error "Number out of range"
  385. | SOME r => REAL r)
  386. end
  387. else parse_error ("Invalid number \"" ^ (String.implode digits) ^ "\"")
  388. end
  389. fun parseObject (T.CURLY_R :: xs) = (OBJECT [], xs)
  390. | parseObject tokens =
  391. let fun parsePair (T.STRING key :: T.COLON :: xs) = let
  392. val (j, xs) = parseTokens xs
  393. in
  394. ((key, j), xs)
  395. end
  396. | parsePair other =
  397. parse_error("Object key/value pair expected around \"" ^
  398. show other ^ "\"")
  399. fun parseObject' _ [] = parse_error "End of input during object"
  400. | parseObject' acc tokens =
  401. case parsePair tokens of
  402. (pair, T.COMMA :: xs) =>
  403. parseObject' (pair :: acc) xs
  404. | (pair, T.CURLY_R :: xs) =>
  405. (OBJECT (rev (pair :: acc)), xs)
  406. | (_, _) =>parse_error "Expected , or } after object element"
  407. in
  408. parseObject' [] tokens
  409. end
  410. and parseArray (T.SQUARE_R :: xs) = (ARRAY [], xs)
  411. | parseArray tokens =
  412. let fun parseArray' _ [] = error "End of input during array"
  413. | parseArray' acc tokens =
  414. case parseTokens tokens of
  415. (j, T.COMMA :: xs) => parseArray' (j :: acc) xs
  416. | (j, T.SQUARE_R :: xs) => (ARRAY (rev (j :: acc)), xs)
  417. | (_, _) => error "Expected , or ] after array element"
  418. in
  419. parseArray' [] tokens
  420. end
  421. and parseTokens [] = parse_error "Value expected"
  422. | parseTokens (tok :: xs) =
  423. (case tok of
  424. T.NUMBER d => (NUMBER ((parseNumber d)), xs)
  425. | T.STRING s => (STRING s, xs)
  426. | T.BOOL b => (BOOL b, xs)
  427. | T.NULL => (NULL, xs)
  428. | T.CURLY_L => parseObject xs
  429. | T.SQUARE_L => parseArray xs
  430. | _ => parse_error ("Unexpected token " ^ T.string_of_T tok ^
  431. " before " ^ show xs))
  432. fun json_of_string str = case parseTokens (Nano_Json_Lexer.tokenize_string str) of
  433. (value, []) => value
  434. | (_, _) => parse_error "Extra data after input"
  435. val term_of_json_string = term_of_json o json_of_string
  436. end
  437. \<close>
  438. subsection\<open>Isar Setup\<close>
  439. subsubsection\<open>The JSON Cartouche\<close>
  440. syntax "_cartouche_nano_json" :: "cartouche_position \<Rightarrow> 'a" ("JSON _")
  441. parse_translation\<open>
  442. let
  443. fun translation args =
  444. let
  445. fun err () = raise TERM ("Common._cartouche_nano_json", args)
  446. fun input s pos = Symbol_Pos.implode (Symbol_Pos.cartouche_content (Symbol_Pos.explode (s, pos)))
  447. in
  448. case args of
  449. [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] =>
  450. (case Term_Position.decode_position p of
  451. SOME (pos, _) => c $ Nano_Json_Parser.term_of_json_string (input s pos) $ p
  452. | NONE => err ())
  453. | _ => err ()
  454. end
  455. in
  456. [(@{syntax_const "_cartouche_nano_json"}, K translation)]
  457. end
  458. \<close>
  459. subsubsection\<open>Isar Top-Level Commands\<close>
  460. ML\<open>
  461. structure Nano_Json_Parser_Isar = struct
  462. fun make_const_def (constname, trm) lthy = let
  463. val arg = ((Binding.name constname, NoSyn), ((Binding.name (constname^"_def"),[]), trm))
  464. val ((_, (_ , thm)), lthy') = Local_Theory.define arg lthy
  465. in
  466. (thm, lthy')
  467. end
  468. fun def_json name json = snd o (make_const_def (name, Nano_Json_Parser.term_of_json_string json ))
  469. fun def_json_file name filename lthy = let
  470. val filename = Path.explode filename
  471. val thy = Proof_Context.theory_of lthy
  472. val master_dir = Resources.master_directory thy
  473. val abs_filename = if (Path.is_absolute filename)
  474. then filename
  475. else Path.append master_dir filename
  476. val json = File.read abs_filename
  477. in
  478. def_json name json lthy
  479. end
  480. val jsonFileP = Parse.name -- Parse.name
  481. val jsonP = Parse.name -- Parse.cartouche
  482. end
  483. \<close>
  484. ML\<open>
  485. val _ = Outer_Syntax.local_theory @{command_keyword "definition_JSON"} "Define JSON."
  486. (Nano_Json_Parser_Isar.jsonP >> (fn (name, json) => Nano_Json_Parser_Isar.def_json name json));
  487. val _ = Outer_Syntax.local_theory @{command_keyword "import_JSON"} "Define JSON from file."
  488. (Nano_Json_Parser_Isar.jsonFileP >> (fn (name, filename) => Nano_Json_Parser_Isar.def_json_file name filename));
  489. \<close>
  490. subsection\<open>Examples\<close>
  491. text\<open>
  492. Now we can use the JSON Cartouche for defining JSON-like data ``on-the-fly'', e.g.:
  493. \<close>
  494. lemma \<open>y == JSON\<open>{"name": [true,false,"test"]}\<close>\<close>
  495. oops
  496. text\<open>
  497. Note that you need to escape quotes within the JSON Cartouche, if you are using
  498. quotes as lemma delimiters, e.g.,:
  499. \<close>
  500. lemma "y == JSON\<open>{\"name\": [true,false,\"test\"]}\<close>"
  501. oops
  502. text\<open>
  503. Thus, we recommend to use the Cartouche delimiters when using the JSON Cartouche with non
  504. trivial data structures:
  505. \<close>
  506. lemma \<open> example01 == JSON \<open>{"menu": {
  507. "id": "file",
  508. "value": "File",
  509. "popup": {
  510. "menuitem": [
  511. {"value": "New", "onclick": "CreateNewDoc()"},
  512. {"value": "Open", "onclick": "OpenDoc()"},
  513. {"value": "Close", "onclick": "CloseDoc()"}
  514. ]
  515. }
  516. }}\<close>\<close>
  517. by(simp add: example01_def)
  518. text\<open>
  519. Using the top level Isar commands defined in the last section, we can now easily define
  520. JSON-like data:
  521. \<close>
  522. definition_JSON example02 \<open>
  523. {"menu": {
  524. "id": "file",
  525. "value": "File",
  526. "popup": {
  527. "menuitem": [
  528. {"value": "New", "onclick": "CreateNewDoc()"},
  529. {"value": "Open", "onclick": "OpenDoc()"},
  530. {"value": "Close", "onclick": "CloseDoc()"}
  531. ]
  532. }
  533. }}
  534. \<close>
  535. thm example02_def
  536. lemma "example01 = example02"
  537. by(simp add: example01_def example02_def)
  538. text\<open>
  539. Moreover, we can import JSON from external files:
  540. \<close>
  541. import_JSON example03 "example.json"
  542. thm example03_def
  543. lemma "example01 = example03"
  544. by(simp add: example01_def example03_def)
  545. section\<open>Serializing Nano JSON\<close>
  546. text\<open>
  547. In this section, we define the necessary infrastructure to serialize (export) data from HOL using
  548. a JSON-like data structure that other JSON tools should be able to import.
  549. \<close>
  550. subsection\<open>ML Implementation\<close>
  551. ML\<open>
  552. signature NANO_JSON_SERIALIZER = sig
  553. val serialize_json: Nano_Json_Type.json -> string
  554. val serialize_json_pretty: Nano_Json_Type.json -> string
  555. val serialize_term: term -> string
  556. val serialize_term_pretty: term -> string
  557. end
  558. structure Nano_Json_Serializer : NANO_JSON_SERIALIZER = struct
  559. open Nano_Json_Type
  560. fun escapeJsonString s =
  561. let fun bs c = "\\"^(Char.toString c)
  562. fun escape #"\"" = bs #"\""
  563. | escape #"\\" = bs #"\\"
  564. | escape #"\b" = bs #"b"
  565. | escape #"\f" = bs #"f"
  566. | escape #"\n" = bs #"n"
  567. | escape #"\r" = bs #"r"
  568. | escape #"\t" = bs #"t"
  569. | escape c =
  570. let val ord = Char.ord c
  571. in
  572. if ord < 0x20
  573. then let val hex = Word.toString (Word.fromInt ord)
  574. val prfx = if ord < 0x10 then "\\u000" else "\\u00"
  575. in
  576. prfx^hex
  577. end
  578. else
  579. Char.toString c
  580. end
  581. in
  582. String.concat (map escape (String.explode s))
  583. end
  584. fun serialize pretty json = let
  585. val nl = if pretty = NONE then "" else "\n"
  586. fun indent' 0 = ""
  587. | indent' n = " "^(indent' (n-1))
  588. fun indent n = (case pretty of NONE => ""
  589. | SOME n' => indent' (n+n'))
  590. fun serialize' _ (OBJECT []) = "{}"
  591. | serialize' _ (ARRAY []) = "[]"
  592. | serialize' n (OBJECT pp) = "{"^nl^(indent (n+1)) ^ String.concatWith
  593. (","^nl^(indent (n+1)))
  594. (map (fn (key, value) =>
  595. serialize' (n+1) (STRING key) ^ ":" ^
  596. serialize' (n+1) value) pp) ^
  597. nl^(indent n)^"}"
  598. | serialize' n (ARRAY arr) = "["^nl^(indent (n+1)) ^ String.concatWith
  599. (","^nl^(indent (n+1)))
  600. (map (serialize' (n+1) ) arr) ^
  601. nl^(indent n)^"]"
  602. | serialize' _ (NUMBER (REAL n)) = String.implode (map (fn #"~" => #"-" | c => c)
  603. (String.explode (IEEEReal.toString n)))
  604. | serialize' _ (NUMBER (INTEGER n)) = String.implode (map (fn #"~" => #"-" | c => c)
  605. (String.explode (Int.toString n)))
  606. | serialize' _ (STRING s) = "\"" ^ escapeJsonString s ^ "\""
  607. | serialize' _ (BOOL b) = Bool.toString b
  608. | serialize' _ NULL = "null"
  609. in
  610. (serialize' 0 json)^nl
  611. end
  612. val serialize_json = serialize NONE
  613. val serialize_json_pretty = serialize (SOME 0)
  614. val serialize_term = (serialize NONE) o json_of_term
  615. val serialize_term_pretty = (serialize (SOME 0)) o json_of_term
  616. end
  617. \<close>
  618. subsection\<open>Isar Setup\<close>
  619. ML\<open>
  620. structure Nano_Json_Serialize_Isar = struct
  621. fun export_json ctxt json_const filename =
  622. let
  623. val thy = Proof_Context.theory_of ctxt
  624. val master_dir = Resources.master_directory thy
  625. val term = Thm.concl_of (Global_Theory.get_thm thy (json_const^"_def"))
  626. val json_term = case term of
  627. Const (@{const_name "Pure.eq"}, _) $ _ $ json_term => json_term
  628. | _ $ (_ $ json_term) => json_term
  629. | _ => error ("Term structure not supported: "
  630. ^(Sledgehammer_Util.hackish_string_of_term ctxt term))
  631. val json_string = Nano_Json_Serializer.serialize_term_pretty json_term
  632. in
  633. case filename of
  634. SOME filename => let
  635. val filename = Path.explode filename
  636. val abs_filename = if (Path.is_absolute filename)
  637. then filename
  638. else Path.append master_dir filename
  639. in
  640. File.write (abs_filename) json_string
  641. handle (IO.Io{name=name,...}) => warning ("Could not write \""^name^"\".")
  642. end
  643. | NONE => tracing json_string
  644. end
  645. end
  646. \<close>
  647. ML\<open>
  648. Outer_Syntax.command ("serialize_JSON", Position.none) "export JSON data to an external file"
  649. (Parse.name -- Scan.option Parse.name >> (fn (const_name,filename) =>
  650. (Toplevel.keep (fn state => Nano_Json_Serialize_Isar.export_json (Toplevel.context_of state) const_name filename))));
  651. \<close>
  652. subsection\<open>Examples\<close>
  653. text\<open>
  654. We can now serialize JSON and print the result in the output window of Isabelle/HOL:
  655. \<close>
  656. serialize_JSON example01
  657. text\<open>
  658. Alternatively, we can export the serialized JSON into a file:
  659. \<close>
  660. serialize_JSON example01 example01.json
  661. section\<open>Putting Everything Together\<close>
  662. text\<open>
  663. For convenience, we provide an ML structure that provides access to both the parser and the
  664. serializer:,
  665. \<close>
  666. ML\<open>
  667. structure Nano_Json = struct
  668. open Nano_Json_Type
  669. open Nano_Json_Parser
  670. open Nano_Json_Serializer
  671. end
  672. \<close>
  673. end