Re: [Caml-list] Static exception in lambda code

[luc.maranget@inria.fr (Luc Maranget)]

> Luc Maranget suggested that static exception mechanism in lambda code,
> namely Lstaticcatch and Lstaticraise, could be used to implement break
> and continue.
> 
> However, this doesn't work right now. In bytecomp/simplif.ml,
> simplify_exits simplify
> (catch (seq (exit 1) (assign a b)) with (1) unit) to
> (seq unit (assign a b))
> which is not appropriate.

Interesting.

> 
> The comment says: "simplify catch body with (i ...) handler ... if
> (exit i ...) occurs exactly once in body, substitute it with handler".
> simplify_exits suppress catch if no exit occurs in body, which is
> nice, but this simplification is dangerous if one is to use this
> mechanism to implement break and continue.
> 
> So, which is the case?
> 1. The simplification is not safe, so it should be removed.
> 2. The simplification is consistent with intended semantics of static
> catch/raise, so static catch/raise is not directly useful to implement
> break/continue or for that matter, return.

Point 2, I guess. Simplifiation assumes a local-function semantics

(exit 1 e) is (apply f1 e)
(catch e1 (1 x) e2) is let f x = e1 in e1
[additionally, (exit i e) always occur in terminal position in e1]

This is the semantics assumed by the pattern-matching compiler, which
introduces all those exit/catch in the lambda-code.

However, later in the compiler (eg bytecode production)
(remaining) exit/catch pairs are compiled
as follows (informaly)

(exit i) ->
  branch labi

(catch e1 with (1 x) e2) ->
   [[ e1 ]]
   branch end 
 labi:
    [[ e2 ]]
 end: 
(actual code may be slightly different, with additional
stack adjustments)

Hence my idea to compile break with exit/catch


But, as you discovered, optimizing away break is wrong,
because you loose the branch/label effect.

There may be a simple solution :
add a flag to Lstaticatch, so as to inform simplif
wether the problematic optimization apply to it or not.

There is a similar trick in simplif for let's,
let's are tagged for simplif to know what kind of
optimisation are applicable to them.

Cf. <bytecomp/lambda.mli>


type let_kind = Strict | Alias | StrictOpt | Variable

(* Meaning of kinds for let x = e in e':
    Strict: e may have side-effets; always evaluate e first
      (If e is a simple expression, e.g. a variable or constant,
       we may still substitute e'[x/e].)
    Alias: e is pure, we can substitute e'[x/e] if x has 0 or 1 occurrences
      in e'
    StrictOpt: e does not have side-effects, but depend on the store;
      we can discard e if x does not appear in e'
    Variable: the variable x is assigned later in e' *)


catch's from the match compiler should probably be something
like Alias, which catch's from break/continue should
probably be something like StrictOpt.


Finally, there remains a (potential) pitfall in the
semantics assumed by the match compiler :
  (exit 1 e) is (apply f1 e)
  (catch e1 (1 x) e2) is let f x = e1 in e1
  [additionally, (exit i e) always occur in tail-call position in e1]

This is [...]

I assume that you think the following to be  valid code :

  for k=1 to n do
    f (if .. then break else ())
  done

Then break is not in tail call position. I have the feeling it does
not hurt, but such things require more investigation.

-- 
Luc