48 end; |
48 end; |
49 |
49 |
50 signature SEXTENSION1 = |
50 signature SEXTENSION1 = |
51 sig |
51 sig |
52 include SEXTENSION0 |
52 include SEXTENSION0 |
53 val empty_sext: sext |
53 local open Parser.SynExt.Ast in |
54 val simple_sext: mixfix list -> sext |
54 val empty_sext: sext |
55 val constants: sext -> (string list * string) list |
55 val simple_sext: mixfix list -> sext |
56 val pure_sext: sext |
56 val constants: sext -> (string list * string) list |
57 val syntax_types: string list |
57 val pure_sext: sext |
58 val syntax_consts: (string list * string) list |
58 val syntax_types: string list |
59 val constrainAbsC: string |
59 val syntax_consts: (string list * string) list |
|
60 val constrainAbsC: string |
|
61 val pure_trfuns: |
|
62 (string * (ast list -> ast)) list * |
|
63 (string * (term list -> term)) list * |
|
64 (string * (term list -> term)) list * |
|
65 (string * (ast list -> ast)) list |
|
66 end |
60 end; |
67 end; |
61 |
68 |
62 signature SEXTENSION = |
69 signature SEXTENSION = |
63 sig |
70 sig |
64 include SEXTENSION1 |
71 include SEXTENSION1 |
65 local open Parser Parser.SynExt Parser.SynExt.Ast in |
72 local open Parser Parser.SynExt Parser.SynExt.Ast in |
66 val xrules_of: sext -> xrule list |
73 val xrules_of: sext -> xrule list |
67 val abs_tr': term -> term |
74 val abs_tr': term -> term |
|
75 val prop_tr': bool -> term -> term |
68 val appl_ast_tr': ast * ast list -> ast |
76 val appl_ast_tr': ast * ast list -> ast |
69 val syn_ext_of_sext: string list -> string list -> string list -> (string -> typ) -> sext -> syn_ext |
77 val syn_ext_of_sext: string list -> string list -> string list -> (string -> typ) -> sext -> syn_ext |
70 val pt_to_ast: (string -> (ast list -> ast) option) -> parsetree -> ast |
78 val pt_to_ast: (string -> (ast list -> ast) option) -> parsetree -> ast |
71 val ast_to_term: (string -> (term list -> term) option) -> ast -> term |
79 val ast_to_term: (string -> (term list -> term) option) -> ast -> term |
72 val apropC: string |
|
73 end |
80 end |
74 end; |
81 end; |
75 |
82 |
76 functor SExtensionFun(Parser: PARSER): SEXTENSION = |
83 functor SExtensionFun(structure TypeExt: TYPE_EXT and Parser: PARSER |
|
84 sharing TypeExt.SynExt = Parser.SynExt): SEXTENSION = |
77 struct |
85 struct |
78 |
86 |
79 structure Parser = Parser; |
87 structure Parser = Parser; |
80 open Parser.Lexicon Parser.SynExt.Ast Parser.SynExt Parser; |
88 open TypeExt Parser.Lexicon Parser.SynExt.Ast Parser.SynExt Parser; |
81 |
89 |
82 |
90 |
83 (** datatype sext **) |
91 (** datatype sext **) (* FIXME remove *) |
84 |
92 |
85 datatype mixfix = |
93 datatype mixfix = |
86 Mixfix of string * string * string * int list * int | |
94 Mixfix of string * string * string * int list * int | |
87 Delimfix of string * string * string | |
95 Delimfix of string * string * string | |
88 Infixl of string * string * int | |
96 Infixl of string * string * int | |
89 Infixr of string * string * int | |
97 Infixr of string * string * int | |
90 Binder of string * string * string * int * int | |
98 Binder of string * string * string * int * int | |
91 TInfixl of string * string * int | |
99 TInfixl of string * string * int | |
92 TInfixr of string * string * int; |
100 TInfixr of string * string * int; |
93 |
101 |
|
102 |
|
103 (* FIXME -> syntax.ML, BASIC_SYNTAX, SYNTAX *) |
94 datatype xrule = |
104 datatype xrule = |
95 op |-> of (string * string) * (string * string) | |
105 op |-> of (string * string) * (string * string) | |
96 op <-| of (string * string) * (string * string) | |
106 op <-| of (string * string) * (string * string) | |
97 op <-> of (string * string) * (string * string); |
107 op <-> of (string * string) * (string * string); |
98 |
108 |
164 | lambda_ast_tr (*"_lambda"*) asts = raise_ast "lambda_ast_tr" asts; |
179 | lambda_ast_tr (*"_lambda"*) asts = raise_ast "lambda_ast_tr" asts; |
165 |
180 |
166 fun abs_tr (*"_abs"*) [Free (x, T), body] = absfree (x, T, body) |
181 fun abs_tr (*"_abs"*) [Free (x, T), body] = absfree (x, T, body) |
167 | abs_tr (*"_abs"*) (ts as [Const (c, _) $ Free (x, T) $ tT, body]) = |
182 | abs_tr (*"_abs"*) (ts as [Const (c, _) $ Free (x, T) $ tT, body]) = |
168 if c = constrainC then |
183 if c = constrainC then |
169 Const ("_constrainAbs", dummyT) $ absfree (x, T, body) $ tT |
184 const "_constrainAbs" $ absfree (x, T, body) $ tT |
170 else raise_term "abs_tr" ts |
185 else raise_term "abs_tr" ts |
171 | abs_tr (*"_abs"*) ts = raise_term "abs_tr" ts; |
186 | abs_tr (*"_abs"*) ts = raise_term "abs_tr" ts; |
172 |
187 |
173 |
188 |
174 (* nondependent abstraction *) |
189 (* nondependent abstraction *) |
179 |
194 |
180 (* binder *) |
195 (* binder *) |
181 |
196 |
182 fun mk_binder_tr (sy, name) = |
197 fun mk_binder_tr (sy, name) = |
183 let |
198 let |
184 val const = Const (name, dummyT); |
199 fun tr (Free (x, T), t) = const name $ absfree (x, T, t) |
185 |
|
186 fun tr (Free (x, T), t) = const $ absfree (x, T, t) |
|
187 | tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t)) |
200 | tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t)) |
188 | tr (t1 as Const (c, _) $ Free (x, T) $ tT, t) = |
201 | tr (t1 as Const (c, _) $ Free (x, T) $ tT, t) = |
189 if c = constrainC then |
202 if c = constrainC then |
190 const $ (Const ("_constrainAbs", dummyT) $ absfree (x, T, t) $ tT) |
203 const name $ (const "_constrainAbs" $ absfree (x, T, t) $ tT) |
191 else raise_term "binder_tr" [t1, t] |
204 else raise_term "binder_tr" [t1, t] |
192 | tr (t1, t2) = raise_term "binder_tr" [t1, t2]; |
205 | tr (t1, t2) = raise_term "binder_tr" [t1, t2]; |
193 |
206 |
194 fun binder_tr (*sy*) [idts, body] = tr (idts, body) |
207 fun binder_tr (*sy*) [idts, body] = tr (idts, body) |
195 | binder_tr (*sy*) ts = raise_term "binder_tr" ts; |
208 | binder_tr (*sy*) ts = raise_term "binder_tr" ts; |
196 in |
209 in |
197 (sy, binder_tr) |
210 (sy, binder_tr) |
198 end; |
211 end; |
199 |
212 |
200 |
213 |
201 (* atomic props *) |
214 (* meta propositions *) |
202 |
215 |
203 fun aprop_tr (*"_aprop"*) [t] = |
216 fun aprop_tr (*"_aprop"*) [t] = const constrainC $ t $ const "prop" |
204 Const (constrainC, dummyT) $ t $ Free ("prop", dummyT) |
|
205 | aprop_tr (*"_aprop"*) ts = raise_term "aprop_tr" ts; |
217 | aprop_tr (*"_aprop"*) ts = raise_term "aprop_tr" ts; |
|
218 |
|
219 fun insort_tr (*"_insort"*) [ty, srt] = |
|
220 srt $ (const constrainC $ const "TYPE" $ (const "itself" $ ty)) |
|
221 | insort_tr (*"_insort"*) ts = raise_term "insort_tr" ts; |
206 |
222 |
207 |
223 |
208 (* meta implication *) |
224 (* meta implication *) |
209 |
225 |
210 fun bigimpl_ast_tr (*"_bigimpl"*) [asms, concl] = |
226 fun bigimpl_ast_tr (*"_bigimpl"*) [asms, concl] = |
295 |
311 |
296 fun mk_binder_tr' (name, sy) = |
312 fun mk_binder_tr' (name, sy) = |
297 let |
313 let |
298 fun mk_idts [] = raise Match (*abort translation*) |
314 fun mk_idts [] = raise Match (*abort translation*) |
299 | mk_idts [idt] = idt |
315 | mk_idts [idt] = idt |
300 | mk_idts (idt :: idts) = Const ("_idts", dummyT) $ idt $ mk_idts idts; |
316 | mk_idts (idt :: idts) = const "_idts" $ idt $ mk_idts idts; |
301 |
317 |
302 fun tr' t = |
318 fun tr' t = |
303 let |
319 let |
304 val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t; |
320 val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t; |
305 in |
321 in |
306 Const (sy, dummyT) $ mk_idts xs $ bd |
322 const sy $ mk_idts xs $ bd |
307 end; |
323 end; |
308 |
324 |
309 fun binder_tr' (*name*) (t :: ts) = |
325 fun binder_tr' (*name*) (t :: ts) = |
310 list_comb (tr' (Const (name, dummyT) $ t), ts) |
326 list_comb (tr' (const name $ t), ts) |
311 | binder_tr' (*name*) [] = raise Match; |
327 | binder_tr' (*name*) [] = raise Match; |
312 in |
328 in |
313 (name, binder_tr') |
329 (name, binder_tr') |
314 end; |
330 end; |
315 |
331 |
321 Appl [Constant "_idts", Appl [Constant "_idtyp", x, ty], xs] |
337 Appl [Constant "_idts", Appl [Constant "_idtyp", x, ty], xs] |
322 else raise Match |
338 else raise Match |
323 | idts_ast_tr' (*"_idts"*) _ = raise Match; |
339 | idts_ast_tr' (*"_idts"*) _ = raise Match; |
324 |
340 |
325 |
341 |
|
342 (* meta propositions *) |
|
343 |
|
344 fun prop_tr' show_sorts tm = |
|
345 let |
|
346 fun aprop t = const "_aprop" $ t; |
|
347 |
|
348 fun is_prop tys t = |
|
349 fastype_of1 (tys, t) = propT handle TERM _ => false; |
|
350 |
|
351 fun tr' _ (t as Const _) = t |
|
352 | tr' _ (t as Free (x, ty)) = |
|
353 if ty = propT then aprop (Free (x, dummyT)) else t |
|
354 | tr' _ (t as Var (xi, ty)) = |
|
355 if ty = propT then aprop (Var (xi, dummyT)) else t |
|
356 | tr' tys (t as Bound _) = |
|
357 if is_prop tys t then aprop t else t |
|
358 | tr' tys (Abs (x, ty, t)) = Abs (x, ty, tr' (ty :: tys) t) |
|
359 | tr' tys (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [ty])))) = |
|
360 if is_prop tys t then |
|
361 const "_insort" $ term_of_typ show_sorts ty $ tr' tys t1 |
|
362 else tr' tys t1 $ tr' tys t2 |
|
363 | tr' tys (t as t1 $ t2) = |
|
364 (if is_Const (head_of t) orelse not (is_prop tys t) |
|
365 then I else aprop) (tr' tys t1 $ tr' tys t2); |
|
366 in |
|
367 tr' [] tm |
|
368 end; |
|
369 |
|
370 |
326 (* meta implication *) |
371 (* meta implication *) |
327 |
372 |
328 fun impl_ast_tr' (*"==>"*) asts = |
373 fun impl_ast_tr' (*"==>"*) asts = |
329 (case unfold_ast_p "==>" (Appl (Constant "==>" :: asts)) of |
374 (case unfold_ast_p "==>" (Appl (Constant "==>" :: asts)) of |
330 (asms as _ :: _ :: _, concl) |
375 (asms as _ :: _ :: _, concl) |
335 (* dependent / nondependent quantifiers *) |
380 (* dependent / nondependent quantifiers *) |
336 |
381 |
337 fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) = |
382 fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) = |
338 if 0 mem (loose_bnos B) then |
383 if 0 mem (loose_bnos B) then |
339 let val (x', B') = variant_abs (x, dummyT, B); |
384 let val (x', B') = variant_abs (x, dummyT, B); |
340 in list_comb (Const (q, dummyT) $ Free (x', T) $ A $ B', ts) end |
385 in list_comb (const q $ Free (x', T) $ A $ B', ts) end |
341 else list_comb (Const (r, dummyT) $ A $ B, ts) |
386 else list_comb (const r $ A $ B, ts) |
342 | dependent_tr' _ _ = raise Match; |
387 | dependent_tr' _ _ = raise Match; |
343 |
388 |
344 |
389 |
345 (* implode atoms *) |
390 (* implode atoms *) |
346 |
391 |
486 term_of ast |
532 term_of ast |
487 end; |
533 end; |
488 |
534 |
489 |
535 |
490 |
536 |
491 (** the Pure syntax **) |
537 (** pure_trfuns **) |
|
538 |
|
539 val pure_trfuns = |
|
540 ([(applC, appl_ast_tr), ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), |
|
541 ("_bigimpl", bigimpl_ast_tr)], |
|
542 [("_abs", abs_tr), ("_aprop", aprop_tr), ("_insort", insort_tr), ("_K", k_tr), |
|
543 ("_explode", explode_tr)], |
|
544 [], |
|
545 [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'), ("==>", impl_ast_tr'), |
|
546 ("_implode", implode_ast_tr')]); |
|
547 |
|
548 val constrainAbsC = "_constrainAbs"; |
|
549 |
|
550 |
|
551 (** the Pure syntax **) (* FIXME remove *) |
492 |
552 |
493 val pure_sext = |
553 val pure_sext = |
494 NewSext { |
554 NewSext { |
495 mixfix = [ |
555 mixfix = [ |
496 Mixfix ("(3%_./ _)", "[idts, 'a] => ('b => 'a)", "_lambda", [0], 0), |
556 Mixfix ("(3%_./ _)", "[idts, 'a] => ('b => 'a)", "_lambda", [0], 0), |
524 val syntax_types = terminals @ ["syntax", logic, "type", "types", "sort", |
584 val syntax_types = terminals @ ["syntax", logic, "type", "types", "sort", |
525 "classes", args, "idt", "idts", "aprop", "asms"]; |
585 "classes", args, "idt", "idts", "aprop", "asms"]; |
526 |
586 |
527 val syntax_consts = [(["_K", "_explode", "_implode"], "syntax")]; |
587 val syntax_consts = [(["_K", "_explode", "_implode"], "syntax")]; |
528 |
588 |
529 val constrainAbsC = "_constrainAbs"; |
|
530 val apropC = "_aprop"; |
|
531 |
|
532 |
589 |
533 end; |
590 end; |
534 |
591 |