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