--- a/src/Pure/Syntax/extension.ML Tue Nov 30 10:55:43 1993 +0100
+++ b/src/Pure/Syntax/extension.ML Tue Nov 30 11:04:07 1993 +0100
@@ -3,10 +3,6 @@
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
External grammar definition (internal interface).
-
-TODO:
- ext = {roots, mfix, extra_consts} | {.._translation} | {.._rules} (?)
- extend_xgram: move '.. \\ roots1' to Syntax.extend_tables (no?)
*)
signature EXTENSION0 =
@@ -83,21 +79,36 @@
(* ext_components *)
-fun ext_components (Ext ext) =
- {roots = #roots ext, mfix = #mfix ext, extra_consts = #extra_consts ext,
+fun ext_components (Ext ext) = {
+ roots = #roots ext,
+ mfix = #mfix ext,
+ extra_consts = #extra_consts ext,
parse_ast_translation = #parse_ast_translation ext,
+ parse_rules = [],
parse_translation = #parse_translation ext,
print_translation = #print_translation ext,
- print_ast_translation = #print_ast_translation ext,
- parse_rules = [], print_rules = []}
- | ext_components (ExtRules {parse_rules, print_rules}) =
- {parse_rules = parse_rules, print_rules = print_rules, roots = [], mfix = [],
- extra_consts = [], parse_ast_translation = [], parse_translation = [],
- print_translation = [], print_ast_translation = []}
- | ext_components (ExtRoots roots) =
- {roots = roots, mfix = [], extra_consts = [], parse_ast_translation = [],
- parse_rules = [], parse_translation = [], print_translation = [],
- print_rules = [], print_ast_translation = []};
+ print_rules = [],
+ print_ast_translation = #print_ast_translation ext}
+ | ext_components (ExtRules {parse_rules, print_rules}) = {
+ roots = [],
+ mfix = [],
+ extra_consts = [],
+ parse_ast_translation = [],
+ parse_rules = parse_rules,
+ parse_translation = [],
+ print_translation = [],
+ print_rules = print_rules,
+ print_ast_translation = []}
+ | ext_components (ExtRoots roots) = {
+ roots = roots,
+ mfix = [],
+ extra_consts = [],
+ parse_ast_translation = [],
+ parse_rules = [],
+ parse_translation = [],
+ print_translation = [],
+ print_rules = [],
+ print_ast_translation = []};
(* empty_xgram *)
--- a/src/Pure/Syntax/syntax.ML Tue Nov 30 10:55:43 1993 +0100
+++ b/src/Pure/Syntax/syntax.ML Tue Nov 30 11:04:07 1993 +0100
@@ -110,12 +110,12 @@
(* empty_tables *)
+(*(* FIXME *)
val empty_tables =
Tabs {
lexicon = empty_lexicon,
roots = [],
- (* gram = empty_gram, *) (* FIXME *)
- gram = mk_gram [] [], (* FIXME *)
+ gram = empty_gram,
consts = [],
parse_ast_trtab = Symtab.null,
parse_ruletab = Symtab.null,
@@ -123,6 +123,7 @@
print_trtab = Symtab.null,
print_ruletab = Symtab.null,
prtab = empty_prtab};
+*)
(* extend_tables *)
@@ -158,6 +159,7 @@
(* mk_tables *)
+(* FIXME *)
(* val mk_tables = extend_tables empty_tables; *)
(* FIXME *)
@@ -426,7 +428,7 @@
val type_syn = mk_syntax (ref (ExtGG (ref EmptyGG, type_ext)));
-(* extend *) (* FIXME *) (* FIXME check *)
+(* extend *) (* FIXME *)
fun old_extend syn read_ty (roots, xconsts, sext) =
let
--- a/src/Pure/sign.ML Tue Nov 30 10:55:43 1993 +0100
+++ b/src/Pure/sign.ML Tue Nov 30 11:04:07 1993 +0100
@@ -132,12 +132,6 @@
(*read and check the type mentioned in a const declaration; zero type var
indices because type inference requires it*)
- (* FIXME bug / feature: varifyT'ed TFrees may clash with user specified
- TVars e.g. foo :: "'a => ?'a" *)
- (* FIXME if user supplied TVars were disallowed, zero_tvar_indices would
- become obsolete *)
- (* FIXME disallow "" as const name *)
-
fun read_consts tsg sy (cs, s) =
let val ty = zero_tvar_indices (Type.varifyT (read_typ tsg sy s));
in
@@ -164,7 +158,6 @@
val const_decs' =
map (read_consts tsig' syn') (Syntax.constants sext @ const_decs);
- (* FIXME ^^^^ should be syn *)
in
Sg {
tsig = tsig',
@@ -191,7 +184,7 @@
(Syntax.syntax_types, 0)],
[(["fun"], ([["logic"], ["logic"]], "logic")),
(["prop"], ([], "logic"))],
- [([Syntax.constrainC], "'a::logic => 'a")], (* FIXME replace logic by {} (?) *)
+ [([Syntax.constrainC], "'a::logic => 'a")],
Some Syntax.pure_sext);