author | wenzelm |
Sat, 07 Dec 2024 23:50:18 +0100 | |
changeset 81558 | b57996a0688c |
parent 67721 | 5348bea4accd |
child 81601 | 26ff119fb140 |
permissions | -rw-r--r-- |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Syntax/simple_syntax.ML |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
3 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
4 |
Simple syntax for types and terms --- for bootstrapping Pure. |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
5 |
*) |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
6 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
7 |
signature SIMPLE_SYNTAX = |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
8 |
sig |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
9 |
val read_typ: string -> typ |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
10 |
val read_term: string -> term |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
11 |
val read_prop: string -> term |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
12 |
end; |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
13 |
|
33384 | 14 |
structure Simple_Syntax: SIMPLE_SYNTAX = |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
15 |
struct |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
16 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
17 |
(* scanning tokens *) |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
18 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
19 |
val lexicon = Scan.make_lexicon |
67721 | 20 |
(map Symbol.explode ["\<And>", "\<lambda>", "(", ")", ".", "::", "\<equiv>", "\<Longrightarrow>", "\<Rightarrow>", "&&&", "CONST"]); |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
21 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
22 |
fun read scan s = |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
23 |
(case |
62751 | 24 |
Symbol_Pos.explode0 s |> |
24246 | 25 |
Lexicon.tokenize lexicon false |> |
27888
7ed38f1d11de
filter Lexicon.is_proper -- Lexicon.tokenize now includes improper tokens;
wenzelm
parents:
27802
diff
changeset
|
26 |
filter Lexicon.is_proper |> |
27802
1eddcd7dda2d
datatype token: maintain range, tuned representation;
wenzelm
parents:
27774
diff
changeset
|
27 |
Scan.read Lexicon.stopper scan of |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
28 |
SOME x => x |
24246 | 29 |
| NONE => error ("Malformed input: " ^ quote s)); |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
30 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
31 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
32 |
(* basic scanners *) |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
33 |
|
67552 | 34 |
fun $$ s = |
35 |
Scan.some (fn tok => |
|
36 |
if Lexicon.is_literal tok andalso s = Lexicon.str_of_token tok then SOME s else NONE); |
|
27802
1eddcd7dda2d
datatype token: maintain range, tuned representation;
wenzelm
parents:
27774
diff
changeset
|
37 |
|
25999 | 38 |
fun enum1 s scan = scan ::: Scan.repeat ($$ s |-- scan); |
39 |
fun enum2 s scan = scan ::: Scan.repeat1 ($$ s |-- scan); |
|
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
40 |
|
67553 | 41 |
fun kind k = |
42 |
Scan.some (fn tok => |
|
43 |
if Lexicon.kind_of_token tok = k then SOME (Lexicon.str_of_token tok) else NONE); |
|
27802
1eddcd7dda2d
datatype token: maintain range, tuned representation;
wenzelm
parents:
27774
diff
changeset
|
44 |
|
67553 | 45 |
val tfree = kind Lexicon.Type_Ident; |
46 |
val ident = kind Lexicon.Ident; |
|
47 |
val var = kind Lexicon.Var >> (Lexicon.read_indexname o unprefix "?"); |
|
48 |
val long_ident = kind Lexicon.Long_Ident; |
|
27802
1eddcd7dda2d
datatype token: maintain range, tuned representation;
wenzelm
parents:
27774
diff
changeset
|
49 |
|
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
50 |
val const = long_ident || ident; |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
51 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
52 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
53 |
(* types *) |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
54 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
55 |
(* |
67721 | 56 |
typ = typ1 \<Rightarrow> ... \<Rightarrow> typ1 |
24237 | 57 |
| typ1 |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
58 |
typ1 = typ2 const ... const |
24237 | 59 |
| typ2 |
60 |
typ2 = tfree |
|
61 |
| const |
|
62 |
| ( typ ) |
|
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
63 |
*) |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
64 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
65 |
fun typ x = |
67721 | 66 |
(enum1 "\<Rightarrow>" typ1 >> (op ---> o split_last)) x |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
67 |
and typ1 x = |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
68 |
(typ2 -- Scan.repeat const >> (fn (T, cs) => fold (fn c => fn U => Type (c, [U])) cs T)) x |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
69 |
and typ2 x = |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
70 |
(tfree >> (fn a => TFree (a, [])) || |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
71 |
const >> (fn c => Type (c, [])) || |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
72 |
$$ "(" |-- typ --| $$ ")") x; |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
73 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
74 |
val read_typ = read typ; |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
75 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
76 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
77 |
(* terms *) |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
78 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
79 |
(* |
67721 | 80 |
term = \<And>ident :: typ. term |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
81 |
| term1 |
67721 | 82 |
term1 = term2 \<Longrightarrow> ... \<Longrightarrow> term2 |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
83 |
| term2 |
67721 | 84 |
term2 = term3 \<equiv> term2 |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
27888
diff
changeset
|
85 |
| term3 &&& term2 |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
86 |
| term3 |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
87 |
term3 = ident :: typ |
24246 | 88 |
| var :: typ |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
89 |
| CONST const :: typ |
67721 | 90 |
| \<lambda>ident :: typ. term3 |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
91 |
| term4 |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
92 |
term4 = term5 ... term5 |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
93 |
| term5 |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
94 |
term5 = ident |
24246 | 95 |
| var |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
96 |
| CONST const |
24237 | 97 |
| ( term ) |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
98 |
*) |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
99 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
100 |
local |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
101 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
102 |
val constraint = $$ "::" |-- typ; |
24246 | 103 |
val idt = ident -- constraint; |
104 |
val bind = idt --| $$ "."; |
|
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
105 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
106 |
fun term env T x = |
67721 | 107 |
($$ "\<And>" |-- bind :|-- (fn v => term (v :: env) propT >> (Logic.all (Free v))) || |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
108 |
term1 env T) x |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
109 |
and term1 env T x = |
67721 | 110 |
(enum2 "\<Longrightarrow>" (term2 env propT) >> foldr1 Logic.mk_implies || |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
111 |
term2 env T) x |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
112 |
and term2 env T x = |
56245 | 113 |
(equal env || |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
27888
diff
changeset
|
114 |
term3 env propT -- ($$ "&&&" |-- term2 env propT) >> Logic.mk_conjunction || |
24246 | 115 |
term3 env T) x |
56245 | 116 |
and equal env x = |
67721 | 117 |
(term3 env dummyT -- ($$ "\<equiv>" |-- term2 env dummyT) >> (fn (t, u) => |
56245 | 118 |
Const ("Pure.eq", Term.fastype_of t --> Term.fastype_of u --> propT) $ t $ u)) x |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
119 |
and term3 env T x = |
24246 | 120 |
(idt >> Free || |
121 |
var -- constraint >> Var || |
|
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
122 |
$$ "CONST" |-- const -- constraint >> Const || |
67721 | 123 |
$$ "\<lambda>" |-- bind :|-- (fn v => term3 (v :: env) dummyT >> lambda (Free v)) || |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
124 |
term4 env T) x |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
125 |
and term4 env T x = |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
126 |
(term5 env dummyT -- Scan.repeat1 (term5 env dummyT) >> Term.list_comb || |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
127 |
term5 env T) x |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
128 |
and term5 env T x = |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
129 |
(ident >> (fn a => Free (a, the_default T (AList.lookup (op =) env a))) || |
24246 | 130 |
var >> (fn xi => Var (xi, T)) || |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
131 |
$$ "CONST" |-- const >> (fn c => Const (c, T)) || |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
132 |
$$ "(" |-- term env T --| $$ ")") x; |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
133 |
|
24246 | 134 |
fun read_tm T s = |
67721 | 135 |
let |
136 |
val t = read (term [] T) s |
|
137 |
handle ERROR msg => cat_error ("Malformed input " ^ quote s) msg; |
|
138 |
in |
|
24246 | 139 |
if can (Term.map_types Term.no_dummyT) t then t |
140 |
else error ("Unspecified types in input: " ^ quote s) |
|
141 |
end; |
|
142 |
||
24487 | 143 |
in |
144 |
||
24246 | 145 |
val read_term = read_tm dummyT; |
146 |
val read_prop = read_tm propT; |
|
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
147 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
148 |
end; |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
149 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
150 |
end; |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
151 |