added token translation support;
authorwenzelm
Fri Feb 28 16:46:26 1997 +0100 (1997-02-28)
changeset 270080e6b48c5204
parent 2699 932fae4271d7
child 2701 348ec44248df
added token translation support;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Fri Feb 28 16:45:38 1997 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Feb 28 16:46:26 1997 +0100
     1.3 @@ -39,6 +39,7 @@
     1.4      (string * (term list -> term)) list *
     1.5      (string * (ast list -> ast)) list -> syntax
     1.6    val extend_trfunsT: syntax -> (string * (typ -> term list -> term)) list -> syntax
     1.7 +  val extend_tokentrfuns: syntax -> (string * string * (string -> string * int)) list -> syntax
     1.8    val extend_trrules: syntax -> (string * string) trrule list -> syntax
     1.9    val extend_trrules_i: syntax -> ast trrule list -> syntax
    1.10    val merge_syntaxes: syntax -> syntax -> syntax
    1.11 @@ -69,7 +70,6 @@
    1.12  
    1.13  (** tables of translation functions **)
    1.14  
    1.15 -(*the ref serves as unique id*)
    1.16  (*does not subsume typed print translations*)
    1.17  type 'a trtab = (('a list -> 'a) * stamp) Symtab.table;
    1.18  
    1.19 @@ -96,6 +96,41 @@
    1.20  
    1.21  
    1.22  
    1.23 +(** tables of token translation functions **)
    1.24 +
    1.25 +fun lookup_tokentr tabs modes =
    1.26 +  let val trs = gen_distinct eq_fst (flat (map (assocs tabs) (modes @ [""])))
    1.27 +  in fn c => apsome fst (assoc (trs, c)) end;
    1.28 +
    1.29 +fun merge_tokentrtabs tabs1 tabs2 =
    1.30 +  let
    1.31 +    fun eq_tr ((c1, (_, s1)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2;
    1.32 +
    1.33 +    fun merge mode =
    1.34 +      let
    1.35 +        val trs1 = assocs tabs1 mode;
    1.36 +        val trs2 = assocs tabs2 mode;
    1.37 +        val trs = gen_distinct eq_tr (trs1 @ trs2);
    1.38 +      in
    1.39 +        (case gen_duplicates eq_fst trs of
    1.40 +          [] => (mode, trs)
    1.41 +        | dups => error ("More than one token translation function in mode " ^
    1.42 +            quote mode ^ " for " ^ commas_quote (map fst dups)))
    1.43 +      end;
    1.44 +  in
    1.45 +    map merge (distinct (map fst (tabs1 @ tabs2)))
    1.46 +  end;
    1.47 +
    1.48 +fun extend_tokentrtab tabs tokentrs =
    1.49 +  let
    1.50 +    fun ins_tokentr (ts, (m, c, f)) =
    1.51 +      overwrite (ts, (m, ("_" ^ c, (f, stamp ())) :: assocs ts m));
    1.52 +  in
    1.53 +    merge_tokentrtabs tabs (foldl ins_tokentr ([], tokentrs))
    1.54 +  end;
    1.55 +
    1.56 +
    1.57 +
    1.58  (** tables of translation rules **)
    1.59  
    1.60  type ruletab = (ast * ast) list Symtab.table;
    1.61 @@ -137,6 +172,7 @@
    1.62      print_trtab: ((typ -> term list -> term) * stamp) Symtab.table,
    1.63      print_ruletab: ruletab,
    1.64      print_ast_trtab: ast trtab,
    1.65 +    tokentrtab: (string * (string * ((string -> string * int) * stamp)) list) list,
    1.66      prtabs: prtabs};
    1.67  
    1.68  
    1.69 @@ -154,6 +190,7 @@
    1.70      print_trtab = empty_trtab,
    1.71      print_ruletab = empty_ruletab,
    1.72      print_ast_trtab = empty_trtab,
    1.73 +    tokentrtab = [],
    1.74      prtabs = empty_prtabs};
    1.75  
    1.76  
    1.77 @@ -163,10 +200,10 @@
    1.78    let
    1.79      val {lexicon, logtypes = logtypes1, gram, consts = consts1,
    1.80        parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
    1.81 -      print_ast_trtab, prtabs} = tabs;
    1.82 +      print_ast_trtab, tokentrtab, prtabs} = tabs;
    1.83      val SynExt {logtypes = logtypes2, xprods, consts = consts2, parse_ast_translation,
    1.84        parse_rules, parse_translation, print_translation, print_rules,
    1.85 -      print_ast_translation} = syn_ext;
    1.86 +      print_ast_translation, token_translation} = syn_ext;
    1.87    in
    1.88      Syntax {
    1.89        lexicon = if inout then extend_lexicon lexicon (delims_of xprods) else lexicon,
    1.90 @@ -181,6 +218,7 @@
    1.91        print_ruletab = extend_ruletab print_ruletab print_rules,
    1.92        print_ast_trtab =
    1.93          extend_trtab print_ast_trtab print_ast_translation "print ast translation",
    1.94 +      tokentrtab = extend_tokentrtab tokentrtab token_translation,
    1.95        prtabs = extend_prtabs prtabs mode xprods}
    1.96    end;
    1.97  
    1.98 @@ -193,13 +231,13 @@
    1.99        consts = consts1, 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 -      prtabs = prtabs1} = tabs1;
   1.103 +      tokentrtab = tokentrtab1, prtabs = prtabs1} = tabs1;
   1.104  
   1.105      val {lexicon = lexicon2, logtypes = logtypes2, gram = gram2,
   1.106        consts = consts2, parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
   1.107        parse_trtab = parse_trtab2, print_trtab = print_trtab2,
   1.108        print_ruletab = print_ruletab2, print_ast_trtab = print_ast_trtab2,
   1.109 -      prtabs = prtabs2} = tabs2;
   1.110 +      tokentrtab = tokentrtab2, prtabs = prtabs2} = tabs2;
   1.111    in
   1.112      Syntax {
   1.113        lexicon = merge_lexicons lexicon1 lexicon2,
   1.114 @@ -214,13 +252,16 @@
   1.115        print_ruletab = merge_ruletabs print_ruletab1 print_ruletab2,
   1.116        print_ast_trtab =
   1.117          merge_trtabs print_ast_trtab1 print_ast_trtab2 "print ast translation",
   1.118 +      tokentrtab = merge_tokentrtabs tokentrtab1 tokentrtab2,
   1.119        prtabs = merge_prtabs prtabs1 prtabs2}
   1.120    end;
   1.121  
   1.122  
   1.123  (* type_syn *)
   1.124  
   1.125 -val type_syn = extend_syntax ("", true) empty_syntax type_ext;
   1.126 +val type_syn =
   1.127 +  extend_syntax ("", true) empty_syntax type_ext;
   1.128 +
   1.129  val pure_syn = extend_syntax ("", true) type_syn pure_ext;
   1.130  
   1.131  
   1.132 @@ -401,10 +442,11 @@
   1.133  
   1.134  fun pretty_t t_to_ast prt_t curried (syn as Syntax tabs) t =
   1.135    let
   1.136 -    val {print_trtab, print_ruletab, print_ast_trtab, prtabs, ...} = tabs;
   1.137 +    val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
   1.138      val ast = t_to_ast (lookup_trtab print_trtab) t;
   1.139    in
   1.140      prt_t curried prtabs (lookup_trtab print_ast_trtab)
   1.141 +      (lookup_tokentr tokentrtab (! print_mode))
   1.142        (normalize_ast (lookup_ruletab print_ruletab) ast)
   1.143    end;
   1.144  
   1.145 @@ -439,6 +481,8 @@
   1.146  
   1.147  val extend_trfunsT = ext_syntax syn_ext_trfunsT ("", true);
   1.148  
   1.149 +val extend_tokentrfuns = ext_syntax syn_ext_tokentrfuns ("", true);
   1.150 +
   1.151  fun extend_trrules syn rules =
   1.152    ext_syntax syn_ext_rules ("", true) syn (prep_rules (read_pattern syn) rules);
   1.153