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