More powerful use of `mkAtomicNoFVs` OK?

[toelli-msft]

mkAtomicNoFVs is very useful because it provides a cheap way of preserving sharing whilst using a Haskell-level function to do "substitution" into an Expr. It comes with the caveat

we use the same variable name every time. That's not safe in general, but the bodys we use never mention any other variables, it's fine

However, it would be helpful if the bodys could bind variables! (In particular it would help Hybrid shapes https://github.com/microsoft/knossos-ksc/pull/766). I think that NB3 below is correct, isn't it? (this mkAtomicNoFVs is the same as in master but with a different variable name).

@simonpj Is there a reason we wouldn't want to use mkNoAtomicFVs like this? Perhaps it's too delicate? But it is very useful!

-- (mkAtomicNoFVs e body) returns the expression (let a = e in body a)
-- where body :: TExpr -> TExpr is a function expecting an expression
-- The idea is that body might use its argument many types, and we
-- don't want to duplicate e, so we let-bind it instead
--
-- NB1: there's a short-cut when e is trivial (e.g. another variable)
--
-- NB2: we use the same variable name every time.  That's not safe in
--      general, but if body never mention any other variables,
--      it's fine c.f. the more general Opt.makeAtomic, which does
--      not have this side condition but which requires an in-scope
--      set
--
-- NB3: However, if you want to use bodys that bind variables then
-- just make sure they never bind ksc$mkAtomicVar and all will be fine.
mkAtomicNoFVs :: TExpr -> (TExpr -> TExpr) -> TExpr
mkAtomicNoFVs e body
  | isTrivial e = body e
  | otherwise   = mkLet ev e (body (Var ev))
  where
    ev = TVar (typeof e) (Simple ("ksc$mkAtomicVar"))

[simonpj]

There are two potential gotchas to do with capturing.

• body (which is a TExpr -> TExpr function) already mentions ksc$mkAtomicVar, presumably bound by some other call of this function. E.g. suppose body x returns ksc$mkAtomicVar + x. Then the occurence of ksc$mkAtomicVar in body gets captured by this let.

  Here's a concrete example:

  mkAtomicNoFVs 3 (\v1 ->
  mkAtomicNoFVs 5 (\v2 -> v1+v2))

  This returns the expression

  let ksc$mkAtomicVar = 3 in
  let ksc$mkAtomicVar = 5 in
  ksc$mkAtomicVar + ksc$mkAtomicVar

  which is obviously wrong.

• body binds ksc$mkAtomicVar and mentions x inside that binding. Example

  mkAtomicNoFVs (Lit 4) (\x.  Lam "ksc$mkAtomicVar" x)

  This will produce

  Let "ksc$mkAtomicVar" (Lit 4) (
  Lam "ksc$mkAtomicVar" (Var "ksc$mkAtomicVar"))

  which is obviously wrong.

So long as body neither mentions no binds ksc$mkAtomicVar we are fine.