1structure ProvideUnicode :> ProvideUnicode =
2struct
3
4open HolKernel Feedback
5
6open term_grammar
7
8type term = Term.term
9
10datatype uni_version =
11         RuleUpdate of {newrule : term_grammar.grule}
12       | OverloadUpdate of { u : string, ts : term list }
13
14(* This uni_version type encodes a number of different options for
15   the way in which a Unicode string can be an alternative for a
16   syntactic form.
17
18   If it's a RuleUpdate{u,term_name,newrule,oldtok} form, then u is the
19   list of tokens appearing in newrule, which maps to term_name,
20   and oldtok is an ASCII token of the old rule (if any).
21
22   If it's a OverloadUpdate{u,ts} then u is to be put in as an
23   additional overload from u to the terms ts.
24*)
25
26fun getrule G term_name = let
27  fun tok_of0 es =
28      case es of
29        [] => raise Fail "Unicode.getrule: should never happen"
30      | RE (TOK s) :: _ => s
31      | _ :: rest => tok_of0 rest
32  fun tok_of {elements, ...} = tok_of0 elements
33
34  fun rreplace rf {term_name,paren_style,elements,timestamp,block_style} s =
35      {term_name=term_name, paren_style = paren_style,
36       pp_elements = map (fn (RE (TOK _)) => RE (TOK s) | x => x)
37                         elements,
38       block_style = block_style,
39       fixity = rf}
40  fun search_rrlist rf tfopt k (rrlist : rule_record list) =
41      case rrlist of
42        [] => k tfopt
43      | r :: rest => let
44        in
45          if #term_name r = term_name then let
46              val tfopt' =
47                  case tfopt of
48                    NONE => SOME(#timestamp r, (rreplace rf r, tok_of r))
49                  | SOME (t', _) =>
50                    if #timestamp r > t' then
51                      SOME(#timestamp r, (rreplace rf r, tok_of r))
52                    else tfopt
53            in
54              search_rrlist rf tfopt' k rest
55            end
56          else search_rrlist rf tfopt k rest
57        end
58
59  fun breplace s = binder_grule {term_name = term_name, tok = s}
60  fun search_bslist tfopt k blist =
61      case blist of
62        [] => k tfopt
63      | LAMBDA :: rest => search_bslist tfopt k rest
64      | BinderString {timestamp, term_name = nm, tok} :: rest =>
65        if nm = term_name then let
66            val tfopt' =
67                case tfopt of
68                  NONE => SOME (timestamp, (breplace, tok))
69                | SOME (t', _) => if timestamp > t' then
70                                    SOME (timestamp, (breplace, tok))
71                                  else tfopt
72          in
73            search_bslist tfopt' k rest
74          end
75        else search_bslist tfopt k rest
76
77  fun get_rule_data tf_opt  rs =
78      case rs of
79        [] => Option.map #2 tf_opt
80      | (fixopt, grule) :: rest => let
81        in
82          case grule of
83            PREFIX (BINDER blist) => let
84            in
85              search_bslist tf_opt
86                            (fn tfopt => get_rule_data tfopt rest)
87                            blist
88            end
89          | PREFIX (STD_prefix rrlist) =>
90            search_rrlist (Prefix (valOf fixopt)) tf_opt
91                          (fn tfopt => get_rule_data tfopt rest)
92                          rrlist
93          | SUFFIX TYPE_annotation => get_rule_data tf_opt rest
94          | SUFFIX (STD_suffix rrlist) =>
95            search_rrlist (Suffix (valOf fixopt)) tf_opt
96                          (fn tfopt => get_rule_data tfopt rest)
97                          rrlist
98          | INFIX (STD_infix (rrlist, assoc)) =>
99            search_rrlist (Infix(assoc, valOf fixopt)) tf_opt
100                          (fn tfopt => get_rule_data tfopt rest)
101                          rrlist
102          | INFIX _ => get_rule_data tf_opt rest
103          | CLOSEFIX _ => get_rule_data tf_opt rest
104             (* only support single token overloads and a closefix form must
105                involve two tokens at once *)
106        end
107in
108  get_rule_data NONE (rules G)
109end
110
111fun sd_to_deltas sd =
112  case sd of
113      RuleUpdate {newrule = r} => [GRULE r]
114    | OverloadUpdate{u,ts} => map (fn t => OVERLOAD_ON(u,t)) ts
115
116fun mk_unicode_version {u,tmnm} G = let
117  val oi = term_grammar.overload_info G
118  val sd =
119      case getrule G tmnm of
120        NONE => let
121        in
122          case Overload.info_for_name oi tmnm of
123            NONE => raise mk_HOL_ERR "Unicode" "mk_unicode_version"
124                                     ("No data for term with name "^tmnm)
125          | SOME ops => OverloadUpdate{u = u, ts = #actual_ops ops}
126        end
127      | SOME(f,s) => RuleUpdate{newrule = f u}
128in
129  sd_to_deltas sd
130end
131
132end (* struct *)
133