There is a common name-binding pattern, where a forward declaration of a name is allowed to appear in any place where a statement is allowed. This declaration is basically an implicit block, since the declaration is only visible in the following statements. The declaration defines a new scope which is then used for the follow-up statements. I do not want to make this implicit block explicit in a preprocessing step, so I need to propagate potential new scopes from statement to statement, very similar to a fold, where the intermediate result is propagated from list element to list element.

So I came up with the following:

signature
  constraint generator

    Fold [[ List(a) ^ (b, c) ]]
    
rules

  Fold [[ [] ^ (s, s) ]].
  Fold [[ [x|xs] ^ (s1, s3) ]] :=
    [[x ^ (s1, s2) ]],
    Fold [[ xs ^ (s2, s3) ]].

I then use it like this:

  [[ Block(stmts) ^ (scope, scope) ]] :=
    // new lexical scope for block
    new block_scope,
    block_scope -P-> scope,
    // statements in block scope
    Fold [[ stmts ^ (block_scope, _) ]].

  [[ VarDecl(v, t) ^ (scope, var_scope) ]] :=
    // new lexical scope for variable declaration
    new var_scope,
    // declare local variable
    Variable{v} <- var_scope,
    Variable{v}: t.

I haven’t tested this yet, since I need to do more work on the remaining statements.

How do you handle this kind of pattern in other languages? Should Fold become part of the standard library for NaBL2?

Submitted by Guido Wachsmuth on 16 March 2017 at 12:33

Yes, I develop similar library definitions, which I tend to call Map; see below for my library from the Tiger definition. The problem with this approach is that the generator function you call from the Map or Fold may not get a specific label. I have a number of different Maps, since each collects types in a different way or passes different number of scopes. To properly address this we probably need to support higher-order functions; not building in support for particular patterns.

rules // auxiliary

  [[ None() ^ (s) ]] := true.
  [[ Some(e) ^ (s) ]] := [[ e ^ (s) ]].

  Map[[ [] ^ (s) ]] := true.   
  Map[[ [ x | xs ] ^ (s) ]] := 
    [[ x ^ (s) ]], Map[[ xs ^ (s) ]].
    
  Map2[[ [] ^ (s, s') ]] := true.   
  Map2[[ [ x | xs ] ^ (s, s') ]] := 
    [[ x ^ (s, s') ]], Map2[[ xs ^ (s, s') ]].
    
  MapT2[[ [] ^ (s, s') : [] ]] := true.   
  MapT2[[ [ x | xs ] ^ (s, s') : [ty | tys] ]] := 
    [[ x ^ (s, s') : ty ]], MapT2[[ xs ^ (s, s') : tys ]].
   
  MapTs[[ [] ^ (s) : [] ]] := true.   
  MapTs[[ [ x | xs ] ^ (s) : [ty1 | tys] ]] := 
    [[ x ^ (s) : ty2 ]], 
    ty1 == ty2 | error $[type mismatch] @ x,
    MapTs[[ xs ^ (s) : tys ]].
   
  MapSTs[[ [] ^ (s) : [] ]] := true.   
  MapSTs[[ [ x | xs ] ^ (s) : [ty1 | tys] ]] := 
    [[ x ^ (s) : ty2 ]], 
    ty2 <? ty1 | error $[type [ty1] expected] @ x,
    MapSTs[[ xs ^ (s) : tys ]].
   
  MapTs2[[ [] ^ (s1, s2) : [] ]] := true.   
  MapTs2[[ [ x | xs ] ^ (s1, s2) : [ty | tys] ]] := 
    [[ x ^ (s1, s2) : ty ]], MapTs2[[ xs ^ (s1, s2) : tys ]].