src/HOL/Library/Code_Test.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 61585 a9599d3d7610
child 62597 b3f2b8c906a6
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
     1 (*  Title:      HOL/Library/Code_Test.thy
     2     Author:     Andreas Lochbihler, ETH Zurich
     3 
     4 Test infrastructure for the code generator
     5 *)
     6 
     7 theory Code_Test
     8 imports Main
     9 keywords "test_code" :: diag
    10 begin
    11 
    12 subsection \<open>YXML encoding for @{typ Code_Evaluation.term}\<close>
    13 
    14 datatype (plugins del: code size "quickcheck") yxml_of_term = YXML
    15 
    16 lemma yot_anything: "x = (y :: yxml_of_term)"
    17 by(cases x y rule: yxml_of_term.exhaust[case_product yxml_of_term.exhaust])(simp)
    18 
    19 definition yot_empty :: yxml_of_term where [code del]: "yot_empty = YXML"
    20 definition yot_literal :: "String.literal \<Rightarrow> yxml_of_term"
    21   where [code del]: "yot_literal _ = YXML"
    22 definition yot_append :: "yxml_of_term \<Rightarrow> yxml_of_term \<Rightarrow> yxml_of_term"
    23   where [code del]: "yot_append _ _ = YXML"
    24 definition yot_concat :: "yxml_of_term list \<Rightarrow> yxml_of_term"
    25   where [code del]: "yot_concat _ = YXML"
    26 
    27 text \<open>Serialise @{typ yxml_of_term} to native string of target language\<close>
    28 
    29 code_printing type_constructor yxml_of_term
    30   \<rightharpoonup>  (SML) "string"
    31   and (OCaml) "string"
    32   and (Haskell) "String"
    33   and (Scala) "String"
    34 | constant yot_empty
    35   \<rightharpoonup>  (SML) "\"\""
    36   and (OCaml) "\"\""
    37   and (Haskell) "\"\""
    38   and (Scala) "\"\""
    39 | constant yot_literal
    40   \<rightharpoonup>  (SML) "_"
    41   and (OCaml) "_"
    42   and (Haskell) "_"
    43   and (Scala) "_"
    44 | constant yot_append
    45   \<rightharpoonup> (SML) "String.concat [(_), (_)]"
    46   and (OCaml) "String.concat \"\" [(_); (_)]"
    47   and (Haskell) infixr 5 "++"
    48   and (Scala) infixl 5 "+"
    49 | constant yot_concat
    50   \<rightharpoonup> (SML) "String.concat"
    51   and (OCaml) "String.concat \"\""
    52   and (Haskell) "Prelude.concat"
    53   and (Scala) "_.mkString(\"\")"
    54 
    55 text \<open>
    56   Stripped-down implementations of Isabelle's XML tree with YXML encoding
    57   as defined in @{file "~~/src/Pure/PIDE/xml.ML"}, @{file "~~/src/Pure/PIDE/yxml.ML"}
    58   sufficient to encode @{typ "Code_Evaluation.term"} as in @{file "~~/src/Pure/term_xml.ML"}.
    59 \<close>
    60 
    61 datatype (plugins del: code size "quickcheck") xml_tree = XML_Tree
    62 
    63 lemma xml_tree_anything: "x = (y :: xml_tree)"
    64 by(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp)
    65 
    66 context begin
    67 local_setup \<open>Local_Theory.map_background_naming (Name_Space.mandatory_path "xml")\<close>
    68 
    69 type_synonym attributes = "(String.literal \<times> String.literal) list"
    70 type_synonym body = "xml_tree list"
    71 
    72 definition Elem :: "String.literal \<Rightarrow> attributes \<Rightarrow> xml_tree list \<Rightarrow> xml_tree"
    73 where [code del]: "Elem _ _ _ = XML_Tree"
    74 
    75 definition Text :: "String.literal \<Rightarrow> xml_tree"
    76 where [code del]: "Text _ = XML_Tree"
    77 
    78 definition node :: "xml_tree list \<Rightarrow> xml_tree"
    79 where "node ts = Elem (STR '':'') [] ts"
    80 
    81 definition tagged :: "String.literal \<Rightarrow> String.literal option \<Rightarrow> xml_tree list \<Rightarrow> xml_tree"
    82 where "tagged tag x ts = Elem tag (case x of None \<Rightarrow> [] | Some x' \<Rightarrow> [(STR ''0'', x')]) ts"
    83 
    84 definition list where "list f xs = map (node \<circ> f) xs"
    85 
    86 definition X :: yxml_of_term where "X = yot_literal (STR [Char Nibble0 Nibble5])"
    87 definition Y :: yxml_of_term where "Y = yot_literal (STR [Char Nibble0 Nibble6])"
    88 definition XY :: yxml_of_term where "XY = yot_append X Y"
    89 definition XYX :: yxml_of_term where "XYX = yot_append XY X"
    90 
    91 end
    92 
    93 code_datatype xml.Elem xml.Text
    94 
    95 definition yxml_string_of_xml_tree :: "xml_tree \<Rightarrow> yxml_of_term \<Rightarrow> yxml_of_term"
    96 where [code del]: "yxml_string_of_xml_tree _ _ = YXML"
    97 
    98 lemma yxml_string_of_xml_tree_code [code]:
    99   "yxml_string_of_xml_tree (xml.Elem name atts ts) rest =
   100    yot_append xml.XY (
   101    yot_append (yot_literal name) (
   102    foldr (\<lambda>(a, x) rest. 
   103      yot_append xml.Y (
   104      yot_append (yot_literal a) (
   105      yot_append (yot_literal (STR ''='')) (
   106      yot_append (yot_literal x) rest)))) atts (
   107    foldr yxml_string_of_xml_tree ts (
   108    yot_append xml.XYX rest))))"
   109   "yxml_string_of_xml_tree (xml.Text s) rest = yot_append (yot_literal s) rest"
   110 by(rule yot_anything)+
   111 
   112 definition yxml_string_of_body :: "xml.body \<Rightarrow> yxml_of_term"
   113 where "yxml_string_of_body ts = foldr yxml_string_of_xml_tree ts yot_empty"
   114 
   115 text \<open>
   116   Encoding @{typ Code_Evaluation.term} into XML trees
   117   as defined in @{file "~~/src/Pure/term_xml.ML"}
   118 \<close>
   119 
   120 definition xml_of_typ :: "Typerep.typerep \<Rightarrow> xml.body"
   121 where [code del]: "xml_of_typ _ = [XML_Tree]"
   122 
   123 definition xml_of_term :: "Code_Evaluation.term \<Rightarrow> xml.body"
   124 where [code del]: "xml_of_term _ = [XML_Tree]"
   125 
   126 lemma xml_of_typ_code [code]:
   127   "xml_of_typ (typerep.Typerep t args) = [xml.tagged (STR ''0'') (Some t) (xml.list xml_of_typ args)]"
   128 by(simp add: xml_of_typ_def xml_tree_anything)
   129 
   130 lemma xml_of_term_code [code]:
   131   "xml_of_term (Code_Evaluation.Const x ty) = [xml.tagged (STR ''0'') (Some x) (xml_of_typ ty)]"
   132   "xml_of_term (Code_Evaluation.App t1 t2)  = [xml.tagged (STR ''5'') None [xml.node (xml_of_term t1), xml.node (xml_of_term t2)]]"
   133   "xml_of_term (Code_Evaluation.Abs x ty t) = [xml.tagged (STR ''4'') (Some x) [xml.node (xml_of_typ ty), xml.node (xml_of_term t)]]"
   134   \<comment> \<open>
   135     FIXME: @{const Code_Evaluation.Free} is used only in @{theory Quickcheck_Narrowing} to represent
   136     uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables.
   137 \<close>
   138   "xml_of_term (Code_Evaluation.Free x ty)  = [xml.tagged (STR ''1'') (Some x) (xml_of_typ ty)]"
   139 by(simp_all add: xml_of_term_def xml_tree_anything)
   140 
   141 definition yxml_string_of_term :: "Code_Evaluation.term \<Rightarrow> yxml_of_term"
   142 where "yxml_string_of_term = yxml_string_of_body \<circ> xml_of_term"
   143 
   144 subsection \<open>Test engine and drivers\<close>
   145 
   146 ML_file "code_test.ML"
   147 
   148 end