Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma

Benutzer


products/Sources/formale Sprachen/Isabelle/HOL/Library/ (Isabelle Prover Version 2025-1^©) Datei vom 16.11.2025 mit Größe 5 kB

Quelle Code_Test.thy

Sprache: Isabelle

(* Title: HOL/Library/Code_Test.thy
Author: Andreas Lochbihler, ETH Zürich

Test infrastructure for the code generator.
*)

section ‹

Code_Test
Main
"test_code" :: diag

‹YXML encoding for typ‹Code_Evaluation.term› (λ(valermif_insert xs))))])"

(plugins del: code size "quickcheck") yxml_of_term = YXML

yot_anything: "x = (y :: yxml_of_term)"
(cases x y rule: yxml_of_term.exhaust[case_product yxml_of_term.exhaust])(simp)

yot_empty :: yxml_of_term where [code del]: "yot_empty = YXML"
yot_literal :: "String.literal → yxml_of_term"
where [code del]: "yot_literal _ = YXML"
yot_append :: "yxml_of_term → yxml_of_term → yxml_of_term"
where [code del]: "yot_append _ _ = YXML"
yot_concat :: "yxml_of_term list → yxml_of_term"
where [code del]: "yot_concat _ = YXML"

type_constructor yxml_of_term
⇀ (SML) "string"
and (OCaml) "string"
and (Haskell) "String"
and (Scala) "String"
constant yot_empty
⇀ (SML) "\"\""
and (OCaml) "\"\""
and (Haskell) "\"\""
and (Scala) "\"\""
constant yot_literal
⇀ (SML) "_"
and (OCaml) "_"
and (Haskell) "_"
and (Scala) "_"
constant yot_append
\<poonup
and (OCaml) "String.concat \"\" [(_); (_)]"
and (Haskell) infixr 5 "++"
and (Scala) infixl 5 "+"
constant yot_concat
⇀ (SML) "String.concat"
and (OCaml) "String.concat \"\""
and (Haskell) "Prelude.concat"
and (Scala) "_.mkString(\"\")"

‹
Stripped-down implementations of Isabelle's XML tree with YXML encoding as
defined in 🚫‹~~/src/Pure/PIDE/xml.ML›, 🚫‹~~/src/Pure/PIDE/yxml.ML›
sufficient to encode typ‹Code_Evaluation.term› as in
🚫‹~~/src/Pure/term_xml.ML›.
›

(plugins del: code size "quickcheck") xml_tree = XML_Tree

xml_tree_anything: "x = (y :: xml_tree)"
(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp)

begin
‹Local_Theory.map_background_naming (Name_Space.mandatory_path "xml")›

attributes = "(String.literal × String.literal) list"
body = "xml_tree list"

Elem :: "String.literal → attributes → xml_tree list → xml_tree"
[code del]: "Elem _ _ _ = XML_Tree"

Text :: "String.literal → xml_tree"
[code del]: "Text _ = XML_Tree"

node :: "xml_tree list → xml_tree"
"node ts = Elem (STR '':'') [] ts"

tagged :: "String.literal → String.literal option → xml_tree list → xml_tree"
"tagged tag x ts = Elem tag (case x of None → [] | Some x' → [(STR ''0'', x')]) ts"

list where "list f xs = map (node ∘ f) xs"

X :: yxml_of_term where "X = yot_literal (STR 0x05)"
Y :: yxml_of_term where "Y = yot_literal (STR 0x06)"
XY :: yxml_of_term where "XY = yot_append X Y"
XYX :: yxml_of_term where "XYX = yot_append XY X"

xml.Elem xml.Text

yxml_string_of_xml_tree :: "xml_tree → yxml_of_term → yxml_of_term"
[code del]: "yxml_string_of_xml_tree _ _ = YXML"

yxml_string_of_xml_tree_code [code]:
"yxml_string_of_xml_tree (xml.Elem name atts ts) rest =
yot_append xml.XY (
yot_append (yot_literal name) (
foldr (λ(a, x) rest.
yot_append xml.Y (
yot_append (yot_literal a) (
yot_append (yot_literal (STR ''='')) (
yot_append (yot_literal x) rest)))) atts (
foldr yxml_string_of_xml_tree ts (
yot_append xml.XYX rest))))"
"yxml_string_of_xml_tree (xml.Text s) rest = yot_append (yot_literal s) rest"
(rule yot_anything)+

yxml_string_of_body :: "xml.body → yxml_of_term"
"yxml_string_of_body ts = foldr yxml_string_of_xml_tree ts yot_empty"

‹
Encoding typ‹Code_Evaluation.term› into XML trees as defined in
🚫‹~~/src/Pure/term_xml.ML›.
›

xml_of_typ :: "Typerep.typerep → xml.body"
[code del]: "xml_of_typ _ = [XML_Tree]"

xml_of_term :: "Code_Evaluation.term → xml.body"
[code del]: "xml_of_term _ = [XML_Tree]"

xml_of_typ_code [code]:
"xml_of_typ (typerep.Typerep t args) = [xml.tagged (STR ''0'') (Some t) (xml.list xml_of_typ args)]"
(simp add: xml_of_typ_def xml_tree_anything)

xml_of_term_code [code]:
"xml_of_term (Code_Evaluation.Const x ty) = [xml.tagged (STR ''0'') (Some x) (xml_of_typ ty)]"
"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)]]"
"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)]]"
― ‹FIXME: const‹Code_Evaluation.Free› is used only in 🚫‹HOL.Quickcheck_Narrowing› to represent
uninstantiated parameters in constructors. Here, we always translate them to 🚫‹Free› variables.›
"xml_of_term (Code_Evaluation.Free x ty) = [xml.tagged (STR ''1'') (Some x) (xml_of_typ ty)]"
(simp_all add: xml_of_term_def xml_tree_anything)

yxml_string_of_term :: "Code_Evaluation.term → yxml_of_term"
"yxml_string_of_term = yxml_string_of_body ∘ xml_of_term"

‹Test engine and drivers›

‹code_test.ML›

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.26 Sekunden ¤

Wurzel

Suchen

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.