equal
deleted
inserted
replaced
|
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 "../ProgLang/Script" begin |
|
9 |
|
10 syntax |
|
11 |
|
12 "_plus" :: 'a |
|
13 "_minus" :: 'a |
|
14 "_umin" :: 'a |
|
15 "_times" :: 'a |
|
16 |
|
17 translations |
|
18 |
|
19 "op +" => "_plus :: [real, real] => real" (*infixl 65 *) |
|
20 "op -" => "_minus :: [real, real] => real" (*infixl 65 *) |
|
21 "uminus"=> "_umin :: [real] => real" (*"- _" [80] 80*) |
|
22 "op *" => "_times :: [real, real] => real" (*infixl 70 *) |
|
23 |
|
24 ML {* |
|
25 val parse_translation = |
|
26 [("_plus", curry Term.list_comb (Syntax.const "op +")), |
|
27 ("_minus", curry Term.list_comb (Syntax.const "op -")), |
|
28 ("_umin", curry Term.list_comb (Syntax.const "uminus")), |
|
29 ("_times", curry Term.list_comb (Syntax.const "op *"))]; |
|
30 *} |
|
31 |
|
32 end |