src/Pure/Syntax/syntax.ML
changeset 25394 db25c98f32e1
parent 25387 d9ab1e3a8acb
child 25476 03da46cfab9e
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sun Nov 11 14:00:12 2007 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Nov 11 14:00:13 2007 +0100
     1.3 @@ -23,14 +23,6 @@
     1.4    include SYN_TRANS1
     1.5    include MIXFIX1
     1.6    include PRINTER0
     1.7 -  val extend_trtab: string -> (string * ('a * stamp)) list ->
     1.8 -    ('a * stamp) Symtab.table -> ('a * stamp) Symtab.table
     1.9 -  val merge_trtabs: string -> ('a * stamp) Symtab.table -> ('a * stamp) Symtab.table ->
    1.10 -    ('a * stamp) Symtab.table
    1.11 -  val merge_tr'tabs: ('a * stamp) list Symtab.table -> ('a * stamp) list Symtab.table
    1.12 -    -> ('a * stamp) list Symtab.table
    1.13 -  val extend_tr'tab: (string * ('a * stamp)) list ->
    1.14 -    ('a * stamp) list Symtab.table -> ('a * stamp) list Symtab.table
    1.15    datatype 'a trrule =
    1.16      ParseRule of 'a * 'a |
    1.17      PrintRule of 'a * 'a |
    1.18 @@ -41,30 +33,28 @@
    1.19    type mode
    1.20    val mode_default: mode
    1.21    val mode_input: mode
    1.22 -  val extend_type_gram: (string * int * mixfix) list -> syntax -> syntax
    1.23 -  val extend_consts: string list -> syntax -> syntax
    1.24 -  val extend_trfuns:
    1.25 +  val update_type_gram: (string * int * mixfix) list -> syntax -> syntax
    1.26 +  val update_consts: string list -> syntax -> syntax
    1.27 +  val update_trfuns:
    1.28      (string * ((ast list -> ast) * stamp)) list *
    1.29      (string * ((term list -> term) * stamp)) list *
    1.30      (string * ((bool -> typ -> term list -> term) * stamp)) list *
    1.31      (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax
    1.32 -  val extend_advanced_trfuns:
    1.33 +  val update_advanced_trfuns:
    1.34      (string * ((Proof.context -> ast list -> ast) * stamp)) list *
    1.35      (string * ((Proof.context -> term list -> term) * stamp)) list *
    1.36      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
    1.37      (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
    1.38    val extend_tokentrfuns: (string * string * (string -> output * int)) list -> syntax -> syntax
    1.39 -  val extend_const_gram: (string -> bool) ->
    1.40 +  val update_const_gram: (string -> bool) ->
    1.41      mode -> (string * typ * mixfix) list -> syntax -> syntax
    1.42    val remove_const_gram: (string -> bool) ->
    1.43      mode -> (string * typ * mixfix) list -> syntax -> syntax
    1.44 -  val update_const_gram: (string -> bool) ->
    1.45 -    mode -> (string * typ * mixfix) list -> syntax -> syntax
    1.46 -  val extend_trrules: Proof.context -> (string -> bool) -> syntax ->
    1.47 +  val update_trrules: Proof.context -> (string -> bool) -> syntax ->
    1.48      (string * string) trrule list -> syntax -> syntax
    1.49    val remove_trrules: Proof.context -> (string -> bool) -> syntax ->
    1.50      (string * string) trrule list -> syntax -> syntax
    1.51 -  val extend_trrules_i: ast trrule list -> syntax -> syntax
    1.52 +  val update_trrules_i: ast trrule list -> syntax -> syntax
    1.53    val remove_trrules_i: ast trrule list -> syntax -> syntax
    1.54    val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
    1.55    val merge_syntaxes: syntax -> syntax -> syntax
    1.56 @@ -79,10 +69,11 @@
    1.57      (string -> string option) -> (string -> string option) ->
    1.58      (typ -> typ) -> (sort -> sort) -> Proof.context ->
    1.59      (string -> bool) -> syntax -> typ -> string -> term
    1.60 -  val standard_parse_typ: Proof.context -> syntax -> ((indexname * sort) list -> indexname -> sort) ->
    1.61 -    (sort -> sort) -> string -> typ
    1.62 +  val standard_parse_typ: Proof.context -> syntax ->
    1.63 +    ((indexname * sort) list -> indexname -> sort) -> (sort -> sort) -> string -> typ
    1.64    val standard_parse_sort: Proof.context -> syntax -> (sort -> sort) -> string -> sort
    1.65 -  val standard_unparse_term: (string -> xstring) -> Proof.context -> syntax -> bool -> term -> Pretty.T
    1.66 +  val standard_unparse_term: (string -> xstring) ->
    1.67 +    Proof.context -> syntax -> bool -> term -> Pretty.T
    1.68    val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
    1.69    val standard_unparse_sort: Proof.context -> syntax -> sort -> Pretty.T
    1.70    val ambiguity_level: int ref
    1.71 @@ -166,7 +157,7 @@
    1.72  
    1.73  fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns;
    1.74  
    1.75 -fun extend_trtab name trfuns tab = Symtab.extend (remove_trtab trfuns tab, trfuns)
    1.76 +fun update_trtab name trfuns tab = Symtab.extend (remove_trtab trfuns tab, trfuns)
    1.77    handle Symtab.DUP c => err_dup_trfun name c;
    1.78  
    1.79  fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2)
    1.80 @@ -176,7 +167,7 @@
    1.81  (* print (ast) translations *)
    1.82  
    1.83  fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
    1.84 -fun extend_tr'tab trfuns = fold_rev Symtab.update_list trfuns;
    1.85 +fun update_tr'tab trfuns = fold_rev (Symtab.update_list SynExt.eq_trfun) trfuns;
    1.86  fun remove_tr'tab trfuns = fold (Symtab.remove_list SynExt.eq_trfun) trfuns;
    1.87  fun merge_tr'tabs tab1 tab2 = Symtab.merge_list SynExt.eq_trfun (tab1, tab2);
    1.88  
    1.89 @@ -223,9 +214,9 @@
    1.90  fun dest_ruletab tab = maps snd (Symtab.dest tab);
    1.91  
    1.92  
    1.93 -(* empty, extend, merge ruletabs *)
    1.94 +(* empty, update, merge ruletabs *)
    1.95  
    1.96 -val extend_ruletab = fold_rev (fn r => Symtab.update_list (Ast.head_of_rule r, r));
    1.97 +val update_ruletab = fold_rev (fn r => Symtab.update_list (op =) (Ast.head_of_rule r, r));
    1.98  val remove_ruletab = fold (fn r => Symtab.remove_list (op =) (Ast.head_of_rule r, r));
    1.99  fun merge_ruletabs tab1 tab2 = Symtab.merge_list (op =) (tab1, tab2);
   1.100  
   1.101 @@ -276,9 +267,9 @@
   1.102      prtabs = Printer.empty_prtabs}, stamp ());
   1.103  
   1.104  
   1.105 -(* extend_syntax *)
   1.106 +(* update_syntax *)
   1.107  
   1.108 -fun extend_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
   1.109 +fun update_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
   1.110    let
   1.111      val {input, lexicon, gram, consts = consts1, prmodes = prmodes1,
   1.112        parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
   1.113 @@ -286,23 +277,25 @@
   1.114      val SynExt.SynExt {xprods, consts = consts2, prmodes = prmodes2,
   1.115        parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
   1.116        print_ast_translation, token_translation} = syn_ext;
   1.117 +    val input' = if inout then fold (insert (op =)) xprods input else input;
   1.118 +    val changed = length input <> length input';
   1.119      fun if_inout xs = if inout then xs else [];
   1.120    in
   1.121      Syntax
   1.122 -    ({input = if_inout xprods @ input,
   1.123 -      lexicon = Scan.extend_lexicon (if_inout (SynExt.delims_of xprods)) lexicon,
   1.124 -      gram = Parser.extend_gram gram (if_inout xprods),
   1.125 +    ({input = input',
   1.126 +      lexicon = if changed then Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon,
   1.127 +      gram = if changed then Parser.extend_gram gram xprods else gram,
   1.128        consts = Library.merge (op =) (consts1, filter_out NameSpace.is_qualified consts2),
   1.129        prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
   1.130        parse_ast_trtab =
   1.131 -        extend_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,
   1.132 -      parse_ruletab = extend_ruletab (if_inout parse_rules) parse_ruletab,
   1.133 -      parse_trtab = extend_trtab "parse translation" (if_inout parse_translation) parse_trtab,
   1.134 -      print_trtab = extend_tr'tab print_translation print_trtab,
   1.135 -      print_ruletab = extend_ruletab print_rules print_ruletab,
   1.136 -      print_ast_trtab = extend_tr'tab print_ast_translation print_ast_trtab,
   1.137 +        update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,
   1.138 +      parse_ruletab = update_ruletab (if_inout parse_rules) parse_ruletab,
   1.139 +      parse_trtab = update_trtab "parse translation" (if_inout parse_translation) parse_trtab,
   1.140 +      print_trtab = update_tr'tab print_translation print_trtab,
   1.141 +      print_ruletab = update_ruletab print_rules print_ruletab,
   1.142 +      print_ast_trtab = update_tr'tab print_ast_translation print_ast_trtab,
   1.143        tokentrtab = extend_tokentrtab token_translation tokentrtab,
   1.144 -      prtabs = Printer.extend_prtabs mode xprods prtabs}, stamp ())
   1.145 +      prtabs = Printer.update_prtabs mode xprods prtabs}, stamp ())
   1.146    end;
   1.147  
   1.148  
   1.149 @@ -317,7 +310,7 @@
   1.150        parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
   1.151        print_ast_trtab, tokentrtab, prtabs} = tabs;
   1.152      val input' = if inout then subtract (op =) xprods input else input;
   1.153 -    val changed = input <> input';
   1.154 +    val changed = length input <> length input';
   1.155      fun if_inout xs = if inout then xs else [];
   1.156    in
   1.157      Syntax
   1.158 @@ -375,8 +368,8 @@
   1.159  
   1.160  val basic_syn =
   1.161    empty_syntax
   1.162 -  |> extend_syntax mode_default TypeExt.type_ext
   1.163 -  |> extend_syntax mode_default SynExt.pure_ext;
   1.164 +  |> update_syntax mode_default TypeExt.type_ext
   1.165 +  |> update_syntax mode_default SynExt.pure_ext;
   1.166  
   1.167  val basic_nonterms =
   1.168    (Lexicon.terminals @ [SynExt.logic, "type", "types", "sort", "classes",
   1.169 @@ -619,31 +612,27 @@
   1.170  
   1.171  (** modify syntax **)
   1.172  
   1.173 -fun ext_syntax f decls = extend_syntax mode_default (f decls);
   1.174 +fun ext_syntax f decls = update_syntax mode_default (f decls);
   1.175  
   1.176 -val extend_type_gram       = ext_syntax Mixfix.syn_ext_types;
   1.177 -val extend_consts          = ext_syntax SynExt.syn_ext_const_names;
   1.178 -val extend_trfuns          = ext_syntax SynExt.syn_ext_trfuns;
   1.179 -val extend_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns;
   1.180 +val update_type_gram       = ext_syntax Mixfix.syn_ext_types;
   1.181 +val update_consts          = ext_syntax SynExt.syn_ext_const_names;
   1.182 +val update_trfuns          = ext_syntax SynExt.syn_ext_trfuns;
   1.183 +val update_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns;
   1.184  val extend_tokentrfuns     = ext_syntax SynExt.syn_ext_tokentrfuns;
   1.185  
   1.186 -fun extend_const_gram is_logtype prmode decls =
   1.187 -  extend_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);
   1.188 +fun update_const_gram is_logtype prmode decls =
   1.189 +  update_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);
   1.190  
   1.191  fun remove_const_gram is_logtype prmode decls =
   1.192    remove_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);
   1.193  
   1.194 -fun update_const_gram is_logtype prmode decls =
   1.195 -  let val syn_ext = Mixfix.syn_ext_consts is_logtype decls
   1.196 -  in remove_syntax prmode syn_ext #> extend_syntax prmode syn_ext end;
   1.197 -
   1.198 -fun extend_trrules ctxt is_logtype syn =
   1.199 +fun update_trrules ctxt is_logtype syn =
   1.200    ext_syntax SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
   1.201  
   1.202  fun remove_trrules ctxt is_logtype syn =
   1.203    remove_syntax mode_default o SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
   1.204  
   1.205 -val extend_trrules_i = ext_syntax SynExt.syn_ext_rules o cert_rules;
   1.206 +val update_trrules_i = ext_syntax SynExt.syn_ext_rules o cert_rules;
   1.207  val remove_trrules_i = remove_syntax mode_default o SynExt.syn_ext_rules o cert_rules;
   1.208  
   1.209