|
1 (* Title: Pure/Syntax/standard_syntax.ML |
|
2 Author: Makarius |
|
3 |
|
4 Standard implementation of inner syntax operations. |
|
5 *) |
|
6 |
|
7 structure Standard_Syntax: sig end = |
|
8 struct |
|
9 |
|
10 fun parse_failed ctxt pos msg kind = |
|
11 cat_error msg ("Failed to parse " ^ kind ^ |
|
12 Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad "")); |
|
13 |
|
14 fun parse_sort ctxt text = |
|
15 let |
|
16 val (syms, pos) = Syntax.parse_token ctxt Markup.sort text; |
|
17 val S = |
|
18 Syntax.standard_parse_sort ctxt (ProofContext.type_context ctxt) |
|
19 (ProofContext.syn_of ctxt) (syms, pos) |
|
20 handle ERROR msg => parse_failed ctxt pos msg "sort"; |
|
21 in Type.minimize_sort (ProofContext.tsig_of ctxt) S end; |
|
22 |
|
23 fun parse_typ ctxt text = |
|
24 let |
|
25 val (syms, pos) = Syntax.parse_token ctxt Markup.typ text; |
|
26 val T = |
|
27 Syntax.standard_parse_typ ctxt (ProofContext.type_context ctxt) |
|
28 (ProofContext.syn_of ctxt) (ProofContext.get_sort ctxt) (syms, pos) |
|
29 handle ERROR msg => parse_failed ctxt pos msg "type"; |
|
30 in T end; |
|
31 |
|
32 fun parse_term T ctxt text = |
|
33 let |
|
34 val (T', _) = Type_Infer.paramify_dummies T 0; |
|
35 val (markup, kind) = |
|
36 if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term"); |
|
37 val (syms, pos) = Syntax.parse_token ctxt markup text; |
|
38 |
|
39 val default_root = Config.get ctxt Syntax.default_root; |
|
40 val root = |
|
41 (case T' of |
|
42 Type (c, _) => |
|
43 if c <> "prop" andalso Type.is_logtype (ProofContext.tsig_of ctxt) c |
|
44 then default_root else c |
|
45 | _ => default_root); |
|
46 |
|
47 fun check t = (Syntax.check_term ctxt (Type.constraint T' t); Exn.Result t) |
|
48 handle exn as ERROR _ => Exn.Exn exn; |
|
49 val t = |
|
50 Syntax.standard_parse_term check ctxt |
|
51 (ProofContext.type_context ctxt) (ProofContext.term_context ctxt) |
|
52 (ProofContext.syn_of ctxt) root (syms, pos) |
|
53 handle ERROR msg => parse_failed ctxt pos msg kind; |
|
54 in t end; |
|
55 |
|
56 |
|
57 fun unparse_sort ctxt = |
|
58 Syntax.standard_unparse_sort {extern_class = Type.extern_class (ProofContext.tsig_of ctxt)} |
|
59 ctxt (ProofContext.syn_of ctxt); |
|
60 |
|
61 fun unparse_typ ctxt = |
|
62 let |
|
63 val tsig = ProofContext.tsig_of ctxt; |
|
64 val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig}; |
|
65 in Syntax.standard_unparse_typ extern ctxt (ProofContext.syn_of ctxt) end; |
|
66 |
|
67 fun unparse_term ctxt = |
|
68 let |
|
69 val tsig = ProofContext.tsig_of ctxt; |
|
70 val syntax = ProofContext.syntax_of ctxt; |
|
71 val consts = ProofContext.consts_of ctxt; |
|
72 val extern = |
|
73 {extern_class = Type.extern_class tsig, |
|
74 extern_type = Type.extern_type tsig, |
|
75 extern_const = Consts.extern consts}; |
|
76 in |
|
77 Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt |
|
78 (Local_Syntax.syn_of syntax) (not (Pure_Thy.old_appl_syntax (ProofContext.theory_of ctxt))) |
|
79 end; |
|
80 |
|
81 |
|
82 val _ = Syntax.install_operations |
|
83 {parse_sort = parse_sort, |
|
84 parse_typ = parse_typ, |
|
85 parse_term = parse_term dummyT, |
|
86 parse_prop = parse_term propT, |
|
87 unparse_sort = unparse_sort, |
|
88 unparse_typ = unparse_typ, |
|
89 unparse_term = unparse_term}; |
|
90 |
|
91 end; |