removed separate logtypes field of syntax; removed test_read, simple_str_of_sort, simple_string_of_typ; provide default_mode;
authorwenzelm
Wed Jun 09 18:54:43 2004 +0200 (2004-06-09)
changeset 149047d8dc92fcb7f
parent 14903 d264b8ad3eec
child 14905 5f3fc2f62071
removed separate logtypes field of syntax; removed test_read, simple_str_of_sort, simple_string_of_typ; provide default_mode;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Wed Jun 09 18:54:26 2004 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Wed Jun 09 18:54:43 2004 +0200
     1.3 @@ -38,35 +38,35 @@
     1.4      ParsePrintRule of 'a * 'a
     1.5    type syntax
     1.6    val is_keyword: syntax -> string -> bool
     1.7 -  val extend_log_types: string list -> syntax -> syntax
     1.8    val extend_type_gram: (string * int * mixfix) list -> syntax -> syntax
     1.9 -  val extend_const_gram: string * bool -> (string * typ * mixfix) list -> syntax -> syntax
    1.10 +  val extend_const_gram: (string -> bool) ->
    1.11 +    string * bool -> (string * typ * mixfix) list -> syntax -> syntax
    1.12    val extend_consts: string list -> syntax -> syntax
    1.13    val extend_trfuns:
    1.14      (string * (ast list -> ast)) list *
    1.15      (string * (term list -> term)) list *
    1.16      (string * (bool -> typ -> term list -> term)) list *
    1.17      (string * (ast list -> ast)) list -> syntax -> syntax
    1.18 -  val extend_tokentrfuns: (string * string * (string -> string * real)) list -> syntax -> syntax
    1.19 -  val extend_trrules: syntax -> (string * string) trrule list -> syntax -> syntax
    1.20 +  val extend_tokentrfuns:
    1.21 +    (string * string * (string -> string * real)) list -> syntax -> syntax
    1.22    val extend_trrules_i: ast trrule list -> syntax -> syntax
    1.23 +  val extend_trrules: (string -> bool) -> syntax ->
    1.24 +    (string * string) trrule list -> syntax -> syntax
    1.25    val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
    1.26 +  val default_mode: string * bool
    1.27    val merge_syntaxes: syntax -> syntax -> syntax
    1.28    val type_syn: syntax
    1.29    val pure_syn: syntax
    1.30    val print_gram: syntax -> unit
    1.31    val print_trans: syntax -> unit
    1.32    val print_syntax: syntax -> unit
    1.33 -  val test_read: syntax -> string -> string -> unit
    1.34 -  val read: syntax -> typ -> string -> term list
    1.35 +  val read: (string -> bool) -> syntax -> typ -> string -> term list
    1.36    val read_typ: syntax -> ((indexname * sort) list -> indexname -> sort) -> (sort -> sort) ->
    1.37      string -> typ
    1.38    val read_sort: syntax -> string -> sort
    1.39    val pretty_term: syntax -> bool -> term -> Pretty.T
    1.40    val pretty_typ: syntax -> typ -> Pretty.T
    1.41    val pretty_sort: syntax -> sort -> Pretty.T
    1.42 -  val simple_str_of_sort: sort -> string
    1.43 -  val simple_string_of_typ: typ -> string
    1.44    val simple_pprint_typ: typ -> pprint_args -> unit
    1.45    val ambiguity_level: int ref
    1.46    val ambiguity_is_error: bool ref
    1.47 @@ -166,7 +166,6 @@
    1.48  datatype syntax =
    1.49    Syntax of {
    1.50      lexicon: Scan.lexicon,
    1.51 -    logtypes: string list,
    1.52      gram: Parser.gram,
    1.53      consts: string list,
    1.54      prmodes: string list,
    1.55 @@ -187,7 +186,6 @@
    1.56  val empty_syntax =
    1.57    Syntax {
    1.58      lexicon = Scan.empty_lexicon,
    1.59 -    logtypes = [],
    1.60      gram = Parser.empty_gram,
    1.61      consts = [],
    1.62      prmodes = [],
    1.63 @@ -203,18 +201,17 @@
    1.64  
    1.65  (* extend_syntax *)
    1.66  
    1.67 -fun extend_syntax (mode, inout) (Syntax tabs) syn_ext =
    1.68 +fun extend_syntax (mode, inout) syn_ext (Syntax tabs) =
    1.69    let
    1.70 -    val {lexicon, logtypes = logtypes1, gram, consts = consts1, prmodes = prmodes1,
    1.71 +    val {lexicon, gram, consts = consts1, prmodes = prmodes1,
    1.72        parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
    1.73        print_ast_trtab, tokentrtab, prtabs} = tabs;
    1.74 -    val SynExt.SynExt {logtypes = logtypes2, xprods, consts = consts2, prmodes = prmodes2,
    1.75 +    val SynExt.SynExt {xprods, consts = consts2, prmodes = prmodes2,
    1.76        parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
    1.77        print_ast_translation, token_translation} = syn_ext;
    1.78    in
    1.79      Syntax {
    1.80        lexicon = if inout then Scan.extend_lexicon lexicon (SynExt.delims_of xprods) else lexicon,
    1.81 -      logtypes = merge_lists logtypes1 logtypes2,
    1.82        gram = if inout then Parser.extend_gram gram xprods else gram,
    1.83        consts = consts2 @ consts1,
    1.84        prmodes = (mode ins_string prmodes2) union_string prmodes1,
    1.85 @@ -229,26 +226,27 @@
    1.86        prtabs = Printer.extend_prtabs prtabs mode xprods}
    1.87    end;
    1.88  
    1.89 +val default_mode = ("", true);
    1.90 +
    1.91  
    1.92  (* merge_syntaxes *)
    1.93  
    1.94  fun merge_syntaxes (Syntax tabs1) (Syntax tabs2) =
    1.95    let
    1.96 -    val {lexicon = lexicon1, logtypes = logtypes1, gram = gram1, consts = consts1,
    1.97 -      prmodes = prmodes1, parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1,
    1.98 +    val {lexicon = lexicon1, gram = gram1, consts = consts1, prmodes = prmodes1,
    1.99 +      parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1,
   1.100        parse_trtab = parse_trtab1, print_trtab = print_trtab1,
   1.101        print_ruletab = print_ruletab1, print_ast_trtab = print_ast_trtab1,
   1.102        tokentrtab = tokentrtab1, prtabs = prtabs1} = tabs1;
   1.103  
   1.104 -    val {lexicon = lexicon2, logtypes = logtypes2, gram = gram2, consts = consts2,
   1.105 -      prmodes = prmodes2, parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
   1.106 +    val {lexicon = lexicon2, gram = gram2, consts = consts2, prmodes = prmodes2,
   1.107 +      parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
   1.108        parse_trtab = parse_trtab2, print_trtab = print_trtab2,
   1.109        print_ruletab = print_ruletab2, print_ast_trtab = print_ast_trtab2,
   1.110        tokentrtab = tokentrtab2, prtabs = prtabs2} = tabs2;
   1.111    in
   1.112      Syntax {
   1.113        lexicon = Scan.merge_lexicons lexicon1 lexicon2,
   1.114 -      logtypes = merge_lists logtypes1 logtypes2,
   1.115        gram = Parser.merge_grams gram1 gram2,
   1.116        consts = unique_strings (sort_strings (consts1 @ consts2)),
   1.117        prmodes = merge_lists prmodes1 prmodes2,
   1.118 @@ -266,8 +264,8 @@
   1.119  
   1.120  (* type_syn *)
   1.121  
   1.122 -val type_syn = extend_syntax ("", true) empty_syntax TypeExt.type_ext;
   1.123 -val pure_syn = extend_syntax ("", true) type_syn SynExt.pure_ext;
   1.124 +val type_syn = empty_syntax |> extend_syntax default_mode TypeExt.type_ext;
   1.125 +val pure_syn = type_syn |> extend_syntax default_mode SynExt.pure_ext;
   1.126  
   1.127  
   1.128  
   1.129 @@ -281,11 +279,10 @@
   1.130  
   1.131  fun print_gram (Syntax tabs) =
   1.132    let
   1.133 -    val {lexicon, logtypes, prmodes, gram, prtabs, ...} = tabs;
   1.134 +    val {lexicon, prmodes, gram, prtabs, ...} = tabs;
   1.135      val prmodes' = sort_strings (filter_out (equal "") prmodes);
   1.136    in
   1.137      [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon),
   1.138 -      Pretty.strs ("logtypes:" :: logtypes),
   1.139        Pretty.big_list "prods:" (Parser.pretty_gram gram),
   1.140        pretty_strs_qs "print modes:" prmodes']
   1.141      |> Pretty.chunks |> Pretty.writeln
   1.142 @@ -327,34 +324,14 @@
   1.143  
   1.144  (** read **)
   1.145  
   1.146 -(* test_read *)
   1.147 -
   1.148 -fun test_read (Syntax tabs) root str =
   1.149 -  let
   1.150 -    val {lexicon, gram, parse_ast_trtab, parse_ruletab, ...} = tabs;
   1.151 -
   1.152 -    val chars = Symbol.explode str;
   1.153 -    val toks = Lexicon.tokenize lexicon false chars;
   1.154 -    val _ = writeln ("tokens: " ^ space_implode " " (map Lexicon.display_token toks));
   1.155 -
   1.156 -    fun show_pt pt =
   1.157 -      let
   1.158 -        val [raw_ast] = SynTrans.pts_to_asts (K None) [pt];
   1.159 -        val _ = writeln ("raw: " ^ Ast.str_of_ast raw_ast);
   1.160 -        val [pre_ast] = SynTrans.pts_to_asts (lookup_tr parse_ast_trtab) [pt];
   1.161 -        val _ = Ast.normalize true true (lookup_ruletab parse_ruletab) pre_ast;
   1.162 -      in () end;
   1.163 -  in seq show_pt (Parser.parse gram root toks) end;
   1.164 -
   1.165 -
   1.166  (* read_ast *)
   1.167  
   1.168  val ambiguity_level = ref 1;
   1.169  
   1.170 -fun read_asts (Syntax tabs) xids root str =
   1.171 +fun read_asts is_logtype (Syntax tabs) xids root str =
   1.172    let
   1.173 -    val {lexicon, gram, parse_ast_trtab, logtypes, ...} = tabs;
   1.174 -    val root' = if root mem logtypes then SynExt.logic else root;
   1.175 +    val {lexicon, gram, parse_ast_trtab, ...} = tabs;
   1.176 +    val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
   1.177      val chars = Symbol.explode str;
   1.178      val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
   1.179  
   1.180 @@ -375,10 +352,10 @@
   1.181  
   1.182  (* read *)
   1.183  
   1.184 -fun read (syn as Syntax tabs) ty str =
   1.185 +fun read is_logtype (syn as Syntax tabs) ty str =
   1.186    let
   1.187      val {parse_ruletab, parse_trtab, ...} = tabs;
   1.188 -    val asts = read_asts syn false (SynExt.typ_to_nonterm ty) str;
   1.189 +    val asts = read_asts is_logtype syn false (SynExt.typ_to_nonterm ty) str;
   1.190    in
   1.191      SynTrans.asts_to_terms (lookup_tr parse_trtab)
   1.192        (map (Ast.normalize_ast (lookup_ruletab parse_ruletab)) asts)
   1.193 @@ -388,7 +365,7 @@
   1.194  (* read types *)
   1.195  
   1.196  fun read_typ syn get_sort map_sort str =
   1.197 -  (case read syn SynExt.typeT str of
   1.198 +  (case read (K false) syn SynExt.typeT str of
   1.199      [t] => TypeExt.typ_of_term (get_sort (TypeExt.raw_term_sorts t)) map_sort t
   1.200    | _ => error "read_typ: ambiguous syntax");
   1.201  
   1.202 @@ -396,7 +373,7 @@
   1.203  (* read sorts *)
   1.204  
   1.205  fun read_sort syn str =
   1.206 -  (case read syn TypeExt.sortT str of
   1.207 +  (case read (K false) syn TypeExt.sortT str of
   1.208      [t] => TypeExt.sort_of_term t
   1.209    | _ => error "read_sort: ambiguous syntax");
   1.210  
   1.211 @@ -430,7 +407,7 @@
   1.212    | None => rule);
   1.213  
   1.214  
   1.215 -fun read_pattern syn (root, str) =
   1.216 +fun read_pattern is_logtype syn (root, str) =
   1.217    let
   1.218      val Syntax {consts, ...} = syn;
   1.219  
   1.220 @@ -440,7 +417,7 @@
   1.221            else ast
   1.222        | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
   1.223    in
   1.224 -    (case read_asts syn true root str of
   1.225 +    (case read_asts is_logtype syn true root str of
   1.226        [ast] => constify ast
   1.227      | _ => error ("Syntactically ambiguous input: " ^ quote str))
   1.228    end handle ERROR =>
   1.229 @@ -472,35 +449,25 @@
   1.230  fun pretty_typ syn = pretty_t Printer.typ_to_ast Printer.pretty_typ_ast syn false;
   1.231  fun pretty_sort syn = pretty_t Printer.sort_to_ast Printer.pretty_typ_ast syn false;
   1.232  
   1.233 -val simple_str_of_sort = Pretty.str_of o pretty_sort type_syn;
   1.234 -val simple_string_of_typ = Pretty.string_of o (pretty_typ type_syn);
   1.235  val simple_pprint_typ = Pretty.pprint o Pretty.quote o (pretty_typ type_syn);
   1.236  
   1.237  
   1.238  
   1.239 -(** extend syntax (external interfaces) **)
   1.240 -
   1.241 -fun ext_syntax mk_syn_ext prmode decls (syn as Syntax {logtypes, ...}) =
   1.242 -  extend_syntax prmode syn (mk_syn_ext logtypes decls);
   1.243 +(** extend syntax **)
   1.244  
   1.245 -
   1.246 -fun extend_log_types logtypes syn =
   1.247 -  extend_syntax ("", true) syn (SynExt.syn_ext_logtypes logtypes);
   1.248 -
   1.249 -val extend_type_gram = ext_syntax Mixfix.syn_ext_types ("", true);
   1.250 +fun ext_syntax' f is_logtype prmode decls = extend_syntax prmode (f is_logtype decls);
   1.251 +fun ext_syntax f = ext_syntax' (K f) (K false) default_mode;
   1.252  
   1.253 -fun extend_const_gram prmode = ext_syntax Mixfix.syn_ext_consts prmode;
   1.254 -
   1.255 -val extend_consts = ext_syntax SynExt.syn_ext_const_names ("", true);
   1.256 -
   1.257 -val extend_trfuns = ext_syntax SynExt.syn_ext_trfuns ("", true);
   1.258 +val extend_type_gram   = ext_syntax Mixfix.syn_ext_types;
   1.259 +val extend_const_gram  = ext_syntax' Mixfix.syn_ext_consts;
   1.260 +val extend_consts      = ext_syntax SynExt.syn_ext_const_names;
   1.261 +val extend_trfuns      = ext_syntax SynExt.syn_ext_trfuns;
   1.262 +val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns;
   1.263 +val extend_trrules_i   = ext_syntax SynExt.syn_ext_rules o prep_rules I;
   1.264  
   1.265 -val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns ("", true);
   1.266 -
   1.267 -fun extend_trrules syn rules =
   1.268 -  ext_syntax SynExt.syn_ext_rules ("", true) (prep_rules (read_pattern syn) rules);
   1.269 -
   1.270 -fun extend_trrules_i rules = ext_syntax SynExt.syn_ext_rules ("", true) (prep_rules I rules);
   1.271 +fun extend_trrules is_logtype syn rules =
   1.272 +  ext_syntax' (K SynExt.syn_ext_rules) (K false) default_mode
   1.273 +    (prep_rules (read_pattern is_logtype syn) rules);
   1.274  
   1.275  
   1.276