*** empty log message ***
authorwenzelm
Tue Nov 30 11:04:07 1993 +0100 (1993-11-30)
changeset 171ab0f93a291b5
parent 170 590c9d1e0d73
child 172 3224c46737ef
*** empty log message ***
src/Pure/Syntax/extension.ML
src/Pure/Syntax/syntax.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Syntax/extension.ML	Tue Nov 30 10:55:43 1993 +0100
     1.2 +++ b/src/Pure/Syntax/extension.ML	Tue Nov 30 11:04:07 1993 +0100
     1.3 @@ -3,10 +3,6 @@
     1.4      Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     1.5  
     1.6  External grammar definition (internal interface).
     1.7 -
     1.8 -TODO:
     1.9 -  ext = {roots, mfix, extra_consts} | {.._translation} | {.._rules} (?)
    1.10 -  extend_xgram: move '.. \\ roots1' to Syntax.extend_tables (no?)
    1.11  *)
    1.12  
    1.13  signature EXTENSION0 =
    1.14 @@ -83,21 +79,36 @@
    1.15  
    1.16  (* ext_components *)
    1.17  
    1.18 -fun ext_components (Ext ext) =
    1.19 -      {roots = #roots ext, mfix = #mfix ext, extra_consts = #extra_consts ext,
    1.20 +fun ext_components (Ext ext) = {
    1.21 +      roots = #roots ext,
    1.22 +      mfix = #mfix ext,
    1.23 +      extra_consts = #extra_consts ext,
    1.24        parse_ast_translation = #parse_ast_translation ext,
    1.25 +      parse_rules = [],
    1.26        parse_translation = #parse_translation ext,
    1.27        print_translation = #print_translation ext,
    1.28 -      print_ast_translation = #print_ast_translation ext,
    1.29 -      parse_rules = [], print_rules = []}
    1.30 -  | ext_components (ExtRules {parse_rules, print_rules}) =
    1.31 -      {parse_rules = parse_rules, print_rules = print_rules, roots = [], mfix = [],
    1.32 -      extra_consts = [], parse_ast_translation = [], parse_translation = [],
    1.33 -      print_translation = [], print_ast_translation = []}
    1.34 -  | ext_components (ExtRoots roots) =
    1.35 -      {roots = roots, mfix = [], extra_consts = [], parse_ast_translation = [],
    1.36 -      parse_rules = [], parse_translation = [], print_translation = [],
    1.37 -      print_rules = [], print_ast_translation = []};
    1.38 +      print_rules = [],
    1.39 +      print_ast_translation = #print_ast_translation ext}
    1.40 +  | ext_components (ExtRules {parse_rules, print_rules}) = {
    1.41 +      roots = [],
    1.42 +      mfix = [],
    1.43 +      extra_consts = [],
    1.44 +      parse_ast_translation = [],
    1.45 +      parse_rules = parse_rules,
    1.46 +      parse_translation = [],
    1.47 +      print_translation = [],
    1.48 +      print_rules = print_rules,
    1.49 +      print_ast_translation = []}
    1.50 +  | ext_components (ExtRoots roots) = {
    1.51 +      roots = roots,
    1.52 +      mfix = [],
    1.53 +      extra_consts = [],
    1.54 +      parse_ast_translation = [],
    1.55 +      parse_rules = [],
    1.56 +      parse_translation = [],
    1.57 +      print_translation = [],
    1.58 +      print_rules = [],
    1.59 +      print_ast_translation = []};
    1.60  
    1.61  
    1.62  (* empty_xgram *)
     2.1 --- a/src/Pure/Syntax/syntax.ML	Tue Nov 30 10:55:43 1993 +0100
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Nov 30 11:04:07 1993 +0100
     2.3 @@ -110,12 +110,12 @@
     2.4  
     2.5  (* empty_tables *)
     2.6  
     2.7 +(*(* FIXME *)
     2.8  val empty_tables =
     2.9    Tabs {
    2.10      lexicon = empty_lexicon,
    2.11      roots = [],
    2.12 -    (* gram = empty_gram, *)    (* FIXME *)
    2.13 -    gram = mk_gram [] [],       (* FIXME *)
    2.14 +    gram = empty_gram,
    2.15      consts = [],
    2.16      parse_ast_trtab = Symtab.null,
    2.17      parse_ruletab = Symtab.null,
    2.18 @@ -123,6 +123,7 @@
    2.19      print_trtab = Symtab.null,
    2.20      print_ruletab = Symtab.null,
    2.21      prtab = empty_prtab};
    2.22 +*)
    2.23  
    2.24  
    2.25  (* extend_tables *)
    2.26 @@ -158,6 +159,7 @@
    2.27  
    2.28  (* mk_tables *)
    2.29  
    2.30 +(* FIXME *)
    2.31  (* val mk_tables = extend_tables empty_tables; *)
    2.32  
    2.33  (* FIXME *)
    2.34 @@ -426,7 +428,7 @@
    2.35  val type_syn = mk_syntax (ref (ExtGG (ref EmptyGG, type_ext)));
    2.36  
    2.37  
    2.38 -(* extend *)  (* FIXME *) (* FIXME check *)
    2.39 +(* extend *)  (* FIXME *)
    2.40  
    2.41  fun old_extend syn read_ty (roots, xconsts, sext) =
    2.42    let
     3.1 --- a/src/Pure/sign.ML	Tue Nov 30 10:55:43 1993 +0100
     3.2 +++ b/src/Pure/sign.ML	Tue Nov 30 11:04:07 1993 +0100
     3.3 @@ -132,12 +132,6 @@
     3.4      (*read and check the type mentioned in a const declaration; zero type var
     3.5        indices because type inference requires it*)
     3.6  
     3.7 -    (* FIXME bug / feature: varifyT'ed TFrees may clash with user specified
     3.8 -      TVars e.g. foo :: "'a => ?'a" *)
     3.9 -    (* FIXME if user supplied TVars were disallowed, zero_tvar_indices would
    3.10 -      become obsolete *)
    3.11 -    (* FIXME disallow "" as const name *)
    3.12 -
    3.13      fun read_consts tsg sy (cs, s) =
    3.14        let val ty = zero_tvar_indices (Type.varifyT (read_typ tsg sy s));
    3.15        in
    3.16 @@ -164,7 +158,6 @@
    3.17  
    3.18      val const_decs' =
    3.19        map (read_consts tsig' syn') (Syntax.constants sext @ const_decs);
    3.20 -                    (* FIXME ^^^^ should be syn *)
    3.21    in
    3.22      Sg {
    3.23        tsig = tsig',
    3.24 @@ -191,7 +184,7 @@
    3.25    (Syntax.syntax_types, 0)],
    3.26   [(["fun"],  ([["logic"], ["logic"]], "logic")),
    3.27    (["prop"], ([], "logic"))],
    3.28 - [([Syntax.constrainC], "'a::logic => 'a")],  (* FIXME replace logic by {} (?) *)
    3.29 + [([Syntax.constrainC], "'a::logic => 'a")],
    3.30   Some Syntax.pure_sext);
    3.31  
    3.32