[ new ] Add %nomangle (#2063)

This is (for once) not a breaking changes, instead backends will need to opt in to this change, using the utilities in Compiler.NoMangle. See the js backend for an example of how to do this.

This is the first step to being able to use idris to create libraries usable by other languages.

docs/source/backends/index.rst

@@ -65,7 +65,7 @@ running ``:set profile`` at the REPL. The profile data generated will depend
 on the back end you are using. Currently, the Chez and Racket back ends
 support generating profile data.
 
-There are five code generators provided in Idris 2, and (later) there will be
+There are five code generators provided in Idris 2, and there is
 a system for plugging in new code generators for a variety of targets. The
 default is to compile via Chez Scheme, with an alternative via Racket or Gambit.
 You can set the code generator at the REPL with the `:set codegen` command,
@@ -86,3 +86,11 @@ There are also external code generators that aren't part of the main Idris 2
 repository and can be found on Idris 2 wiki:
 
 `External backends <https://github.com/idris-lang/Idris2/wiki/External-backends>`_
+
+There is work in progress support for generating
+libraries for other languages from idris2 code.
+
+.. toctree::
+   :maxdepth: 1
+
+   libraries

docs/source/backends/libraries.rst

@@ -0,0 +1,32 @@
+***************
+Libraries
+***************
+
+This pragma tells the backend what name to use for a given function.
+
+.. code-block:: idris
+
+    %nomangle
+    foo : Int -> Int
+    foo x = x + 1
+
+On backends that support this feature, the function will be called ``foo``
+rather than being mangled, with the namespace.
+
+If the name you want to use isn't a valid idris identifier, you can use a different name
+for the idris name and name that appears in the compiled code, e.g.
+
+.. code-block:: idris
+
+    %nomangle "$_baz"
+    baz : Int
+    baz = 42
+
+You can also specificy different names for different backends, in a similar way to %foreign
+
+.. code-block:: idris
+
+    %nomangle "refc:idr_add_one"
+              "node:add_one"
+    plusOne : Bits32 -> Bits32
+    plusOne x = x + 1

idris2api.ipkg

@@ -14,6 +14,7 @@ modules =
     Compiler.Generated,
     Compiler.Inline,
     Compiler.LambdaLift,
+    Compiler.NoMangle,
     Compiler.Opts.CSE,
     Compiler.Separate,
     Compiler.VMCode,
@@ -155,6 +156,7 @@ modules =
     Libraries.Data.List.Lazy,
     Libraries.Data.List1,
     Libraries.Data.NameMap,
+    Libraries.Data.NameMap.Traversable,
     Libraries.Data.PosMap,
     Libraries.Data.Primitives,
     Libraries.Data.SortedMap,

libs/base/Language/Reflection/TTImp.idr

@@ -90,6 +90,11 @@ mutual
        Unique : AltType
        UniqueDefault : TTImp -> AltType
 
+  public export
+  data NoMangleDirective : Type where
+     CommonName : String -> NoMangleDirective
+     BackendNames : List (String, String) -> NoMangleDirective
+
   public export
   data FnOpt : Type where
        Inline : FnOpt
@@ -108,6 +113,8 @@ mutual
        Totality : TotalReq -> FnOpt
        Macro : FnOpt
        SpecArgs : List Name -> FnOpt
+       ||| Keep the user provided name during codegen
+       NoMangle : NoMangleDirective -> FnOpt
 
   public export
   data ITy : Type where

src/Compiler/Common.idr

@@ -5,6 +5,7 @@ import Compiler.ANF
 import Compiler.CompileExpr
 import Compiler.Inline
 import Compiler.LambdaLift
+import Compiler.NoMangle
 import Compiler.Opts.CSE
 import Compiler.VMCode
 
@@ -150,6 +151,7 @@ getMinimalDef (Coded ns bin)
          pure (def, Just (ns, bin))
 
 -- ||| Recursively get all calls in a function definition
+-- ||| Note: this only checks resolved names
 getAllDesc : {auto c : Ref Ctxt Defs} ->
              List Name -> -- calls to check
              IOArray (Int, Maybe (Namespace, Binary)) ->
@@ -274,13 +276,14 @@ getCompileData doLazyAnnots phase_in tm_in
            "Found names: " ++ concat (intersperse ", " $ map show $ keys ns)
          tm <- toFullNames tm_in
          natHackNames' <- traverse toResolvedNames natHackNames
+         noMangleNames <- getAllNoMangle
          -- make an array of Bools to hold which names we've found (quicker
          -- to check than a NameMap!)
          asize <- getNextEntry
          arr <- coreLift $ newArray asize
 
          defs <- get Ctxt
-         logTime "++ Get names" $ getAllDesc (natHackNames' ++ keys ns) arr defs
+         logTime "++ Get names" $ getAllDesc (natHackNames' ++ noMangleNames ++ keys ns) arr defs
 
          let entries = catMaybes !(coreLift (toList arr))
          let allNs = map (Resolved . fst) entries

src/Compiler/ES/Codegen.idr

@@ -12,9 +12,11 @@ import Compiler.ES.Doc
 import Compiler.ES.ToAst
 import Compiler.ES.TailRec
 import Compiler.ES.State
+import Compiler.NoMangle
 import Libraries.Data.SortedMap
 import Libraries.Utils.Hex
 import Libraries.Data.String.Extra
+import Libraries.Data.NameMap
 
 import Data.Vect
 
@@ -71,15 +73,18 @@ jsIdent s = concatMap okchar (unpack s)
                   then cast c
                   else "x" ++ asHex (cast c)
 
+jsReservedNames : List String
+jsReservedNames =
+  [ "var", "switch"
+  , "return", "const"
+  , "function", "break"
+  , "continue"
+  ]
+
 keywordSafe : String -> String
-keywordSafe "var"    = "var$"
+keywordSafe s = if s `elem` jsReservedNames
-keywordSafe "switch" = "switch$"
+  then s ++ "$"
-keywordSafe "return" = "return$"
+  else s
-keywordSafe "const"  = "const$"
-keywordSafe "function" = "function$"
-keywordSafe "break"  = "break$"
-keywordSafe "continue" = "continue$"
-keywordSafe s = s
 
 --------------------------------------------------------------------------------
 --          JS Name
@@ -90,16 +95,22 @@ jsUserName (Basic n) = keywordSafe $ jsIdent n
 jsUserName (Field n) = "rf__" ++ jsIdent n
 jsUserName Underscore = keywordSafe $ jsIdent "_"
 
+jsMangleName : Name -> String
+jsMangleName (NS ns n) = jsIdent (showNSWithSep "_" ns) ++ "_" ++ jsMangleName n
+jsMangleName (UN n) = jsUserName n
+jsMangleName (MN n i) = jsIdent n ++ "_" ++ show i
+jsMangleName (PV n d) = "pat__" ++ jsMangleName n
+jsMangleName (DN _ n) = jsMangleName n
+jsMangleName (Nested (i, x) n) = "n__" ++ show i ++ "_" ++ show x ++ "_" ++ jsMangleName n
+jsMangleName (CaseBlock x y) = "case__" ++ jsIdent x ++ "_" ++ show y
+jsMangleName (WithBlock x y) = "with__" ++ jsIdent x ++ "_" ++ show y
+jsMangleName (Resolved i) = "fn__" ++ show i
+
+parameters (noMangle : NoMangleMap)
   jsName : Name -> String
-jsName (NS ns n) = jsIdent (showNSWithSep "_" ns) ++ "_" ++ jsName n
+  jsName n = case isNoMangle noMangle n of
-jsName (UN n) = jsUserName n
+    Just name => name
-jsName (MN n i) = jsIdent n ++ "_" ++ show i
+    Nothing => jsMangleName n
-jsName (PV n d) = "pat__" ++ jsName n
-jsName (DN _ n) = jsName n
-jsName (Nested (i, x) n) = "n__" ++ show i ++ "_" ++ show x ++ "_" ++ jsName n
-jsName (CaseBlock x y) = "case__" ++ jsIdent x ++ "_" ++ show y
-jsName (WithBlock x y) = "with__" ++ jsIdent x ++ "_" ++ show y
-jsName (Resolved i) = "fn__" ++ show i
 
   jsNameDoc : Name -> Doc
   jsNameDoc = Text . jsName
@@ -111,8 +122,9 @@ mainExpr = MN "__mainExpression" 0
 --          Pretty Printing
 --------------------------------------------------------------------------------
 
+parameters (noMangle : NoMangleMap)
   var : Var -> Doc
-var (VName x) = jsNameDoc x
+  var (VName x) = jsNameDoc noMangle x
   var (VLoc x)  = Text $ "$" ++ asHex (cast x)
   var (VRef x)  = Text $ "$R" ++ asHex (cast x)
 
@@ -472,11 +484,12 @@ searchForeign knownBackends decls =
 -- generate a toplevel function definition.
 makeForeign :  {auto d : Ref Ctxt Defs}
             -> {auto c : Ref ESs ESSt}
+            -> {auto nm : Ref NoMangleMap NoMangleMap}
             -> (name : Name)
             -> (ffDecl : String)
             -> Core Doc
 makeForeign n x = do
-  nd <- var <$> getOrRegisterRef n
+  nd <- var !(get NoMangleMap) <$> getOrRegisterRef n
   let (ty, def) = readCCPart x
   case ty of
     "lambda" => pure . constant nd . paren $ Text def
@@ -506,6 +519,7 @@ makeForeign n x = do
 -- to extract a declaration for one of the supported backends.
 foreignDecl :  {auto d : Ref Ctxt Defs}
             -> {auto c : Ref ESs ESSt}
+            -> {auto nm : Ref NoMangleMap NoMangleMap}
             -> Name
             -> List String
             -> Core Doc
@@ -602,9 +616,9 @@ switch sc alts def =
 -- creates an argument list for a (possibly multi-argument)
 -- anonymous function. An empty argument list is treated
 -- as a delayed computation (prefixed by `() =>`).
-lambdaArgs : List Var -> Doc
+lambdaArgs : (noMangle : NoMangleMap) -> List Var -> Doc
-lambdaArgs [] = "()" <+> lambdaArrow
+lambdaArgs noMangle [] = "()" <+> lambdaArrow
-lambdaArgs xs = hcat $ (<+> lambdaArrow) . var <$> xs
+lambdaArgs noMangle xs = hcat $ (<+> lambdaArrow) . var noMangle <$> xs
 
 insertBreak : (r : Effect) -> (Doc, Doc) -> (Doc, Doc)
 insertBreak Returns x = x
@@ -612,12 +626,20 @@ insertBreak (ErrorWithout _) (pat, exp) = (pat, vcat [exp, "break;"])
 
 mutual
   -- converts an `Exp` to JS code
-  exp : {auto c : Ref ESs ESSt} -> Exp -> Core Doc
+  exp :  {auto c : Ref ESs ESSt}
-  exp (EMinimal x) = pure $ minimal x
+      -> {auto nm : Ref NoMangleMap NoMangleMap}
-  exp (ELam xs (Return $ y@(ECon _ _ _))) =
+      -> Exp
-     map (\e => lambdaArgs xs <+> paren e) (exp y)
+      -> Core Doc
-  exp (ELam xs (Return $ y)) = (lambdaArgs xs <+> ) <$> exp y
+  exp (EMinimal x) = pure $ minimal !(get NoMangleMap) x
-  exp (ELam xs y) = (lambdaArgs xs <+>) . block <$> stmt y
+  exp (ELam xs (Return $ y@(ECon _ _ _))) = do
+     nm <- get NoMangleMap
+     map (\e => lambdaArgs nm xs <+> paren e) (exp y)
+  exp (ELam xs (Return $ y)) = do
+     nm <- get NoMangleMap
+     (lambdaArgs nm xs <+> ) <$> exp y
+  exp (ELam xs y) = do
+     nm <- get NoMangleMap
+     (lambdaArgs nm xs <+>) . block <$> stmt y
   exp (EApp x xs) = do
     o    <- exp x
     args <- traverse exp xs
@@ -631,18 +653,27 @@ mutual
   exp EErased = pure "undefined"
 
   -- converts a `Stmt e` to JS code.
-  stmt : {e : _} -> {auto c : Ref ESs ESSt} -> Stmt e -> Core Doc
+  stmt :  {e : _}
+       -> {auto c : Ref ESs ESSt}
+       -> {auto nm : Ref NoMangleMap NoMangleMap}
+       -> Stmt e
+       -> Core Doc
   stmt (Return y) = (\e => "return" <++> e <+> ";") <$> exp y
-  stmt (Const v x) = constant (var v) <$> exp x
+  stmt (Const v x) = do
-  stmt (Declare v s) =
+    nm <- get NoMangleMap
-    (\d => vcat ["let" <++> var v <+> ";",d]) <$> stmt s
+    constant (var nm v) <$> exp x
-  stmt (Assign v x) =
+  stmt (Declare v s) = do
-    (\d => hcat [var v,softEq,d,";"]) <$> exp x
+    nm <- get NoMangleMap
+    (\d => vcat ["let" <++> var nm v <+> ";",d]) <$> stmt s
+  stmt (Assign v x) = do
+    nm <- get NoMangleMap
+    (\d => hcat [var nm v,softEq,d,";"]) <$> exp x
 
   stmt (ConSwitch r sc alts def) = do
     as <- traverse (map (insertBreak r) . alt) alts
     d  <- traverseOpt stmt def
-    pure $  switch (minimal sc <+> ".h") as d
+    nm <- get NoMangleMap
+    pure $  switch (minimal nm sc <+> ".h") as d
     where
         alt : {r : _} -> EConAlt r -> Core (Doc,Doc)
         alt (MkEConAlt _ RECORD b)  = ("undefined",) <$> stmt b
@@ -678,7 +709,10 @@ printDoc Compact y = compact y
 printDoc Minimal y = compact y
 
 -- generate code for the given toplevel function.
-def : {auto c : Ref ESs ESSt} -> Function -> Core String
+def :  {auto c : Ref ESs ESSt}
+    -> {auto nm : Ref NoMangleMap NoMangleMap}
+    -> Function
+    -> Core String
 def (MkFunction n as body) = do
   reset
   ref  <- getOrRegisterRef n
@@ -689,14 +723,15 @@ def (MkFunction n as body) = do
     -- zero argument toplevel functions are converted to
     -- lazily evaluated constants.
     [] => pure $ printDoc mde $
-      constant (var ref) (
+      constant (var !(get NoMangleMap) ref) (
         "__lazy(" <+> function neutral [] b <+> ")"
       )
-    _  => pure $ printDoc mde $ function (var ref) (map var args) b
+    _  => pure $ printDoc mde $ function (var !(get NoMangleMap) ref) (map (var !(get NoMangleMap)) args) b
 
 -- generate code for the given foreign function definition
 foreign :  {auto c : Ref ESs ESSt}
         -> {auto d : Ref Ctxt Defs}
+        -> {auto nm : Ref NoMangleMap NoMangleMap}
         -> (Name,FC,NamedDef)
         -> Core (List String)
 foreign (n, _, MkNmForeign path _ _) = pure . pretty <$> foreignDecl n path
@@ -707,11 +742,24 @@ foreign _                            = pure []
 tailRec : Name
 tailRec = UN $ Basic "__tailRec"
 
+validJSName : String -> Bool
+validJSName name =
+    not (name `elem` jsReservedNames)
+    && all validNameChar (unpack name)
+    && (case strM name of
+      StrNil => True
+      StrCons head _ => not $ isDigit head)
+  where
+    validNameChar : Char -> Bool
+    validNameChar c = isAlphaNum c || c == '_' || c == '$'
+
 ||| Compiles the given `ClosedTerm` for the list of supported
 ||| backends to JS code.
 export
 compileToES : Ref Ctxt Defs -> (cg : CG) -> ClosedTerm -> List String -> Core String
 compileToES c cg tm ccTypes = do
+  _ <- initNoMangle "javascript" validJSName
+
   cdata      <- getCompileData False Cases tm
 
   -- read a derive the codegen mode to use from
@@ -722,7 +770,7 @@ compileToES c cg tm ccTypes = do
              else Pretty
 
   -- initialize the state used in the code generator
-  s <- newRef ESs $ init mode (isArg mode) isFun ccTypes
+  s <- newRef ESs $ init mode (isArg mode) isFun ccTypes !(get NoMangleMap)
 
   -- register the toplevel `__tailRec` function to make sure
   -- it is not mangled in `Minimal` mode
@@ -743,7 +791,7 @@ compileToES c cg tm ccTypes = do
   foreigns <- concat <$> traverse foreign allDefs
 
   -- lookup the (possibly mangled) name of the main function
-  mainName <- compact . var <$> getOrRegisterRef mainExpr
+  mainName <- compact . var !(get NoMangleMap) <$> getOrRegisterRef mainExpr
 
   -- main function and list of all declarations
   let main =  "try{"

src/Compiler/ES/State.idr

@@ -4,6 +4,7 @@ module Compiler.ES.State
 
 import Core.Context
 import Compiler.ES.Ast
+import Compiler.NoMangle
 import Libraries.Data.SortedMap
 
 %default total
@@ -105,6 +106,9 @@ record ESSt where
   ||| `["browser","javascript"]`.
   ccTypes  : List String
 
+  ||| %nomangle names
+  noMangleMap : NoMangleMap
+
 --------------------------------------------------------------------------------
 --          Local Variables
 --------------------------------------------------------------------------------
@@ -174,10 +178,12 @@ nextRef = do
   put ESs $ record { ref $= (+1) } st
   pure $ VRef st.ref
 
-registerRef : {auto c : Ref ESs ESSt} -> (name : Name) -> Core Var
+registerRef :  {auto c : Ref ESs ESSt}
+            -> (name : Name)
+            -> Core Var
 registerRef n = do
   st <- get ESs
-  if keepRefName n st.mode
+  if keepRefName n st.mode || isJust (isNoMangle st.noMangleMap n)
      then let v = VName n in addRef n v >> pure v
      else do v <- nextRef
              addRef n v
@@ -188,7 +194,9 @@ registerRef n = do
 ||| The name will be replace with an index if the current
 ||| `GCMode` is set to `Minimal`.
 export
-getOrRegisterRef : {auto c : Ref ESs ESSt} -> Name -> Core Var
+getOrRegisterRef :  {auto c : Ref ESs ESSt}
+                 -> Name
+                 -> Core Var
 getOrRegisterRef n = do
   Nothing <- lookup n . refs <$> get ESs
     | Just v => pure v
@@ -226,9 +234,10 @@ init :  (mode  : CGMode)
      -> (isArg : Exp -> Bool)
      -> (isFun : Exp -> Bool)
      -> (types : List String)
+     -> (noMangle : NoMangleMap)
      -> ESSt
-init mode isArg isFun ccs =
+init mode isArg isFun ccs noMangle =
-  MkESSt mode isArg isFun 0 0 empty empty empty ccs
+  MkESSt mode isArg isFun 0 0 empty empty empty ccs noMangle
 
 ||| Reset the local state before defining a new toplevel
 ||| function.

src/Compiler/NoMangle.idr

@@ -0,0 +1,81 @@
+||| Utilities for dealing with %nomangle functions
+module Compiler.NoMangle
+
+import Core.Core
+import Core.Context
+import Libraries.Data.NameMap
+import Libraries.Data.NameMap.Traversable
+
+export
+record NoMangleMap where
+    constructor MkNMMap
+    map : NameMap (Maybe String)
+
+findNoMangle : List DefFlag -> Maybe NoMangleDirective
+findNoMangle [] = Nothing
+findNoMangle (NoMangle x :: _) = Just x
+findNoMangle (_ :: xs) = findNoMangle xs
+
+||| Get a map of all %nomangle names
+||| Errors for all invalid names, so the backend can skip checking
+||| or adding escape characters.
+||| @ backend what backend is this being used in?
+||| @ valid a validator to check a name is valid
+|||         for the given backend
+export
+initNoMangle :
+    {auto d : Ref Ctxt Defs} ->
+    (backend : String) ->
+    (valid : String -> Bool) ->
+    Core (Ref NoMangleMap NoMangleMap)
+initNoMangle backend valid = do
+    defs <- get Ctxt
+    let ctxt = defs.gamma
+    map <- traverseNameMap
+        (\nm, res => do
+            Just gdef <- lookupCtxtExact (Resolved res) ctxt
+                | Nothing => pure Nothing
+            let Just ns = findNoMangle gdef.flags
+                | Nothing => pure Nothing
+            name <- case ns of
+                CommonName name => pure name
+                BackendNames ns =>
+                    maybe
+                        (throw (InternalError "missing %nomangle name for \{show nm} on \{backend} backend"))
+                        pure
+                        (lookupBackend ns)
+            let True = valid name
+                | False => throw (InternalError "\{show name} is not a valid name on the \{backend} backend")
+            pure $ Just name
+        ) ctxt.resolvedAs
+    newRef NoMangleMap $ MkNMMap map
+  where
+    lookupBackend : List (String, String) -> Maybe String
+    lookupBackend [] = Nothing
+    lookupBackend ((b, n) :: ns) = if b == backend then Just n else lookupBackend ns
+
+export
+isNoMangle : NoMangleMap -> Name -> Maybe String
+isNoMangle nm n = join $ lookup n nm.map
+
+export
+lookupNoMangle :
+    {auto nm : Ref NoMangleMap NoMangleMap} ->
+    Name ->
+    Core (Maybe String)
+lookupNoMangle n = pure $ isNoMangle !(get NoMangleMap) n
+
+export
+getAllNoMangle : {auto c : Ref Ctxt Defs} -> Core (List Name)
+getAllNoMangle = do
+    defs <- get Ctxt
+    foldlNames (addNames defs) (pure []) defs.gamma.resolvedAs
+  where
+    addNames : Defs -> Core (List Name) -> Name -> Int -> Core (List Name)
+    addNames defs acc _ res = do
+        Just gdef <- lookupCtxtExact (Resolved res) defs.gamma
+            | Nothing => acc
+        let Just name = findNoMangle gdef.flags
+            | Nothing => acc
+        ns <- acc
+        pure $ (Resolved res) :: ns

src/Core/Context/Context.idr

@@ -191,6 +191,11 @@ Show Clause where
   show (MkClause {vars} env lhs rhs)
       = show vars ++ ": " ++ show lhs ++ " = " ++ show rhs
 
+public export
+data NoMangleDirective : Type where
+    CommonName : String -> NoMangleDirective
+    BackendNames : List (String, String) -> NoMangleDirective
+
 public export
 data DefFlag
     = Inline
@@ -222,6 +227,8 @@ data DefFlag
     | Identity Nat
          -- Is it the identity function at runtime?
          -- The nat represents which argument the function evaluates to
+    | NoMangle NoMangleDirective
+         -- use the user provided name directly (backend, name)
 
 export
 Eq DefFlag where
@@ -237,6 +244,7 @@ Eq DefFlag where
     (==) AllGuarded AllGuarded = True
     (==) (ConType x) (ConType y) = x == y
     (==) (Identity x) (Identity y) = x == y
+    (==) (NoMangle _) (NoMangle _) = True
     (==) _ _ = False
 
 export
@@ -253,6 +261,7 @@ Show DefFlag where
   show AllGuarded = "allguarded"
   show (ConType ci) = "contype " ++ show ci
   show (Identity x) = "identity " ++ show x
+  show (NoMangle _) = "nomangle"
 
 public export
 data SizeChange = Smaller | Same | Unknown

src/Core/TTC.idr

@@ -1016,6 +1016,16 @@ TTC TotalReq where
              2 => pure PartialOK
              _ => corrupt "TotalReq"
 
+TTC NoMangleDirective where
+  toBuf b (CommonName n) = do tag 0; toBuf b n
+  toBuf b (BackendNames ns) = do tag 1; toBuf b ns
+
+  fromBuf b
+      = case !getTag of
+             0 => do n <- fromBuf b; pure (CommonName n)
+             1 => do ns <- fromBuf b; pure (BackendNames ns)
+             _ => corrupt "NoMangleDirective"
+
 TTC DefFlag where
   toBuf b Inline = tag 2
   toBuf b NoInline = tag 13
@@ -1029,6 +1039,7 @@ TTC DefFlag where
   toBuf b AllGuarded = tag 10
   toBuf b (ConType ci) = do tag 11; toBuf b ci
   toBuf b (Identity x) = do tag 12; toBuf b x
+  toBuf b (NoMangle x) = do tag 14; toBuf b x
 
   fromBuf b
       = case !getTag of
@@ -1044,6 +1055,7 @@ TTC DefFlag where
              11 => do ci <- fromBuf b; pure (ConType ci)
              12 => do x <- fromBuf b; pure (Identity x)
              13 => pure NoInline
+             14 => do x <- fromBuf b; pure (NoMangle x)
              _ => corrupt "DefFlag"
 
 export

src/Idris/Parser.idr

@@ -1399,6 +1399,32 @@ fnDirectOpt fname
   <|> do pragma "foreign"
          cs <- block (expr pdef fname)
          pure $ PForeign cs
+  <|> do pragma "nomangle"
+         commit
+         ns <- many (strBegin *> strLit <* strEnd)
+         ns' <- parseNoMangle ns
+         pure $ IFnOpt (NoMangle ns')
+  where
+    parseNames : List String -> List (Maybe String, String)
+    parseNames = map
+        (\x => case split (== ':') x of
+            name ::: [] => (Nothing, name)
+            bck ::: ns => (Just bck, concat ns))
+
+    parseNoMangle : List String -> EmptyRule (Maybe NoMangleDirective)
+    parseNoMangle [] = pure Nothing
+    parseNoMangle ns = case parseNames ns of
+        [(Nothing, name)] => pure $ Just $ CommonName name
+        ns =>
+            let ns = the (Either String (List (String, String))) $
+                    traverse
+                    (\case
+                        (Nothing, _) => Left "expected backend specifier and name, found name"
+                        (Just b, name) => Right (b, name))
+                    ns
+             in case ns of
+                Left msg => fail msg
+                Right ns => pure $ Just $ BackendNames ns
 
 builtinDecl : OriginDesc -> IndentInfo -> Rule PDecl
 builtinDecl fname indents

src/Libraries/Data/NameMap.idr

@@ -383,3 +383,13 @@ export
 mapMaybeM : Monad m => (Name -> m (Maybe a)) -> NameMap v -> m (NameMap a)
 mapMaybeM test Empty = pure Empty
 mapMaybeM test (M _ t) = treeMapMaybeM test t
+
+treeFoldl : (acc -> Name -> v -> acc) -> acc -> Tree _ v -> acc
+treeFoldl f z (Leaf k v) = f z k v
+treeFoldl f z (Branch2 l _ r) = treeFoldl f (treeFoldl f z l) r
+treeFoldl f z (Branch3 l _ m _ r) = treeFoldl f (treeFoldl f (treeFoldl f z l) m) r
+
+export
+foldlNames : (acc -> Name -> v -> acc) -> acc -> NameMap v -> acc
+foldlNames f z Empty = z
+foldlNames f z (M _ t) = treeFoldl f z t

src/Libraries/Data/NameMap/Traversable.idr

@@ -0,0 +1,22 @@
+module Libraries.Data.NameMap.Traversable
+
+import Core.Core
+import Core.Name
+import Libraries.Data.NameMap
+
+treeTraverse : (Name -> a -> Core b) -> Tree h a -> Core (Tree h b)
+treeTraverse f (Leaf k v) = Leaf k <$> f k v
+treeTraverse f (Branch2 l k r) =
+    (\l', r' => Branch2 l' k r')
+    <$> treeTraverse f l
+    <*> treeTraverse f r
+treeTraverse f (Branch3 l k1 m k2 r) =
+    (\l', m', r' => Branch3 l' k1 m' k2 r')
+    <$> treeTraverse f l
+    <*> treeTraverse f m
+    <*> treeTraverse f r
+
+export
+traverseNameMap : (Name -> a -> Core b) -> NameMap a -> Core (NameMap b)
+traverseNameMap f Empty = pure Empty
+traverseNameMap f (M h t) = M h <$> treeTraverse f t

src/TTImp/ProcessType.idr

@@ -21,6 +21,7 @@ import TTImp.TTImp
 import TTImp.Utils
 
 import Data.List
+import Data.List1
 import Data.String
 import Libraries.Data.NameMap
 
@@ -43,6 +44,7 @@ processFnOpt : {auto c : Ref Ctxt Defs} ->
                Name -> FnOpt -> Core ()
 processFnOpt fc _ ndef Inline
     = do throwIfHasFlag fc ndef NoInline "%noinline and %inline are mutually exclusive"
+         throwIfHasFlag fc ndef (NoMangle (CommonName "")) "%nomangle and %inline are mutually exclusive"
          setFlag fc ndef Inline
 processFnOpt fc _ ndef NoInline
     = do throwIfHasFlag fc ndef Inline "%inline and %noinline are mutually exclusive"
@@ -72,6 +74,18 @@ processFnOpt fc _ ndef (Totality tot)
     = setFlag fc ndef (SetTotal tot)
 processFnOpt fc _ ndef Macro
     = setFlag fc ndef Macro
+processFnOpt fc True ndef (NoMangle mname) = do
+    throwIfHasFlag fc ndef Inline "%inline and %nomangle are mutually exclusive"
+    name <- case mname of
+        Nothing => case userNameRoot !(getFullName ndef) of
+            Nothing => throw (GenericMsg fc "Unable to find user name root of \{show ndef}")
+            Just (Basic name) => pure $ CommonName name
+            Just (Field name) => pure $ CommonName name
+            Just Underscore => throw (GenericMsg fc "Unable to set '_' as %nomangle")
+        Just name => pure name
+    setFlag fc ndef (NoMangle name)
+    setFlag fc ndef NoInline
+processFnOpt fc False ndef (NoMangle _) = throw (GenericMsg fc "Unable to set %nomangle for non-global functions")
 processFnOpt fc _ ndef (SpecArgs ns)
     = do defs <- get Ctxt
          Just gdef <- lookupCtxtExact ndef (gamma defs)

src/TTImp/Reflect.idr

@@ -271,6 +271,19 @@ mutual
                _ => cantReify val "AltType"
     reify defs val = cantReify val "AltType"
 
+  export
+  Reify NoMangleDirective where
+    reify defs val@(NDCon _ n _ _ args)
+        = case (dropAllNS !(full (gamma defs) n), args) of
+               (UN (Basic "CommonName"), [(_, name)])
+                    => do n <- reify defs !(evalClosure defs name)
+                          pure $ CommonName n
+               (UN (Basic "BackendNames"), [(_, names)])
+                    => do ns <- reify defs !(evalClosure defs names)
+                          pure $ BackendNames ns
+               _ => cantReify val "NoMangleDirective"
+    reify defs val = cantReify val "NoMangleDirective"
+
   export
   Reify FnOpt where
     reify defs val@(NDCon _ n _ _ args)
@@ -296,6 +309,9 @@ mutual
                (UN (Basic "SpecArgs"), [(_, x)])
                     => do x' <- reify defs !(evalClosure defs x)
                           pure (SpecArgs x')
+               (UN (Basic "NoMangle"), [(_, n)])
+                    => do ds <- reify defs !(evalClosure defs n)
+                          pure (NoMangle ds)
                _ => cantReify val "FnOpt"
     reify defs val = cantReify val "FnOpt"
 
@@ -637,6 +653,15 @@ mutual
         = do x' <- reflect fc defs lhs env x
              appCon fc defs (reflectionttimp "UniqueDefault") [x']
 
+  export
+  Reflect NoMangleDirective where
+    reflect fc defs lhs env (CommonName n)
+        = do n' <- reflect fc defs lhs env n
+             appCon fc defs (reflectionttimp "CommonName") [n']
+    reflect fc defs lhs env (BackendNames ns)
+        = do ns' <- reflect fc defs lhs env ns
+             appCon fc defs (reflectionttimp "BackendNames") [ns']
+
   export
   Reflect FnOpt where
     reflect fc defs lhs env Inline = getCon fc defs (reflectionttimp "Inline")
@@ -660,6 +685,9 @@ mutual
     reflect fc defs lhs env (SpecArgs r)
         = do r' <- reflect fc defs lhs env r
              appCon fc defs (reflectionttimp "SpecArgs") [r']
+    reflect fc defs lhs env (NoMangle n)
+        = do n' <- reflect fc defs lhs env n
+             appCon fc defs (reflectionttimp "NoMangle") [n']
 
   export
   Reflect ImpTy where

src/TTImp/TTImp.idr

@@ -230,12 +230,18 @@ mutual
        Totality : TotalReq -> FnOpt' nm
        Macro : FnOpt' nm
        SpecArgs : List Name -> FnOpt' nm
+       NoMangle : Maybe NoMangleDirective -> FnOpt' nm
 
   public export
   isTotalityReq : FnOpt' nm -> Bool
   isTotalityReq (Totality _) = True
   isTotalityReq _ = False
 
+  export
+  Show NoMangleDirective where
+    show (CommonName name) = "\"\{name}\""
+    show (BackendNames ns) = showSep " " (map (\(b, n) => "\"\{b}:\{n}\"") ns)
+
   export
   covering
   Show nm => Show (FnOpt' nm) where
@@ -252,6 +258,14 @@ mutual
     show (Totality PartialOK) = "partial"
     show Macro = "%macro"
     show (SpecArgs ns) = "%spec " ++ showSep " " (map show ns)
+    show (NoMangle Nothing) = "%nomangle"
+    show (NoMangle (Just ns)) = "%nomangle \{show ns}"
+
+  export
+  Eq NoMangleDirective where
+    CommonName x == CommonName y = x == y
+    BackendNames xs == BackendNames ys = xs == ys
+    _ == _ = False
 
   export
   Eq FnOpt where
@@ -266,6 +280,7 @@ mutual
     (Totality tot_lhs) == (Totality tot_rhs) = tot_lhs == tot_rhs
     Macro == Macro = True
     (SpecArgs ns) == (SpecArgs ns') = ns == ns'
+    (NoMangle x) == (NoMangle y) = x == y
     _ == _ = False
 
   public export
@@ -1232,6 +1247,19 @@ mutual
              con <- fromBuf b; fs <- fromBuf b
              pure (MkImpRecord fc n ps con fs)
 
+  export
+  TTC NoMangleDirective where
+    toBuf b (CommonName n)
+        = do tag 0; toBuf b n
+    toBuf b (BackendNames ns)
+        = do tag 1; toBuf b ns
+
+    fromBuf b
+        = case !getTag of
+               0 => do n <- fromBuf b; pure (CommonName n)
+               1 => do ns <- fromBuf b; pure (BackendNames ns)
+               _ => corrupt "NoMangleDirective"
+
   export
   TTC FnOpt where
     toBuf b Inline = tag 0
@@ -1247,6 +1275,7 @@ mutual
     toBuf b (Totality PartialOK) = tag 8
     toBuf b Macro = tag 9
     toBuf b (SpecArgs ns) = do tag 10; toBuf b ns
+    toBuf b (NoMangle name) = do tag 13; toBuf b name
 
     fromBuf b
         = case !getTag of
@@ -1263,6 +1292,7 @@ mutual
                10 => do ns <- fromBuf b; pure (SpecArgs ns)
                11 => pure TCInline
                12 => pure NoInline
+               13 => do name <- fromBuf b; pure (NoMangle name)
                _ => corrupt "FnOpt"
 
   export

src/TTImp/TTImp/Functor.idr

@@ -121,6 +121,7 @@ mutual
     map f (Totality tot) = Totality tot
     map f Macro = Macro
     map f (SpecArgs ns) = SpecArgs ns
+    map f (NoMangle name) = (NoMangle name)
 
   export
   Functor ImpTy' where

tests/Main.idr

@@ -284,6 +284,7 @@ nodeTests = MkTestPool "Node backend" [] (Just Node)
     , "integers"
     , "fix1839"
     , "tailrec_libs"
+    , "nomangle001", "nomangle002"
     ]
 
 vmcodeInterpTests : IO TestPool

tests/node/nomangle001/expected

@@ -0,0 +1,6 @@
+function foo($0) {
+function $_baz($0) {
+function another_name($0) {
+function foo($0){return $0;}
+function $_baz($0){return $0;}
+function another_name($0){return $0;}

tests/node/nomangle001/nomangle.idr

@@ -0,0 +1,16 @@
+
+%nomangle
+foo : Int -> Int
+foo x = x
+
+%nomangle "$_baz"
+baz : Int -> Int
+baz x = x
+
+%nomangle "refc:idr_another_name"
+          "javascript:another_name"
+anotherName : Int -> Int
+anotherName x = x
+
+main : IO ()
+main = pure ()

tests/node/nomangle001/run

@@ -0,0 +1,7 @@
+rm -rf build
+
+$1 nomangle.idr --no-color --no-banner --console-width 0 -o test1 --cg node
+$1 nomangle.idr --no-color --no-banner --console-width 0 -o test2 --cg node --directive minimal
+
+cat build/exec/test1 | grep -e foo -e baz -e another_name
+cat build/exec/test2 | grep -e foo -e baz -e another_name

tests/node/nomangle002/expected

@@ -0,0 +1,2 @@
+Error: INTERNAL ERROR: "continue" is not a valid name on the javascript backend
+Error: INTERNAL ERROR: missing %nomangle name for Main.break on javascript backend

tests/node/nomangle002/nomangle1.idr

@@ -0,0 +1,7 @@
+
+%nomangle
+continue : Int -> Int
+continue x = x + 1
+
+main : IO ()
+main = pure ()

tests/node/nomangle002/nomangle2.idr

@@ -0,0 +1,11 @@
+
+%nomangle
+continue : Int -> Int
+continue x = x + 1
+
+%nomangle "refc:break"
+break : Int -> Int
+break x = x + 1
+
+main : IO ()
+main = pure ()

tests/node/nomangle002/run

@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 nomangle1.idr --no-color --no-banner --console-width 0 -o test --cg node
+$1 nomangle2.idr --no-color --no-banner --console-width 0 -o test --cg node