1 (* Title: fixed type for _RE_parsing of strings from frontend |
|
2 Author: Walther Neuper |
|
3 9911xx |
|
4 (c) due to copyright terms |
|
5 with hints from Markus Wenzel |
|
6 *) |
|
7 |
|
8 theory Typefix imports "../Scripts/Script" |
|
9 uses ("../Scripts/scrtools.sml") |
|
10 ("../ME/mstools.sml") ("../ME/ctree.sml") ("../ME/ptyps.sml") |
|
11 ("../ME/generate.sml") ("../ME/calchead.sml") ("../ME/appl.sml") |
|
12 ("../ME/rewtools.sml") ("../ME/script.sml") ("../ME/solve.sml") |
|
13 ("../ME/inform.sml") ("../ME/mathengine.sml") |
|
14 ("../xmlsrc/mathml.sml") ("../xmlsrc/datatypes.sml") |
|
15 ("../xmlsrc/pbl-met-hierarchy.sml") ("../xmlsrc/thy-hierarchy.sml") |
|
16 ("../xmlsrc/interface-xml.sml") ("../FE-interface/messages.sml") |
|
17 ("../FE-interface/states.sml") ("../FE-interface/interface.sml") |
|
18 ("../print_exn_G.sml") |
|
19 begin |
|
20 use "../Scripts/scrtools.sml" |
|
21 |
|
22 use "../ME/mstools.sml" |
|
23 use "../ME/ctree.sml" |
|
24 use "../ME/ptyps.sml" |
|
25 use "../ME/generate.sml" |
|
26 use "../ME/calchead.sml" |
|
27 use "../ME/appl.sml" |
|
28 use "../ME/rewtools.sml" |
|
29 use "../ME/script.sml" |
|
30 use "../ME/solve.sml" |
|
31 use "../ME/inform.sml" |
|
32 use "../ME/mathengine.sml" |
|
33 |
|
34 use "../xmlsrc/mathml.sml" |
|
35 use "../xmlsrc/datatypes.sml" |
|
36 use "../xmlsrc/pbl-met-hierarchy.sml" |
|
37 use "../xmlsrc/thy-hierarchy.sml" |
|
38 use "../xmlsrc/interface-xml.sml" |
|
39 |
|
40 use "../FE-interface/messages.sml" |
|
41 use "../FE-interface/states.sml" |
|
42 use "../FE-interface/interface.sml" |
|
43 |
|
44 use "../print_exn_G.sml" |
|
45 |
|
46 syntax |
|
47 |
|
48 "_plus" :: 'a |
|
49 "_minus" :: 'a |
|
50 "_umin" :: 'a |
|
51 "_times" :: 'a |
|
52 |
|
53 translations |
|
54 |
|
55 "op +" => "_plus :: [real, real] => real" (*infixl 65 *) |
|
56 "op -" => "_minus :: [real, real] => real" (*infixl 65 *) |
|
57 "uminus"=> "_umin :: [real] => real" (*"- _" [80] 80*) |
|
58 "op *" => "_times :: [real, real] => real" (*infixl 70 *) |
|
59 |
|
60 ML {* |
|
61 val parse_translation = |
|
62 [("_plus", curry Term.list_comb (Syntax.const "op +")), |
|
63 ("_minus", curry Term.list_comb (Syntax.const "op -")), |
|
64 ("_umin", curry Term.list_comb (Syntax.const "uminus")), |
|
65 ("_times", curry Term.list_comb (Syntax.const "op *"))]; |
|
66 *} |
|
67 |
|
68 end |
|