| author | Walther Neuper <neuper@ist.tugraz.at> |
| Tue, 01 Mar 2011 15:23:59 +0100 | |
| branch | decompose-isar |
| changeset 41905 | b772eb34c16c |
| parent 41899 | d837e83a4835 |
| child 41922 | 32d7766945fb |
| permissions | -rw-r--r-- |
| neuper@37946 | 1 |
(*2foointerpreter.ML*) |
| neuper@37946 | 2 |
|
| neuper@37946 | 3 |
fun foointerpret ((Const ("Foo_Language.fooprog", _)) $ (_ $ _ $ res)) = res;
|
| neuper@37946 | 4 |
|
| neuper@41899 | 5 |
(* Foo_Language's definitions are recognized: *) |
| neuper@41905 | 6 |
(*val trm = Syntax.read_term_global @{theory Foo_Language} "fooprog (a = b)"; *)
|
| neuper@41905 | 7 |
val trm = Syntax.read_term_global @{theory "../1language/Foo_Language"}
|
| neuper@41905 | 8 |
"fooprog (a = b)"; |
| neuper@37946 | 9 |
(*val trm = |
| neuper@37946 | 10 |
Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $
|
| neuper@37946 | 11 |
(Const ("op =", "'a => 'a => bool") $ Free ("a", "'a") $
|
| neuper@37946 | 12 |
Free ("b", "'a"))
|
| neuper@37946 | 13 |
: term*) |
| neuper@37946 | 14 |
foointerpret trm; |