git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13753 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
parent
b0efb7ab3f
commit
8ad94194dc
|
@ -132,7 +132,7 @@ val _ =
|
|||
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword C_export} "read and evaluate C file"
|
||||
(Resources.parse_files "C_file" --| semi >> C_File.C); (* HACK TO BE DONE *)
|
||||
(Resources.parse_files "C_file" --| semi >> C_File.C); (* HACK: TO BE DONE *)
|
||||
|
||||
|
||||
in end
|
||||
|
|
|
@ -54,6 +54,7 @@ inside
|
|||
int a = "outside";
|
||||
\<close>
|
||||
|
||||
|
||||
C \<comment> \<open>Backslash newline\<close> \<open>
|
||||
i\
|
||||
n\
|
||||
|
@ -196,7 +197,7 @@ int a = 0;
|
|||
*/
|
||||
|
||||
/** ML \<open>fn _ => fn _ => fn _ => I\<close> (* An example of correct syntax accepted as usual *)
|
||||
*/
|
||||
*/
|
||||
\<close>
|
||||
|
||||
subsection \<open>Mixing Together Any Types of Antiquotations\<close>
|
||||
|
|
|
@ -145,15 +145,20 @@ fun print_top make_string (_, (value, pos1, pos2)) thy =
|
|||
in thy end
|
||||
\<close>
|
||||
|
||||
C \<open>int f (int a) { /*@ (*1*) @ ML \<open>fn _ => fn _ => fn env =>
|
||||
C (SOME env)
|
||||
\<open>int c = b * 2 + 1 //@ && C \<open>int d = c; //@ @ ML_rev \<open>@{C_def \<up> C'}\<close> \
|
||||
@ C \<open>int b = c + b; //* C' \<open>\<close>\<close> \
|
||||
@ C_rev \<open>int a = c + a; //* C' \<open>\<close>\<close>\<close>
|
||||
//@ && ML \<open>fn stack => fn top => fn _ => \
|
||||
tap (print_top @{make_string} top) \
|
||||
#> C NONE \<open>int b = a; //@ C' \<open>int d = c + a;\<close>\<close> \<close>
|
||||
;\<close>\<close> (*2*) ML \<open>@{C_def \<up> C}\<close> (*3*) ML \<open>@{C_def \<down> C_rev}\<close>
|
||||
(*4*) ++@@ ML \<open>@{print_top'}\<close> */ return 0; }\<close>
|
||||
C \<open>int f (int a)
|
||||
{ /*@ (*1*) @ ML \<open>fn _ => fn _ => fn env =>
|
||||
C (SOME env)
|
||||
\<open>int c = b * 2 + 1 //@ && C \<open>int d = c; //@ @ ML_rev \<open>@{C_def \<up> C'}\<close> \
|
||||
@ C \<open>int b = c + b; //* C'\<open>\<close>\<close> \
|
||||
@ C_rev\<open>int a = c + a; //* C'\<open>\<close>\<close>\<close>
|
||||
//@ && ML \<open>fn stack => fn top => fn _ => \
|
||||
tap (print_top @{make_string} top) \
|
||||
#> C NONE \<open>int b = a; //@ C' \<open>int d = c + a;\<close>\<close>\<close>
|
||||
;\<close>\<close>
|
||||
(*2*) ML \<open>@{C_def \<up> C}\<close>
|
||||
(*3*) ML \<open>@{C_def \<down> C_rev}\<close>
|
||||
(*4*) ++@@ ML \<open>@{print_top'}\<close>
|
||||
*/
|
||||
return 0; }\<close>
|
||||
|
||||
end
|
||||
|
|
|
@ -1004,8 +1004,8 @@ fun command dir name =
|
|||
end)))
|
||||
|
||||
in
|
||||
val _ = Theory.setup ( command Bottom_up ("ML", \<^here>)
|
||||
#> command Top_down ("ML_reverse", \<^here>))
|
||||
val _ = Theory.setup ( command Bottom_up ("ML", @{here})
|
||||
#> command Top_down ("ML_reverse", @{here}))
|
||||
end
|
||||
\<close>
|
||||
|
||||
|
|
Loading…
Reference in New Issue