use shadowing for state

[brabalan]

We should always use shadowing for state. For instance

and run_binary_op_add s c v1 v2 =
  let%spec (s1, (w1, w2)) = (convert_twice_primitive s c v1 v2) in
  if  (type_compare (type_of w1) Coq_type_string)
   || (type_compare (type_of w2) Coq_type_string)
  then let%spec (s2, (str1, str2)) = (convert_twice_string s1 c w1 w2) in
    res_out s2 (res_val (Coq_value_string (strappend str1 str2)))
  else let%spec (s2, (n1, n2)) = (convert_twice_number s1 c w1 w2) in
    res_out s2 (res_val (Coq_value_number (n1 +. n2)))

should be

and run_binary_op_add s c v1 v2 =
  let%spec (s, (w1, w2)) = (convert_twice_primitive s c v1 v2) in
  if  (type_compare (type_of w1) Coq_type_string)
   || (type_compare (type_of w2) Coq_type_string)
  then let%spec (s, (str1, str2)) = (convert_twice_string s c w1 w2) in
    res_out s (res_val (Coq_value_string (strappend str1 str2)))
  else let%spec (s, (n1, n2)) = (convert_twice_number s c w1 w2) in
    res_out s (res_val (Coq_value_number (n1 +. n2)))

[brabalan]

Dealt with 07f480c1dc1758afb7a31bbe53b838ba95131221

[IgnoredAmbience]

Shadowing is broken when binding to variables in patterns. This may also apply to tuple patterns and elsewhere in the codebase.

ppf_match_binders needs to be changed to only use var if not shadowing, and each caller to it. binders is a list of strstr,should be list of strstr*bool (corresponding to check shadowing). Chase the resulting type errors:

• generate_logged_cases - taking and passing binders
• js_of_branch
• js_of_pattern - Tpat_construct case. Tpat_var id case needs a shadowing check, bool as third field of tuple.

Similar with tuple_component_bind.

[IgnoredAmbience]

Test for pattern binders added in 9c8d4c3

[IgnoredAmbience]

Fix committed in fe7d1526

[IgnoredAmbience]

Do not use the environment to detect shadowing: detect shadowing for the wrong reason.

The only time a var is not fine is a match for the same value. Non-monadic let with the same value.

Restrict shadowing check.

1) Handle our own list of variable declarations. List of things declared in current JS scope. 2) Disable shadowing. 3) Name reuse in monadic calls are not shadowed, so should be fine.

[brabalan]

Alternative approach: do automatic renaming to avoid shadowing

• we carry a map around of shadowed names to their renaming (or to an integer)
• ppf_ident_name takes an additional shadow map argument sm to rename the identifier, pass an empty map to not rename anything
• do_check_shadowing takes the map as argument and use it to compute the renamed name, it returns the updated map
  • if the identifier is shadowed, check if it is in the map
    • if so, increase the integer in the map by one and return the map and the identifier to use
    • if not, add it to the map with integer 0 and return the map and the identifier to use
  • otherwise, simply return the map and the original identifier

[IgnoredAmbience]

Function argument patterns do not need a shadowing check, as they shadow in both JS and ML.

[brabalan]

Todo

• change ppf_match_binders to always introduce var
• change apply_dest to always introduce var

[IgnoredAmbience]

Scoping still possibly broken. In jsjsref, running the following test results in a failed heap lookup in the first field dereferencing. This is resulting from a location being compared with an object value. Somewhere a type-cast hasn't stuck. This is either due to the type-casting function being incorrectly compiled, or more likely due to miscompilation of the complex scoping of the base variable in get_value in JsInterpreter.ml. base is rebound 5 locations in this function, including with let%ret and let%OBJECT_ret binders.

var x = { a : { c : 1 } };
x.a.b = 2;
x.a.x = x;
x

[IgnoredAmbience]

get_value is miscompiled. In particular:

let_ret(..., function(_tuple_arg_5) {
  var base𝟙 = _tuple_arg_5[1];
  var s𝟘 = _tuple_arg_5[0];
  return ( object_internal_get(s, base𝟘, get_referenced_name(v𝟘), get_this_value(v𝟘)));
})

corresponds to

let%ret (s, base) = ...
in object_internal_get s base (get_referenced_name v) (get_this_value v)

It would appear that a tuple pattern in a monadic let binding is not updating the shadowing map.

[IgnoredAmbience]

Whilst fixing this, I've noticed much duplicated code for various sections of the compiler, particularly in function compilation having a monad special case.

I'm also finding that mixing in of logged, unlogged, token generation and psuedocode modes make reading the core compilation code extremely hard to read. In the long run it may be worth refactoring the code generation to output to a JS AST, which then has further passes to generate the various variants of output.