| author | Alexander Kargl <akargl@brgkepler.net> |
| Mon, 25 Jul 2011 11:52:07 +0200 | |
| branch | decompose-isar |
| changeset 42176 | 3573fd729e99 |
| parent 38031 | 460c24a6a6ba |
| child 48761 | 4162c4f6f897 |
| permissions | -rw-r--r-- |
| akargl@42176 | 1 |
(* Title: tests for mathml.sml |
| akargl@42176 | 2 |
Author: Walther Neuper 060311 |
| neuper@37906 | 3 |
(c) isac-team 2006 |
| neuper@37906 | 4 |
|
| neuper@37906 | 5 |
use"../smltest/xmlsrc/mathml.sml"; |
| neuper@37906 | 6 |
use"mathml.sml"; |
| neuper@37906 | 7 |
*) |
| neuper@37906 | 8 |
"-----------------------------------------------------------------"; |
| neuper@37906 | 9 |
"table of contents -----------------------------------------------"; |
| neuper@37906 | 10 |
"-----------------------------------------------------------------"; |
| neuper@37906 | 11 |
"within struct ---------------------------------------------------"; |
| neuper@37906 | 12 |
"-----------------------------------------------------------------"; |
| neuper@37906 | 13 |
"--------- encode ^^^ -> ^ ---------------------------------------"; |
| neuper@37906 | 14 |
"--------- encode < -> < and > -> > --------------------------"; |
| neuper@37906 | 15 |
"-----------------------------------------------------------------"; |
| neuper@37906 | 16 |
"exported from struct --------------------------------------------"; |
| neuper@37906 | 17 |
"-----------------------------------------------------------------"; |
| neuper@37906 | 18 |
"--------- ... ---------------------------------------------------"; |
| neuper@37906 | 19 |
"-----------------------------------------------------------------"; |
| neuper@37906 | 20 |
|
| neuper@37906 | 21 |
|
| neuper@37906 | 22 |
|
| neuper@37906 | 23 |
"-----------------------------------------------------------------"; |
| neuper@37906 | 24 |
"within struct ---------------------------------------------------"; |
| neuper@37906 | 25 |
"-----------------------------------------------------------------"; |
| neuper@37906 | 26 |
(*==================================================================*) |
| neuper@37906 | 27 |
|
| neuper@37906 | 28 |
"--------- encode ^^^ -> ^ ---------------------------------------"; |
| neuper@37906 | 29 |
"--------- encode ^^^ -> ^ ---------------------------------------"; |
| neuper@37906 | 30 |
"--------- encode ^^^ -> ^ ---------------------------------------"; |
| neuper@37906 | 31 |
val str = "a^^^2+b^^^2=c^^^2"; |
| neuper@37906 | 32 |
if decode str = "a^2+b^2=c^2" then () |
| neuper@38031 | 33 |
else error "mathml.sml: diff.behav. in encode ^^^ -> ^"; |
| neuper@37906 | 34 |
|
| akargl@42176 | 35 |
"--------- encode < -> < and > -> > --------------------------"; |
| akargl@42176 | 36 |
"--------- encode < -> < and > -> > --------------------------"; |
| akargl@42176 | 37 |
"--------- encode < -> < and > -> > --------------------------"; |
| neuper@37906 | 38 |
val str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"; |
| akargl@42176 | 39 |
if decode str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n" then () |
| akargl@42176 | 40 |
else error "mathml.sml: diff.behav. in encode '<' and '>'"; |
| neuper@37906 | 41 |
|
| akargl@42176 | 42 |
(*========== inhibit exn AK110725 ================================================ |
| neuper@37906 | 43 |
"----- check 'manually' the xml-output of calling functions ------"; |
| akargl@42176 | 44 |
formula2xml 1 (str2term str); |
| neuper@37906 | 45 |
|
| akargl@42176 | 46 |
(* AK110725 |
| akargl@42176 | 47 |
(*str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n" |
| akargl@42176 | 48 |
Failed to parse term*)*) |
| akargl@42176 | 49 |
"~~~~~ fun str2term, args:"; val (str) = (str); |
| akargl@42176 | 50 |
Thy_Info.get_theory "Isac"; |
| akargl@42176 | 51 |
|
| akargl@42176 | 52 |
parse_patt; |
| akargl@42176 | 53 |
parse_patt (Thy_Info.get_theory "Isac"); |
| akargl@42176 | 54 |
(*parse_patt (Thy_Info.get_theory "Isac") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n" |
| akargl@42176 | 55 |
Failed to parse term*)*) |
| akargl@42176 | 56 |
|
| akargl@42176 | 57 |
"~~~~~ fun parse_patt, args:"; val (thy, str) = ((Thy_Info.get_theory "Isac"), str); |
| akargl@42176 | 58 |
(thy, str) |
| akargl@42176 | 59 |
|>> thy2ctxt |
| akargl@42176 | 60 |
(*|-> ProofContext.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n" |
| akargl@42176 | 61 |
Failed to parse term*)*) |
| akargl@42176 | 62 |
|
| akargl@42176 | 63 |
ProofContext.read_term_pattern; |
| akargl@42176 | 64 |
(@{theory "Isac"}, str) |>> thy2ctxt;
|
| akargl@42176 | 65 |
"~~~~~ fun ProofContext.read_term_pattern, args:"; val () = (); |
| akargl@42176 | 66 |
(*AK110725 To be continued...*) |
| akargl@42176 | 67 |
*) |
| neuper@37906 | 68 |
(*==================================================================*) |
| neuper@37906 | 69 |
"-----------------------------------------------------------------"; |
| neuper@37906 | 70 |
"exported from struct --------------------------------------------"; |
| neuper@37906 | 71 |
"-----------------------------------------------------------------"; |
| akargl@42176 | 72 |
========== inhibit exn AK110725 ================================================*) |