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