| /- | |
| Copyright (c) 2018 Microsoft Corporation. All rights reserved. | |
| Released under Apache 2.0 license as described in the file LICENSE. | |
| Author: Leonardo de Moura | |
| -/ | |
| import Lean.Data.Name | |
| namespace Lean | |
| private def String.mangleAux : Nat → String.Iterator → String → String | |
| | 0, it, r => r | |
| | i+1, it, r => | |
| let c := it.curr | |
| if c.isAlpha || c.isDigit then | |
| mangleAux i it.next (r.push c) | |
| else if c = '_' then | |
| mangleAux i it.next (r ++ "__") | |
| else if c.toNat < 255 then | |
| let n := c.toNat | |
| let r := r ++ "_x" | |
| let r := r.push $ Nat.digitChar (n / 16) | |
| let r := r.push $ Nat.digitChar (n % 16) | |
| mangleAux i it.next r | |
| else | |
| let n := c.toNat | |
| let r := r ++ "_u" | |
| let r := r.push $ Nat.digitChar (n / 4096) | |
| let n := n % 4096 | |
| let r := r.push $ Nat.digitChar (n / 256) | |
| let n := n % 256 | |
| let r := r.push $ Nat.digitChar (n / 16) | |
| let r := r.push $ Nat.digitChar (n % 16) | |
| mangleAux i it.next r | |
| def String.mangle (s : String) : String := | |
| String.mangleAux s.length s.mkIterator "" | |
| private def Name.mangleAux : Name → String | |
| | Name.anonymous => "" | |
| | Name.str p s _ => | |
| let m := String.mangle s | |
| match p with | |
| | Name.anonymous => m | |
| | p => mangleAux p ++ "_" ++ m | |
| | Name.num p n _ => mangleAux p ++ "_" ++ toString n ++ "_" | |
| @[export lean_name_mangle] | |
| def Name.mangle (n : Name) (pre : String := "l_") : String := | |
| pre ++ Name.mangleAux n | |
| @[export lean_mk_module_initialization_function_name] | |
| def mkModuleInitializationFunctionName (moduleName : Name) : String := | |
| "initialize_" ++ moduleName.mangle "" | |
| end Lean |