1(*
2 * Copyright 2018, Data61
3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 * ABN 41 687 119 230.
5
6 * This software may be distributed and modified according to the terms of
7 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 * See "LICENSE_BSD2.txt" for details.
9
10 * @TAG(DATA61_BSD)
11 *)
12
13(* Basic tests for the Insulin desugar tool. *)
14
15theory Insulin_Test
16imports
17  Lib.Insulin
18  Main
19begin
20
21ML \<open>
22(*
23 * To be considered successful, desugaring should do two things:
24 *   - remove the unwanted syntax strings
25 *   - return an equivalent term
26 * The following code just checks those two conditions.
27 *)
28
29fun test_desugar ctxt (term, bad_strings) = let
30  val text = (* function being tested *)
31             Insulin.desugar_term ctxt term bad_strings
32             (* strip markup from result *)
33             |> YXML.parse_body
34             |> XML.content_of
35  val remaining_bads = filter (fn bs => String.isSubstring bs text) bad_strings
36  val _ = if null remaining_bads then () else
37          raise TERM ("failed to desugar these strings: [" ^ commas bad_strings ^ "]\n" ^
38                      "output: " ^ text, [term])
39  val term' = Syntax.read_term ctxt text
40  val _ = if term = term' then () else
41          raise TERM ("desugared term not equal to original",
42                      [term, term'])
43  in () end
44\<close>
45
46ML \<open>
47(* The test cases. *)
48[ (@{term "A \<and> B"}, ["\<and>"])
49, (@{term "a + 0 = a * 1"}, ["+", "0", "1"])
50, (@{term "(f(x := y)) z = (if z = x then y else f z)"}, [":="])
51, (@{term "(f(x := y)) z = (if z = x then y else f z)"}, ["="])
52] |> app (test_desugar @{context})
53\<close>
54
55end
56