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