SparseCaseOptimisation removes useful alternatives

[AlexandreTunstall]

On commit 2976a999612ed8137a1e6d9381a8360eac96626d (current HEAD).

In src.grin:

grinMain =
  v <- pure (CA)
  print v
  v2t <- pure (Fother v)
  v2 <- eval v2t
  print v2

print x =
  case x of
    (CA) -> _prim_int_print 1
    (CB) -> _prim_int_print 2

other y = 
  case y of
    (CA) -> pure (CB)
    (CB) -> pure (CA)

eval thunk =
  case thunk of
    (Fother yt) ->
      other yt

Interpreting with stack exec -- grin src.grin --eval yields the output 12 (), but if I run the optimisations with stack exec -- grin src.grin, the resulting code is:

grinMain =
  v <- pure (CA)
  _prim_int_print $ 1
  pure v

Interpreting this code yields 1 (CA), which is different from the output before optimisations.

---

This appears to happen due to SparseCaseOptimisation.

Before, in 004.InlineEval.grin:

grinMain =
  v <- pure (CA)
  print $ v
  v2t <- pure (Fother v)
  v2 <- do
    thunk.0 <- pure v2t
    (Fother yt.0) <- pure thunk.0
    other $ yt.0
  print $ v2

print x =
  case x of
    (CA) ->
      _prim_int_print $ 1
    (CB) ->
      _prim_int_print $ 2

other y =
  case y of
    (CA) ->
      pure (CB)
    (CB) ->
      pure (CA)

After, in 005.SparseCaseOptimisation.grin:

grinMain =
  v <- pure (CA)
  print $ v
  v2t <- pure (Fother v)
  v2 <- do
    thunk.0 <- pure v2t
    (Fother yt.0) <- pure thunk.0
    other $ yt.0
  print $ v2

print x =
  case x of
    (CA) ->
      _prim_int_print $ 1

other y =
  case y of

[andorp]

  v <- pure (CA)
  ...
  v2t <- pure (Fother v)

This seems to be an invalid construction in GRIN. as the Variable v holds to a Node value and it is used in building the (Fother v) node. There is an invariant that the parameters for node values must be locations or simple types. Thus the construction of (Fother v) is invalid.

[AlexandreTunstall]

The syntax reference in the README claims that variables are simple types. Is it out of date, or am I reading it wrong?

Would it be possible to add a case to the linter to catch the mistake? At the moment, the linter gives no warnings/errors on the above program.

[andorp]

The grammar from the PhD is over-generative. Variables in those position must hold to location OR simple types. This comes from the nature of representing the nodes of the evaluation graph in GRIN. Let me find the reference for this in the PhD...

About the linter: It has two modes one that uses a calculated type-environment and one that doesn't. If the type env is present the linter is smarter. For some reason the calculation of the type-environemint in your provided example is failing.

Meanwhile I try to construct a well formed example based on the snippet you provided. The one that uses heap, still has some errors. I'll post that version soon, but it needs a bit deeper digging.

[andorp]

This one:

grinMain =
  v <- pure (CA)
  print v
  v3 <- store v
  v2t <- store (Cother v3)
  v2 <- eval v2t
  print v2

print x =
  case x of
    (CA) -> _prim_int_print 1
    (CB) -> _prim_int_print 2

other y =
  o2 <- fetch y
  o1 <- case o2 of
    (CA) -> pure (CB)
    (CB) -> pure (CA)
  pure o1

eval thunk =
  e1 <- fetch thunk
  case e1 of
    (Cother yt) ->
      other yt

reduces to this:

grinMain =
  _prim_int_print $ 1
  _prim_int_print $ 2

[AlexandreTunstall]

Thanks. Do you want me to leave this open for the lack of linter error?

By the way, the linter gives "expected SimpleVal" errors when using store with a tag (e.g. store (Cother v3) in your fix). Are there any cases where the linter error is justified?

[andorp]

We are in a phase transition from the current syntax to a more restrictive one. See the 32-extended-syntax feature branch.

The misleading error message from the linker is a byproduct of the initial transition. For the interprocedural dead data eliminations need a special form where values can created only using pure simple expression. The new syntax will restrict the AST into that form. That would mean the following snippet:

  v3 <- store v
  v4 <- pure (Fother v3)
  v2t <- store v4
  v2 <- eval v2t

[andorp]

Closing this one as the extract of this conversation can be found in the #76 .

[andorp]

The parameters of node are mentioned slightly in Section 2.4.1 Restrictions. The origin of this restriction comes from the implementation of the HeapPointsTo. Its description can be found in Section 3.2 HPT .