# HG changeset patch # User haftmann # Date 1194524475 -3600 # Node ID 93da87a1d2b366e5421ab396cdc716dad980206f # Parent 027a63deb61c5d7bf963d9c57544d6d91b394064 added purify_sym diff -r 027a63deb61c -r 93da87a1d2b3 src/Tools/code/code_name.ML --- a/src/Tools/code/code_name.ML Thu Nov 08 13:21:14 2007 +0100 +++ b/src/Tools/code/code_name.ML Thu Nov 08 13:21:15 2007 +0100 @@ -12,6 +12,7 @@ sig val purify_var: string -> string val purify_tvar: string -> string + val purify_sym: string -> string val check_modulename: string -> string type var_ctxt; val make_vars: string list -> var_ctxt; @@ -39,7 +40,7 @@ (** purification **) -fun purify_name upper_else_lower = +fun purify_name upper lower = let fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'"; val is_junk = not o is_valid andf Symbol.is_regular; @@ -49,9 +50,10 @@ (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode) --| junk)) -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::); - fun upper_lower cs = if upper_else_lower then nth_map 0 Symbol.to_ascii_upper cs - else (if forall Symbol.is_ascii_upper cs - then map else nth_map 0) Symbol.to_ascii_lower cs; + fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs + else if lower then (if forall Symbol.is_ascii_upper cs + then map else nth_map 0) Symbol.to_ascii_lower cs + else cs; in explode #> scan_valids @@ -62,7 +64,7 @@ end; fun purify_var "" = "x" - | purify_var v = purify_name false v; + | purify_var v = purify_name false true v; fun purify_tvar "" = "'a" | purify_tvar v = @@ -71,7 +73,7 @@ fun check_modulename mn = let val mns = NameSpace.explode mn; - val mns' = map (purify_name true) mns; + val mns' = map (purify_name true false) mns; in if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n" ^ "perhaps try " ^ quote (NameSpace.implode mns')) @@ -179,25 +181,27 @@ (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular)) #> implode #> NameSpace.explode - #> map (purify_name true); + #> map (purify_name true false); -fun purify_base "op &" = "and" - | purify_base "op |" = "or" - | purify_base "op -->" = "implies" - | purify_base "{}" = "empty" - | purify_base "op :" = "member" - | purify_base "op Int" = "intersect" - | purify_base "op Un" = "union" - | purify_base "*" = "product" - | purify_base "+" = "sum" - | purify_base s = if String.isPrefix "op =" s - then "eq" ^ purify_name false s - else purify_name false s; +fun purify_base _ "op &" = "and" + | purify_base _ "op |" = "or" + | purify_base _ "op -->" = "implies" + | purify_base _ "{}" = "empty" + | purify_base _ "op :" = "member" + | purify_base _ "op Int" = "intersect" + | purify_base _ "op Un" = "union" + | purify_base _ "*" = "product" + | purify_base _ "+" = "sum" + | purify_base lower s = if String.isPrefix "op =" s + then "eq" ^ purify_name false lower s + else purify_name false lower s; + +val purify_sym = purify_base false; fun default_policy thy get_basename get_thyname name = let val prefix = (purify_prefix o get_thyname thy) name; - val base = (purify_base o get_basename) name; + val base = (purify_base true o get_basename) name; in NameSpace.implode (prefix @ [base]) end; fun class_policy thy = default_policy thy NameSpace.base thyname_of_class; @@ -222,7 +226,7 @@ of NONE => default_policy thy NameSpace.base thyname_of_const c | SOME thyname => let val prefix = purify_prefix thyname; - val base = (purify_base o NameSpace.base) c; + val base = (purify_base true o NameSpace.base) c; in NameSpace.implode (prefix @ [base]) end;