src/Pure/Syntax/syntax.ML
changeset 167 128e122acc89
parent 144 0a0da273a6c5
child 168 1bf4e2cab673
     1.1 --- a/src/Pure/Syntax/syntax.ML	Mon Nov 29 12:29:41 1993 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Nov 29 12:32:42 1993 +0100
     1.3 @@ -5,10 +5,8 @@
     1.4  Root of Isabelle's syntax module.
     1.5  
     1.6  TODO:
     1.7 -  extend_tables (requires extend_gram) (roots!)
     1.8 -  replace add_synrules by extend_tables
     1.9 -  extend, merge: make roots handling more robust
    1.10 -  extend: use extend_tables
    1.11 +  fix empty_tables, extend_tables, mk_tables (requires empty_gram, extend_gram)
    1.12 +  fix extend (requires extend_tables)
    1.13  *)
    1.14  
    1.15  signature SYNTAX =
    1.16 @@ -22,7 +20,7 @@
    1.17    type syntax
    1.18    val type_syn: syntax
    1.19    val extend: syntax -> (string -> typ) -> string list * string list * sext -> syntax
    1.20 -  val merge: syntax * syntax -> syntax
    1.21 +  val merge: string list -> syntax -> syntax -> syntax
    1.22    val print_gram: syntax -> unit
    1.23    val print_trans: syntax -> unit
    1.24    val print_syntax: syntax -> unit
    1.25 @@ -70,7 +68,7 @@
    1.26  
    1.27  datatype gramgraph =
    1.28    EmptyGG |
    1.29 -  ExtGG of gramgraph ref * (ext * synrules) |
    1.30 +  ExtGG of gramgraph ref * ext |
    1.31    MergeGG of gramgraph ref * gramgraph ref;
    1.32  
    1.33  datatype syntax = Syntax of gramgraph ref * tables;
    1.34 @@ -107,8 +105,62 @@
    1.35    mk_ruletab (flat (map #2 (Symtab.alist_of tab)) @ rules);
    1.36  
    1.37  
    1.38 +
    1.39 +(** tables **)
    1.40 +
    1.41 +(* empty_tables *)
    1.42 +
    1.43 +val empty_tables =
    1.44 +  Tabs {
    1.45 +    lexicon = empty_lexicon,
    1.46 +    roots = [],
    1.47 +    (* gram = empty_gram, *)    (* FIXME *)
    1.48 +    gram = mk_gram [] [],       (* FIXME *)
    1.49 +    consts = [],
    1.50 +    parse_ast_trtab = Symtab.null,
    1.51 +    parse_ruletab = Symtab.null,
    1.52 +    parse_trtab = Symtab.null,
    1.53 +    print_trtab = Symtab.null,
    1.54 +    print_ruletab = Symtab.null,
    1.55 +    prtab = empty_prtab};
    1.56 +
    1.57 +
    1.58 +(* extend_tables *)
    1.59 +
    1.60 +fun extend_tables (Tabs tabs) (XGram xgram) =
    1.61 +  let
    1.62 +    val {lexicon, roots = roots1, gram, consts = consts1, parse_ast_trtab,
    1.63 +      parse_ruletab, parse_trtab, print_trtab, print_ruletab, prtab} = tabs;
    1.64 +    val {roots = roots2, prods, consts = consts2, parse_ast_translation,
    1.65 +      parse_rules, parse_translation, print_translation, print_rules,
    1.66 +      print_ast_translation} = xgram;
    1.67 +  in
    1.68 +    (* FIXME *)
    1.69 +    if not (null prods) then
    1.70 +      error "extend_tables: called with non-empty prods"
    1.71 +    else
    1.72 +
    1.73 +    Tabs {
    1.74 +      lexicon = extend_lexicon lexicon (literals_of prods),
    1.75 +      roots = roots2 union roots1,
    1.76 +      (* gram = extend_gram gram roots2 prods, *)  (* FIXME *)
    1.77 +      gram = gram,                                 (* FIXME *)
    1.78 +      consts = consts2 union consts1,
    1.79 +      parse_ast_trtab =
    1.80 +        extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
    1.81 +      parse_ruletab = extend_ruletab parse_ruletab parse_rules,
    1.82 +      parse_trtab = extend_trtab parse_trtab parse_translation "parse translation",
    1.83 +      print_trtab = extend_trtab print_trtab print_translation "print translation",
    1.84 +      print_ruletab = extend_ruletab print_ruletab print_rules,
    1.85 +      prtab = extend_prtab prtab prods print_ast_translation}
    1.86 +  end;
    1.87 +
    1.88 +
    1.89  (* mk_tables *)
    1.90  
    1.91 +val mk_tables = extend_tables empty_tables;
    1.92 +
    1.93 +(* FIXME *)
    1.94  fun mk_tables (XGram xgram) =
    1.95    let
    1.96      val {roots, prods, consts, parse_ast_translation, parse_rules,
    1.97 @@ -129,25 +181,6 @@
    1.98    end;
    1.99  
   1.100  
   1.101 -(* add_synrules *)
   1.102 -
   1.103 -fun add_synrules (Tabs tabs) (SynRules rules) =
   1.104 -  let
   1.105 -    val {lexicon, roots, gram, consts, parse_ast_trtab, parse_ruletab,
   1.106 -      parse_trtab, print_trtab, print_ruletab, prtab} = tabs;
   1.107 -    val {parse_rules, print_rules} = rules;
   1.108 -  in
   1.109 -    Tabs {
   1.110 -      lexicon = lexicon, roots = roots, gram = gram, consts = consts,
   1.111 -      parse_ast_trtab = parse_ast_trtab,
   1.112 -      parse_ruletab = extend_ruletab parse_ruletab parse_rules,
   1.113 -      parse_trtab = parse_trtab,
   1.114 -      print_trtab = print_trtab,
   1.115 -      print_ruletab = extend_ruletab print_ruletab print_rules,
   1.116 -      prtab = prtab}
   1.117 -  end;
   1.118 -
   1.119 -
   1.120  (* ggr_to_xgram *)
   1.121  
   1.122  fun ggr_to_xgram ggr =
   1.123 @@ -168,9 +201,9 @@
   1.124    end;
   1.125  
   1.126  
   1.127 -(* make_syntax *)
   1.128 +(* mk_syntax *)
   1.129  
   1.130 -fun make_syntax ggr = Syntax (ggr, mk_tables (ggr_to_xgram ggr));
   1.131 +fun mk_syntax ggr = Syntax (ggr, mk_tables (ggr_to_xgram ggr));
   1.132  
   1.133  
   1.134  
   1.135 @@ -390,32 +423,59 @@
   1.136  
   1.137  (* type_syn *)
   1.138  
   1.139 -val type_syn = make_syntax (ref (ExtGG (ref EmptyGG, (type_ext, empty_synrules))));
   1.140 +val type_syn = mk_syntax (ref (ExtGG (ref EmptyGG, type_ext)));
   1.141 +
   1.142 +
   1.143 +(* extend *)  (* FIXME *)
   1.144 +
   1.145 +fun old_extend syn read_ty (roots, xconsts, sext) =
   1.146 +  let
   1.147 +    val Syntax (ggr0, Tabs {roots = roots0, ...}) = syn;
   1.148 +
   1.149 +    val ext1 = ext_of_sext ((distinct roots) \\ roots0) xconsts read_ty sext;
   1.150 +    val (syn1 as Syntax (ggr1, tabs1)) = mk_syntax (ref (ExtGG (ggr0, ext1)));
   1.151 +
   1.152 +    val (parse_rules, print_rules) = read_xrules syn1 (xrules_of sext);
   1.153 +    val ext2 = ExtRules {parse_rules = parse_rules, print_rules = print_rules};
   1.154 +  in
   1.155 +    Syntax (ref (ExtGG (ggr1, ext2)), extend_tables tabs1 (mk_xgram ext2))
   1.156 +  end;
   1.157  
   1.158  
   1.159 -(** extend **)
   1.160 -
   1.161 -fun extend (old_syn as Syntax (ggr, _)) read_ty (roots, xconsts, sext) =
   1.162 +fun new_extend syn read_ty (roots, xconsts, sext) =
   1.163    let
   1.164 -    val ext = ext_of_sext roots xconsts read_ty sext;
   1.165 +    val Syntax (ggr0, tabs0 as Tabs {roots = roots0, ...}) = syn;
   1.166  
   1.167 -    val (tmp_syn as Syntax (_, tmp_tabs)) =
   1.168 -      make_syntax (ref (ExtGG (ggr, (ext, empty_synrules))));
   1.169 +    val ext1 = ext_of_sext ((distinct roots) \\ roots0) xconsts read_ty sext;
   1.170 +    val (syn1 as Syntax (ggr1, tabs1)) =
   1.171 +      Syntax (ref (ExtGG (ggr0, ext1)), extend_tables tabs0 (mk_xgram ext1));
   1.172  
   1.173 -    val (parse_rules, print_rules) = read_xrules tmp_syn (xrules_of sext);
   1.174 -    val rules =
   1.175 -      SynRules {
   1.176 -        parse_rules = parse_rules,
   1.177 -        print_rules = print_rules};
   1.178 +    val (parse_rules, print_rules) = read_xrules syn1 (xrules_of sext);
   1.179 +    val ext2 = ExtRules {parse_rules = parse_rules, print_rules = print_rules};
   1.180    in
   1.181 -    Syntax (ref (ExtGG (ggr, (ext, rules))), add_synrules tmp_tabs rules)
   1.182 +    Syntax (ref (ExtGG (ggr1, ext2)), extend_tables tabs1 (mk_xgram ext2))
   1.183    end;
   1.184  
   1.185  
   1.186 +fun extend syn read_ty (ex as (_, _, sext)) =
   1.187 +  (case sext of
   1.188 +    Sext {mixfix = [], ...} => new_extend
   1.189 +  | NewSext {mixfix = [], ...} => new_extend
   1.190 +  | _ => old_extend) syn read_ty ex;
   1.191 +
   1.192 +
   1.193  (* merge *)
   1.194  
   1.195 -fun merge (Syntax (ggr1, _), Syntax (ggr2, _)) =
   1.196 -  make_syntax (ref (MergeGG (ggr1, ggr2)));
   1.197 +fun merge roots syn1 syn2 =
   1.198 +  let
   1.199 +    val Syntax (ggr1, Tabs {roots = roots1, ...}) = syn1;
   1.200 +    val Syntax (ggr2, Tabs {roots = roots2, ...}) = syn2;
   1.201 +    val mggr = ref (MergeGG (ggr1, ggr2));
   1.202 +  in
   1.203 +    (case ((distinct roots) \\ roots1) \\ roots2 of
   1.204 +      [] => mk_syntax mggr
   1.205 +    | new_roots => mk_syntax (ref (ExtGG (mggr, ExtRoots new_roots))))
   1.206 +  end;
   1.207  
   1.208  
   1.209  end;