src/HOL/Library/Code_Test.thy
author hoelzl
Thu Oct 09 11:00:40 2014 +0200 (2014-10-09)
changeset 58637 3094b0edd6b5
parent 58626 6c473ed0ac70
child 58719 ac4f764c5be1
permissions -rw-r--r--
fix document generation in Code_Test
     1 (*  Title:      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 {* YXML encoding for @{typ Code_Evaluation.term} *}
    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 {* Serialise @{typ yxml_of_term} to native string of target language *}
    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 {*
    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 *}
    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 {* Local_Theory.map_naming (Name_Space.mandatory_path "xml") *}
    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 {*
   116   Encoding @{typ Code_Evaluation.term} into XML trees
   117   as defined in @{file "~~/src/Pure/term_xml.ML"}
   118 *}
   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   (*
   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   *)
   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 {* Test engine and drivers *}
   145 
   146 ML_file "code_test.ML"
   147 
   148 end