1.1 --- a/src/Pure/Syntax/syntax.ML Mon May 31 19:36:13 2010 +0200
1.2 +++ b/src/Pure/Syntax/syntax.ML Mon May 31 21:06:57 2010 +0200
1.3 @@ -168,21 +168,21 @@
1.4 fun err_dup_trfun name c =
1.5 error ("More than one " ^ name ^ " for " ^ quote c);
1.6
1.7 -fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns;
1.8 +fun remove_trtab trfuns = fold (Symtab.remove Syn_Ext.eq_trfun) trfuns;
1.9
1.10 fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab)
1.11 handle Symtab.DUP c => err_dup_trfun name c;
1.12
1.13 -fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2)
1.14 +fun merge_trtabs name tab1 tab2 = Symtab.merge Syn_Ext.eq_trfun (tab1, tab2)
1.15 handle Symtab.DUP c => err_dup_trfun name c;
1.16
1.17
1.18 (* print (ast) translations *)
1.19
1.20 fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
1.21 -fun update_tr'tab trfuns = fold_rev (Symtab.update_list SynExt.eq_trfun) trfuns;
1.22 -fun remove_tr'tab trfuns = fold (Symtab.remove_list SynExt.eq_trfun) trfuns;
1.23 -fun merge_tr'tabs tab1 tab2 = Symtab.merge_list SynExt.eq_trfun (tab1, tab2);
1.24 +fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syn_Ext.eq_trfun) trfuns;
1.25 +fun remove_tr'tab trfuns = fold (Symtab.remove_list Syn_Ext.eq_trfun) trfuns;
1.26 +fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syn_Ext.eq_trfun (tab1, tab2);
1.27
1.28
1.29
1.30 @@ -239,7 +239,7 @@
1.31
1.32 datatype syntax =
1.33 Syntax of {
1.34 - input: SynExt.xprod list,
1.35 + input: Syn_Ext.xprod list,
1.36 lexicon: Scan.lexicon,
1.37 gram: Parser.gram,
1.38 consts: string list,
1.39 @@ -287,7 +287,7 @@
1.40 val {input, lexicon, gram, consts = consts1, prmodes = prmodes1,
1.41 parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
1.42 print_ast_trtab, tokentrtab, prtabs} = tabs;
1.43 - val SynExt.SynExt {xprods, consts = consts2, prmodes = prmodes2,
1.44 + val Syn_Ext.Syn_Ext {xprods, consts = consts2, prmodes = prmodes2,
1.45 parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
1.46 print_ast_translation, token_translation} = syn_ext;
1.47 val new_xprods =
1.48 @@ -296,7 +296,7 @@
1.49 in
1.50 Syntax
1.51 ({input = new_xprods @ input,
1.52 - lexicon = fold Scan.extend_lexicon (SynExt.delims_of new_xprods) lexicon,
1.53 + lexicon = fold Scan.extend_lexicon (Syn_Ext.delims_of new_xprods) lexicon,
1.54 gram = Parser.extend_gram gram new_xprods,
1.55 consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
1.56 prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
1.57 @@ -316,7 +316,7 @@
1.58
1.59 fun remove_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
1.60 let
1.61 - val SynExt.SynExt {xprods, consts = _, prmodes = _,
1.62 + val Syn_Ext.Syn_Ext {xprods, consts = _, prmodes = _,
1.63 parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
1.64 print_ast_translation, token_translation = _} = syn_ext;
1.65 val {input, lexicon, gram, consts, prmodes,
1.66 @@ -328,7 +328,7 @@
1.67 in
1.68 Syntax
1.69 ({input = input',
1.70 - lexicon = if changed then Scan.make_lexicon (SynExt.delims_of input') else lexicon,
1.71 + lexicon = if changed then Scan.make_lexicon (Syn_Ext.delims_of input') else lexicon,
1.72 gram = if changed then Parser.make_gram input' else gram,
1.73 consts = consts,
1.74 prmodes = prmodes,
1.75 @@ -381,13 +381,13 @@
1.76
1.77 val basic_syntax =
1.78 empty_syntax
1.79 - |> update_syntax mode_default TypeExt.type_ext
1.80 - |> update_syntax mode_default SynExt.pure_ext;
1.81 + |> update_syntax mode_default Type_Ext.type_ext
1.82 + |> update_syntax mode_default Syn_Ext.pure_ext;
1.83
1.84 val basic_nonterms =
1.85 - (Lexicon.terminals @ [SynExt.logic, "type", "types", "sort", "classes",
1.86 - SynExt.args, SynExt.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
1.87 - "asms", SynExt.any, SynExt.sprop, "num_const", "float_const",
1.88 + (Lexicon.terminals @ [Syn_Ext.logic, "type", "types", "sort", "classes",
1.89 + Syn_Ext.args, Syn_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
1.90 + "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const",
1.91 "index", "struct"]);
1.92
1.93
1.94 @@ -481,13 +481,13 @@
1.95 val toks = Lexicon.tokenize lexicon xids syms;
1.96 val _ = List.app Lexicon.report_token toks;
1.97
1.98 - val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
1.99 + val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
1.100 val pts = Parser.parse gram root' (filter Lexicon.is_proper toks);
1.101 val len = length pts;
1.102
1.103 val limit = ! ambiguity_limit;
1.104 fun show_pt pt =
1.105 - Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts ctxt (K NONE) [pt])));
1.106 + Pretty.string_of (Ast.pretty_ast (hd (Syn_Trans.pts_to_asts ctxt (K NONE) [pt])));
1.107 in
1.108 if len <= ! ambiguity_level then ()
1.109 else if ! ambiguity_is_error then error (ambiguity_msg pos)
1.110 @@ -497,7 +497,7 @@
1.111 "\nproduces " ^ string_of_int len ^ " parse trees" ^
1.112 (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
1.113 map show_pt (take limit pts))));
1.114 - SynTrans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
1.115 + Syn_Trans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
1.116 end;
1.117
1.118
1.119 @@ -506,9 +506,9 @@
1.120 fun read ctxt is_logtype (syn as Syntax (tabs, _)) ty inp =
1.121 let
1.122 val {parse_ruletab, parse_trtab, ...} = tabs;
1.123 - val asts = read_asts ctxt is_logtype syn false (SynExt.typ_to_nonterm ty) inp;
1.124 + val asts = read_asts ctxt is_logtype syn false (Syn_Ext.typ_to_nonterm ty) inp;
1.125 in
1.126 - SynTrans.asts_to_terms ctxt (lookup_tr parse_trtab)
1.127 + Syn_Trans.asts_to_terms ctxt (lookup_tr parse_trtab)
1.128 (map (Ast.normalize_ast (Symtab.lookup_list parse_ruletab)) asts)
1.129 end;
1.130
1.131 @@ -547,23 +547,23 @@
1.132
1.133 fun standard_parse_term pp check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
1.134 read ctxt is_logtype syn ty (syms, pos)
1.135 - |> map (TypeExt.decode_term get_sort map_const map_free)
1.136 + |> map (Type_Ext.decode_term get_sort map_const map_free)
1.137 |> disambig (Printer.pp_show_brackets pp) check;
1.138
1.139
1.140 (* read types *)
1.141
1.142 fun standard_parse_typ ctxt syn get_sort (syms, pos) =
1.143 - (case read ctxt (K false) syn SynExt.typeT (syms, pos) of
1.144 - [t] => TypeExt.typ_of_term (get_sort (TypeExt.term_sorts t)) t
1.145 + (case read ctxt (K false) syn Syn_Ext.typeT (syms, pos) of
1.146 + [t] => Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t
1.147 | _ => error (ambiguity_msg pos));
1.148
1.149
1.150 (* read sorts *)
1.151
1.152 fun standard_parse_sort ctxt syn (syms, pos) =
1.153 - (case read ctxt (K false) syn TypeExt.sortT (syms, pos) of
1.154 - [t] => TypeExt.sort_of_term t
1.155 + (case read ctxt (K false) syn Type_Ext.sortT (syms, pos) of
1.156 + [t] => Type_Ext.sort_of_term t
1.157 | _ => error (ambiguity_msg pos));
1.158
1.159
1.160 @@ -666,9 +666,9 @@
1.161
1.162 fun ext_syntax f decls = update_syntax mode_default (f decls);
1.163
1.164 -val update_trfuns = ext_syntax SynExt.syn_ext_trfuns;
1.165 -val update_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns;
1.166 -val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns;
1.167 +val update_trfuns = ext_syntax Syn_Ext.syn_ext_trfuns;
1.168 +val update_advanced_trfuns = ext_syntax Syn_Ext.syn_ext_advanced_trfuns;
1.169 +val extend_tokentrfuns = ext_syntax Syn_Ext.syn_ext_tokentrfuns;
1.170
1.171 fun update_type_gram add prmode decls =
1.172 (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
1.173 @@ -677,13 +677,13 @@
1.174 (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
1.175
1.176 fun update_trrules ctxt is_logtype syn =
1.177 - ext_syntax SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
1.178 + ext_syntax Syn_Ext.syn_ext_rules o read_rules ctxt is_logtype syn;
1.179
1.180 fun remove_trrules ctxt is_logtype syn =
1.181 - remove_syntax mode_default o SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
1.182 + remove_syntax mode_default o Syn_Ext.syn_ext_rules o read_rules ctxt is_logtype syn;
1.183
1.184 -val update_trrules_i = ext_syntax SynExt.syn_ext_rules o cert_rules;
1.185 -val remove_trrules_i = remove_syntax mode_default o SynExt.syn_ext_rules o cert_rules;
1.186 +val update_trrules_i = ext_syntax Syn_Ext.syn_ext_rules o cert_rules;
1.187 +val remove_trrules_i = remove_syntax mode_default o Syn_Ext.syn_ext_rules o cert_rules;
1.188
1.189
1.190
1.191 @@ -798,7 +798,7 @@
1.192
1.193 val check_typs = gen_check fst false;
1.194 val check_terms = gen_check snd false;
1.195 -fun check_props ctxt = map (TypeExt.type_constraint propT) #> check_terms ctxt;
1.196 +fun check_props ctxt = map (Type_Ext.type_constraint propT) #> check_terms ctxt;
1.197
1.198 val check_typ = singleton o check_typs;
1.199 val check_term = singleton o check_terms;
1.200 @@ -905,7 +905,7 @@
1.201
1.202
1.203 (*export parts of internal Syntax structures*)
1.204 -open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
1.205 +open Lexicon Syn_Ext Ast Parser Type_Ext Syn_Trans Mixfix Printer;
1.206
1.207 end;
1.208
1.209 @@ -913,9 +913,9 @@
1.210 open Basic_Syntax;
1.211
1.212 forget_structure "Ast";
1.213 -forget_structure "SynExt";
1.214 +forget_structure "Syn_Ext";
1.215 forget_structure "Parser";
1.216 -forget_structure "TypeExt";
1.217 -forget_structure "SynTrans";
1.218 +forget_structure "Type_Ext";
1.219 +forget_structure "Syn_Trans";
1.220 forget_structure "Mixfix";
1.221 forget_structure "Printer";