author | haftmann |
Tue, 23 Sep 2008 18:11:44 +0200 | |
changeset 28337 | 93964076e7b8 |
parent 27888 | 7ed38f1d11de |
child 28856 | 5e009a80fe6d |
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 |
ID: $Id$ |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
4 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
5 |
Simple syntax for types and terms --- for bootstrapping Pure. |
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 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
8 |
signature SIMPLE_SYNTAX = |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
9 |
sig |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
10 |
val read_typ: string -> typ |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
11 |
val read_term: string -> term |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
12 |
val read_prop: string -> term |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
13 |
end; |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
14 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
15 |
structure SimpleSyntax: SIMPLE_SYNTAX = |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
16 |
struct |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
17 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
18 |
(* scanning tokens *) |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
19 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
20 |
val lexicon = Scan.make_lexicon |
24246 | 21 |
(map Symbol.explode ["!!", "%", "(", ")", ".", "::", "==", "==>", "=?=", "=>", "&&", "CONST"]); |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
22 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
23 |
fun read scan s = |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
24 |
(case |
27774 | 25 |
SymbolPos.explode (s, Position.none) |> |
24246 | 26 |
Lexicon.tokenize lexicon false |> |
27888
7ed38f1d11de
filter Lexicon.is_proper -- Lexicon.tokenize now includes improper tokens;
wenzelm
parents:
27802
diff
changeset
|
27 |
filter Lexicon.is_proper |> |
27802
1eddcd7dda2d
datatype token: maintain range, tuned representation;
wenzelm
parents:
27774
diff
changeset
|
28 |
Scan.read Lexicon.stopper scan of |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
29 |
SOME x => x |
24246 | 30 |
| NONE => error ("Malformed input: " ^ quote s)); |
24236
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 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
33 |
(* basic scanners *) |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
34 |
|
27802
1eddcd7dda2d
datatype token: maintain range, tuned representation;
wenzelm
parents:
27774
diff
changeset
|
35 |
fun $$ s = Scan.some (fn Lexicon.Token (Lexicon.Literal, s', _) => |
1eddcd7dda2d
datatype token: maintain range, tuned representation;
wenzelm
parents:
27774
diff
changeset
|
36 |
if s = s' then SOME s else NONE | _ => NONE); |
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 |
|
27802
1eddcd7dda2d
datatype token: maintain range, tuned representation;
wenzelm
parents:
27774
diff
changeset
|
41 |
val tfree = Scan.some (fn Lexicon.Token (Lexicon.TFreeSy, s, _) => SOME s | _ => NONE); |
1eddcd7dda2d
datatype token: maintain range, tuned representation;
wenzelm
parents:
27774
diff
changeset
|
42 |
val ident = Scan.some (fn Lexicon.Token (Lexicon.IdentSy, s, _) => SOME s | _ => NONE); |
1eddcd7dda2d
datatype token: maintain range, tuned representation;
wenzelm
parents:
27774
diff
changeset
|
43 |
|
1eddcd7dda2d
datatype token: maintain range, tuned representation;
wenzelm
parents:
27774
diff
changeset
|
44 |
val var = Scan.some (fn Lexicon.Token (Lexicon.VarSy, s, _) => |
1eddcd7dda2d
datatype token: maintain range, tuned representation;
wenzelm
parents:
27774
diff
changeset
|
45 |
SOME (Lexicon.read_indexname (unprefix "?" s)) | _ => NONE); |
1eddcd7dda2d
datatype token: maintain range, tuned representation;
wenzelm
parents:
27774
diff
changeset
|
46 |
|
1eddcd7dda2d
datatype token: maintain range, tuned representation;
wenzelm
parents:
27774
diff
changeset
|
47 |
val long_ident = Scan.some (fn Lexicon.Token (Lexicon.LongIdentSy, s, _) => SOME s | _ => NONE); |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
48 |
val const = long_ident || ident; |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
49 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
50 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
51 |
(* types *) |
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 |
(* |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
54 |
typ = typ1 => ... => typ1 |
24237 | 55 |
| typ1 |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
56 |
typ1 = typ2 const ... const |
24237 | 57 |
| typ2 |
58 |
typ2 = tfree |
|
59 |
| const |
|
60 |
| ( typ ) |
|
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
61 |
*) |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
62 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
63 |
fun typ x = |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
64 |
(enum1 "=>" typ1 >> (op ---> o split_last)) x |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
65 |
and typ1 x = |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
66 |
(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
|
67 |
and typ2 x = |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
68 |
(tfree >> (fn a => TFree (a, [])) || |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
69 |
const >> (fn c => Type (c, [])) || |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
70 |
$$ "(" |-- typ --| $$ ")") x; |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
71 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
72 |
val read_typ = read typ; |
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 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
75 |
(* terms *) |
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 |
(* |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
78 |
term = !!ident :: typ. term |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
79 |
| term1 |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
80 |
term1 = term2 ==> ... ==> term2 |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
81 |
| term2 |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
82 |
term2 = term3 == term2 |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
83 |
| term3 =?= term2 |
24246 | 84 |
| term3 && term2 |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
85 |
| term3 |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
86 |
term3 = ident :: typ |
24246 | 87 |
| var :: typ |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
88 |
| CONST const :: typ |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
89 |
| %ident :: typ. term3 |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
90 |
| term4 |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
91 |
term4 = term5 ... term5 |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
92 |
| term5 |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
93 |
term5 = ident |
24246 | 94 |
| var |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
95 |
| CONST const |
24237 | 96 |
| ( term ) |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
97 |
*) |
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 |
local |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
100 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
101 |
val constraint = $$ "::" |-- typ; |
24246 | 102 |
val idt = ident -- constraint; |
103 |
val bind = idt --| $$ "."; |
|
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
104 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
105 |
fun term env T x = |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
106 |
($$ "!!" |-- bind :|-- (fn v => |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
107 |
term (v :: env) propT >> (fn B => Term.all (#2 v) $ lambda (Free v) B)) || |
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 = |
24262 | 110 |
(enum2 "==>" (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 = |
24246 | 113 |
(equal env "==" || equal env "=?=" || |
24262 | 114 |
term3 env propT -- ($$ "&&" |-- term2 env propT) >> Logic.mk_conjunction || |
24246 | 115 |
term3 env T) x |
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
116 |
and equal env eq x = |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
117 |
(term3 env dummyT -- ($$ eq |-- term2 env dummyT) >> (fn (t, u) => |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
118 |
Const (eq, Term.fastype_of t --> Term.fastype_of u --> propT) $ t $ u)) x |
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 || |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
123 |
$$ "%" |-- bind :|-- (fn v => term3 (v :: env) dummyT >> lambda (Free v)) || |
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 = |
135 |
let val t = read (term [] T) s in |
|
136 |
if can (Term.map_types Term.no_dummyT) t then t |
|
137 |
else error ("Unspecified types in input: " ^ quote s) |
|
138 |
end; |
|
139 |
||
24487 | 140 |
in |
141 |
||
24246 | 142 |
val read_term = read_tm dummyT; |
143 |
val read_prop = read_tm propT; |
|
24236
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
144 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
145 |
end; |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
146 |
|
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
147 |
end; |
d8b05073edc7
Simple syntax for types and terms --- for bootstrapping Pure.
wenzelm
parents:
diff
changeset
|
148 |