author | bulwahn |
Thu, 29 Jul 2010 17:27:54 +0200 | |
changeset 38074 | 31174744b9a2 |
child 38075 | 3d5e2b7d1374 |
permissions | -rw-r--r-- |
38074
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
1 |
theory Code_Prolog_Examples |
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
2 |
imports Predicate_Compile_Alternative_Defs |
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
3 |
uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML" |
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
4 |
begin |
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
5 |
|
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
6 |
section {* Example append *} |
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
7 |
|
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
8 |
inductive append |
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
9 |
where |
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
10 |
"append [] ys ys" |
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
11 |
| "append xs ys zs ==> append (x # xs) ys (x # zs)" |
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
12 |
|
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
13 |
code_pred append . |
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
14 |
|
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
15 |
ML {* |
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
16 |
tracing (Code_Prolog.write_program (Code_Prolog.generate @{context} [@{const_name append}])) |
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
17 |
*} |
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
18 |
|
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
19 |
ML {* |
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
20 |
Code_Prolog.run (Code_Prolog.generate @{context} [@{const_name append}]) "append" ["X", "Y", "Z"] |
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
21 |
*} |
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
22 |
|
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
diff
changeset
|
23 |
end |