Enable local variables in functions (#1023)

Closes keyboardDrummer#24

## Changes

**LaurelToCoreTranslator.lean**: In the `translateExpr` case for `Block`
with `LocalVariable` (with initializer), replaced the `disallowed` error
with the actual translation:

```lean
let coreMonoType ← translateType ty
return .app () (.abs () name.text (some coreMonoType) bodyExpr) valueExpr
```

This encodes `var x: T := v; body` as the beta-redex `(λ x:T. body) v`,
which the Core evaluator already handles via beta reduction, and the
`Preconditions` module already handles as a let-binding pattern.

**T3_ControlFlowError.lean**: Removed the three `error: local variables
in functions are not YET supported` annotations and the associated
comments, since local variables in functions are now supported.

## Verification

- `LaurelToCoreTranslator` builds successfully
- All Laurel fundamental tests pass (`T1` through `T21`)
- All transform tests pass

Co-authored-by: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>

Author: keyboardDrummer-bot

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

@@ -275,10 +275,8 @@ def translateExpr (expr : StmtExprMd)
   | .Block (⟨ .LocalVariable name ty (some initializer), innerSrc, innerMd⟩ :: rest) label => do
       let valueExpr ← translateExpr  initializer boundVars isPureContext
       let bodyExpr ← translateExpr { val := StmtExpr.Block rest label, source := innerSrc, md := innerMd } (name :: boundVars) isPureContext
-      disallowed (fileRangeToCoreMd innerSrc innerMd) "local variables in functions are not YET supported"
-      -- This doesn't work because of a limitation in Core.
-      -- let coreMonoType := translateType ty
-      -- return .app () (.abs () (some coreMonoType) bodyExpr) valueExpr
+      let coreMonoType ← translateType ty
+      return .app () (.abs () name.text (some coreMonoType) bodyExpr) valueExpr
   | .Block (⟨ .LocalVariable name ty none, innerSrc, innerMd⟩ :: rest) label =>
     disallowed (fileRangeToCoreMd innerSrc innerMd) "local variables in functions must have initializers"
   | .Block (⟨ .IfThenElse cond thenBranch (some elseBranch), innerSrc, innerMd⟩ :: rest) label =>

StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean

@@ -22,15 +22,10 @@ function assertAndAssumeInFunctions(a: int) returns (r: int)
   a
 };
 
-// Lettish bindings in functions not yet supported
-// because Core expressions do not support let bindings
 function letsInFunction() returns (r: int) {
   var x: int := 0;
-//^^^^^^^^^^^^^^^ error: local variables in functions are not YET supported
   var y: int := x + 1;
-//^^^^^^^^^^^^^^^^^^^ error: local variables in functions are not YET supported
   var z: int := y + 1;
-//^^^^^^^^^^^^^^^^^^^ error: local variables in functions are not YET supported
   z
 };