src/HOL/Library/Code_Test.thy
changeset 58626 6c473ed0ac70
parent 58348 2d47c7d10b62
child 58637 3094b0edd6b5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Code_Test.thy	Wed Oct 08 09:09:12 2014 +0200
     1.3 @@ -0,0 +1,148 @@
     1.4 +(*  Title:      Code_Test.thy
     1.5 +    Author:     Andreas Lochbihler, ETH Zurich
     1.6 +
     1.7 +Test infrastructure for the code generator
     1.8 +*)
     1.9 +
    1.10 +theory Code_Test
    1.11 +imports Main
    1.12 +keywords "test_code" :: diag
    1.13 +begin
    1.14 +
    1.15 +subsection {* YXML encoding for @{typ Code_Evaluation.term} *}
    1.16 +
    1.17 +datatype (plugins del: code size "quickcheck") yxml_of_term = YXML
    1.18 +
    1.19 +lemma yot_anything: "x = (y :: yxml_of_term)"
    1.20 +by(cases x y rule: yxml_of_term.exhaust[case_product yxml_of_term.exhaust])(simp)
    1.21 +
    1.22 +definition yot_empty :: yxml_of_term where [code del]: "yot_empty = YXML"
    1.23 +definition yot_literal :: "String.literal \<Rightarrow> yxml_of_term"
    1.24 +  where [code del]: "yot_literal _ = YXML"
    1.25 +definition yot_append :: "yxml_of_term \<Rightarrow> yxml_of_term \<Rightarrow> yxml_of_term"
    1.26 +  where [code del]: "yot_append _ _ = YXML"
    1.27 +definition yot_concat :: "yxml_of_term list \<Rightarrow> yxml_of_term"
    1.28 +  where [code del]: "yot_concat _ = YXML"
    1.29 +
    1.30 +text {* Serialise @{typ yxml_of_term} to native string of target language *}
    1.31 +
    1.32 +code_printing type_constructor yxml_of_term
    1.33 +  \<rightharpoonup>  (SML) "string"
    1.34 +  and (OCaml) "string"
    1.35 +  and (Haskell) "String"
    1.36 +  and (Scala) "String"
    1.37 +| constant yot_empty
    1.38 +  \<rightharpoonup>  (SML) "\"\""
    1.39 +  and (OCaml) "\"\""
    1.40 +  and (Haskell) "\"\""
    1.41 +  and (Scala) "\"\""
    1.42 +| constant yot_literal
    1.43 +  \<rightharpoonup>  (SML) "_"
    1.44 +  and (OCaml) "_"
    1.45 +  and (Haskell) "_"
    1.46 +  and (Scala) "_"
    1.47 +| constant yot_append
    1.48 +  \<rightharpoonup> (SML) "String.concat [(_), (_)]"
    1.49 +  and (OCaml) "String.concat \"\" [(_); (_)]"
    1.50 +  and (Haskell) infixr 5 "++"
    1.51 +  and (Scala) infixl 5 "+"
    1.52 +| constant yot_concat
    1.53 +  \<rightharpoonup> (SML) "String.concat"
    1.54 +  and (OCaml) "String.concat \"\""
    1.55 +  and (Haskell) "Prelude.concat"
    1.56 +  and (Scala) "_.mkString(\"\")"
    1.57 +
    1.58 +text {*
    1.59 +  Stripped-down implementations of Isabelle's XML tree with YXML encoding
    1.60 +  as defined in @{file "~~/src/Pure/PIDE/xml.ML"}, @{file "~~/src/Pure/PIDE/yxml.ML"}
    1.61 +  sufficient to encode @{typ "Code_Evaluation.term"} as in @{file "~~/src/Pure/term_xml.ML"}.
    1.62 +*}
    1.63 +
    1.64 +datatype (plugins del: code size "quickcheck") xml_tree = XML_Tree
    1.65 +
    1.66 +lemma xml_tree_anything: "x = (y :: xml_tree)"
    1.67 +by(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp)
    1.68 +
    1.69 +context begin
    1.70 +local_setup {* Local_Theory.map_naming (Name_Space.mandatory_path "xml") *}
    1.71 +
    1.72 +type_synonym attributes = "(String.literal \<times> String.literal) list"
    1.73 +type_synonym body = "xml_tree list"
    1.74 +
    1.75 +definition Elem :: "String.literal \<Rightarrow> attributes \<Rightarrow> xml_tree list \<Rightarrow> xml_tree"
    1.76 +where [code del]: "Elem _ _ _ = XML_Tree"
    1.77 +
    1.78 +definition Text :: "String.literal \<Rightarrow> xml_tree"
    1.79 +where [code del]: "Text _ = XML_Tree"
    1.80 +
    1.81 +definition node :: "xml_tree list \<Rightarrow> xml_tree"
    1.82 +where "node ts = Elem (STR '':'') [] ts"
    1.83 +
    1.84 +definition tagged :: "String.literal \<Rightarrow> String.literal option \<Rightarrow> xml_tree list \<Rightarrow> xml_tree"
    1.85 +where "tagged tag x ts = Elem tag (case x of None \<Rightarrow> [] | Some x' \<Rightarrow> [(STR ''0'', x')]) ts"
    1.86 +
    1.87 +definition list where "list f xs = map (node \<circ> f) xs"
    1.88 +
    1.89 +definition X :: yxml_of_term where "X = yot_literal (STR [Char Nibble0 Nibble5])"
    1.90 +definition Y :: yxml_of_term where "Y = yot_literal (STR [Char Nibble0 Nibble6])"
    1.91 +definition XY :: yxml_of_term where "XY = yot_append X Y"
    1.92 +definition XYX :: yxml_of_term where "XYX = yot_append XY X"
    1.93 +
    1.94 +end
    1.95 +
    1.96 +code_datatype xml.Elem xml.Text
    1.97 +
    1.98 +definition yxml_string_of_xml_tree :: "xml_tree \<Rightarrow> yxml_of_term \<Rightarrow> yxml_of_term"
    1.99 +where [code del]: "yxml_string_of_xml_tree _ _ = YXML"
   1.100 +
   1.101 +lemma yxml_string_of_xml_tree_code [code]:
   1.102 +  "yxml_string_of_xml_tree (xml.Elem name atts ts) rest =
   1.103 +   yot_append xml.XY (
   1.104 +   yot_append (yot_literal name) (
   1.105 +   foldr (\<lambda>(a, x) rest. 
   1.106 +     yot_append xml.Y (
   1.107 +     yot_append (yot_literal a) (
   1.108 +     yot_append (yot_literal (STR ''='')) (
   1.109 +     yot_append (yot_literal x) rest)))) atts (
   1.110 +   foldr yxml_string_of_xml_tree ts (
   1.111 +   yot_append xml.XYX rest))))"
   1.112 +  "yxml_string_of_xml_tree (xml.Text s) rest = yot_append (yot_literal s) rest"
   1.113 +by(rule yot_anything)+
   1.114 +
   1.115 +definition yxml_string_of_body :: "xml.body \<Rightarrow> yxml_of_term"
   1.116 +where "yxml_string_of_body ts = foldr yxml_string_of_xml_tree ts yot_empty"
   1.117 +
   1.118 +text {*
   1.119 +  Encoding @{typ Code_Evaluation.term} into XML trees
   1.120 +  as defined in @{file "~~/src/Pure/term_xml.ML"}
   1.121 +*}
   1.122 +
   1.123 +definition xml_of_typ :: "Typerep.typerep \<Rightarrow> xml.body"
   1.124 +where [code del]: "xml_of_typ _ = [XML_Tree]"
   1.125 +
   1.126 +definition xml_of_term :: "Code_Evaluation.term \<Rightarrow> xml.body"
   1.127 +where [code del]: "xml_of_term _ = [XML_Tree]"
   1.128 +
   1.129 +lemma xml_of_typ_code [code]:
   1.130 +  "xml_of_typ (typerep.Typerep t args) = [xml.tagged (STR ''0'') (Some t) (xml.list xml_of_typ args)]"
   1.131 +by(simp add: xml_of_typ_def xml_tree_anything)
   1.132 +
   1.133 +lemma xml_of_term_code [code]:
   1.134 +  "xml_of_term (Code_Evaluation.Const x ty) = [xml.tagged (STR ''0'') (Some x) (xml_of_typ ty)]"
   1.135 +  "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)]]"
   1.136 +  "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)]]"
   1.137 +  -- {*
   1.138 +    FIXME: @{const Code_Evaluation.Free} is used only in Quickcheck_Narrowing to represent
   1.139 +    uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables.
   1.140 +  *}
   1.141 +  "xml_of_term (Code_Evaluation.Free x ty)  = [xml.tagged (STR ''1'') (Some x) (xml_of_typ ty)]"
   1.142 +by(simp_all add: xml_of_term_def xml_tree_anything)
   1.143 +
   1.144 +definition yxml_string_of_term :: "Code_Evaluation.term \<Rightarrow> yxml_of_term"
   1.145 +where "yxml_string_of_term = yxml_string_of_body \<circ> xml_of_term"
   1.146 +
   1.147 +subsection {* Test engine and drivers *}
   1.148 +
   1.149 +ML_file "code_test.ML"
   1.150 +
   1.151 +end