Fix bug in procedure type check

Examples/ProcedureTypeError.core.st

@@ -0,0 +1,25 @@
+program Core;
+//
+//  Copyright Strata Contributors
+//
+//  Licensed under the Apache License, Version 2.0 (the "License");
+//  you may not use this file except in compliance with the License.
+//  You may obtain a copy of the License at
+//
+//    https://www.apache.org/licenses/LICENSE-2.0
+//
+//  Unless required by applicable law or agreed to in writing, software
+//  distributed under the License is distributed on an "AS IS" BASIS,
+//  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+//  See the License for the specific language governing permissions and
+//  limitations under the License.
+//
+
+procedure SumPositive(a: int, b: int) returns (c: int)
+spec {
+    requires [precond1]: 0 <= a;
+    requires [precond2]: c <= b;
+}
+{
+    c := a + b;
+};

Examples/expected/ProcedureTypeError.core.expected

@@ -0,0 +1,3 @@
+Successfully parsed.
+❌ Type checking error.
+ProcedureTypeError.core.st(21, (4-32)) [SumPositive:precond2]: Cannot find this fvar in the context! c

Strata/Languages/Core/Procedure.lean

@@ -103,6 +103,12 @@ instance : ToFormat Procedure.Spec where
        preconditions: {format p.preconditions}\n\
        postconditions: {format p.postconditions}"
 
+def Procedure.Spec.preconditionNames (s : Procedure.Spec) : List CoreLabel :=
+  s.preconditions.keys
+
+def Procedure.Spec.postconditionNames (s : Procedure.Spec) : List CoreLabel :=
+  s.postconditions.keys
+
 def Procedure.Spec.eraseTypes (s : Procedure.Spec) : Procedure.Spec :=
   { s with
     preconditions := s.preconditions.map (fun (l, c) => (l, c.eraseTypes)),

Strata/Languages/Core/ProcedureType.lean

@@ -20,86 +20,148 @@ open Imperative (MetaData)
 
 namespace Procedure
 
-def typeCheck (C: Core.Expression.TyContext) (Env : Core.Expression.TyEnv) (p : Program)
-  (proc : Procedure) (md : MetaData Expression) : Except Format (Procedure × Core.Expression.TyEnv) :=
-  let sourceLoc := MetaData.formatFileRangeD md (includeEnd? := false)
-  let sourceLoc := if sourceLoc.isEmpty then sourceLoc else f!"{sourceLoc} "
-  let errorWithSourceLoc := fun e => if sourceLoc.isEmpty then e else f!"{sourceLoc} {e}"
+private def checkNoDuplicates (proc : Procedure) (sourceLoc : Format) :
+    Except Format Unit := do
   if !proc.header.inputs.keys.Nodup then
     .error f!"{sourceLoc}[{proc.header.name}] Duplicates found in the formals!"
-  else if !proc.header.outputs.keys.Nodup then
+  if !proc.header.outputs.keys.Nodup then
     .error f!"{sourceLoc}[{proc.header.name}] Duplicates found in the return variables!"
-  else if !proc.spec.modifies.Nodup then
+  if !proc.spec.modifies.Nodup then
     .error f!"{sourceLoc}[{proc.header.name}] Duplicates found in the modifies clause!"
-  else if proc.spec.modifies.any (fun v => v ∈ proc.header.inputs.keys) then
+
+private def checkVariableScoping (proc : Procedure) (sourceLoc : Format) :
+    Except Format Unit := do
+  if proc.spec.modifies.any (fun v => v ∈ proc.header.inputs.keys) then
     .error f!"{sourceLoc}[{proc.header.name}] Variables in the modifies clause must \
               not appear in the formals.\n\
-              Modifies: {proc.spec.modifies}\n
+              Modifies: {proc.spec.modifies}\n\
               Formals: {proc.header.inputs.keys}"
-  else if proc.spec.modifies.any (fun v => v ∈ proc.header.outputs.keys) then
+  if proc.spec.modifies.any (fun v => v ∈ proc.header.outputs.keys) then
     .error f!"{sourceLoc}[{proc.header.name}] Variables in the modifies clause must \
               not appear in the return values.\n\
-              Modifies: {proc.spec.modifies}\n
+              Modifies: {proc.spec.modifies}\n\
               Returns: {proc.header.outputs.keys}"
-  else if proc.header.inputs.keys.any (fun v => v ∈ proc.header.outputs.keys) then
-    .error f!"{sourceLoc}[{proc.header.name}] Variables in the formals must not appear \
-              in the return values.\n\
-              Formals: {proc.header.inputs.keys}\n
+  if proc.header.inputs.keys.any (fun v => v ∈ proc.header.outputs.keys) then
+    .error f!"{sourceLoc}[{proc.header.name}] Variables in the formals must \
+              not appear in the return values.\n\
+              Formals: {proc.header.inputs.keys}\n\
               Returns: {proc.header.outputs.keys}"
-  else if proc.spec.modifies.any (fun v => (Env.context.types.find? v).isNone) then
-    .error f!"{sourceLoc}[{proc.header.name}]: All the variables in the modifies \
-              clause must exist in the context! \
+
+private def checkModifiesClause (proc : Procedure) (Env : Core.Expression.TyEnv)
+    (sourceLoc : Format) : Except Format Unit := do
+  if proc.spec.modifies.any (fun v => (Env.context.types.find? v).isNone) then
+    .error f!"{sourceLoc}[{proc.header.name}]: All the variables in the modifies clause \
+              must exist in the context!\n\
               Modifies: {proc.spec.modifies}"
-  else do
-    let modifiedVars := (Imperative.Block.modifiedVars proc.body).eraseDups
-    let definedVars := (Imperative.Block.definedVars proc.body).eraseDups
-    let allowedVars := proc.header.outputs.keys ++ proc.spec.modifies ++ definedVars
-    if modifiedVars.any (fun v => v ∉ allowedVars) then
-      .error f!"{sourceLoc}[{proc.header.name}]: This procedure modifies variables it is not allowed to!\n\
-                Variables actually modified: {modifiedVars}\n\
-                Modification allowed for these variables: {allowedVars}"
-    else
-     let preconditions := Procedure.Spec.getCheckExprs proc.spec.preconditions
-     if preconditions.any (fun p => OldExpressions.containsOldExpr p) then
-      .error f!"{sourceLoc}[{proc.header.name}]: Preconditions cannot contain applications of\
-                the `old` function!"
-     else
-      -- 1. Temporarily add the formals and returns into the context.
-      let Env := Env.pushEmptyContext
-      let (mty_sig, Env) ← Lambda.LMonoTySignature.instantiate C Env proc.header.typeArgs
-                            (proc.header.inputs ++ proc.header.outputs)
-                            |>.mapError errorWithSourceLoc
-      let lty_sig := Lambda.LMonoTySignature.toTrivialLTy mty_sig
-      let Env := Env.addToContext lty_sig
-      -- 2. Normalize the old expressions in the postconditions. The evaluator
-      --    depends on this step! See also note in `OldExpressions.lean`.
-      let postcondition_checks := OldExpressions.normalizeOldChecks proc.spec.postconditions
-      -- 3. Ensure that the preconditions and postconditions are of type boolean.
-      let postconditions := postcondition_checks.map (fun (_, c) => c.expr)
-      let (preconditions_a, Env) ← Lambda.LExpr.resolves C Env preconditions |>.mapError errorWithSourceLoc
-      let pre_tys := preconditions_a.map Lambda.LExpr.toLMonoTy
-      let preconditions := preconditions_a.map Lambda.LExpr.unresolved
-      let (postconditions_a, Env) ← Lambda.LExpr.resolves C Env postconditions |>.mapError errorWithSourceLoc
-      let post_tys := postconditions_a.map Lambda.LExpr.toLMonoTy
-      let postconditions := postconditions_a.map Lambda.LExpr.unresolved
-      if (pre_tys ++ post_tys).any (fun ty => ty != .tcons "bool" []) then
-        .error f!"{sourceLoc}[{proc.header.name}]: Expected pre- and post-conditions to be of type Bool!"
-      else
-        -- 4. Typecheck the body of the procedure.
-        -- Note that `Statement.typeCheck` already reports source locations in
-        -- error messages.
-        let (annotated_body, Env) ← Statement.typeCheck C Env p (.some proc) proc.body
-        -- Remove formals and returns from the context.
-        let Env := Env.popContext
-        let preconditions := Procedure.Spec.updateCheckExprs preconditions proc.spec.preconditions
-        let postconditions := Procedure.Spec.updateCheckExprs postconditions proc.spec.postconditions
-        let new_hdr := { proc.header with typeArgs := [],
-                                          inputs := mty_sig.take proc.header.inputs.length,
-                                          outputs := mty_sig.drop proc.header.inputs.length }
-        let new_spec := { proc.spec with preconditions := preconditions, postconditions := postconditions }
-        let new_proc := { proc with header := new_hdr, spec := new_spec, body := annotated_body }
-        .ok (new_proc, Env)
+
+private def checkModificationRights (proc : Procedure) (sourceLoc : Format) :
+    Except Format Unit := do
+  let modifiedVars := (Imperative.Block.modifiedVars proc.body).eraseDups
+  let definedVars := (Imperative.Block.definedVars proc.body).eraseDups
+  let allowedVars := proc.header.outputs.keys ++ proc.spec.modifies ++ definedVars
+  if modifiedVars.any (fun v => v ∉ allowedVars) then
+    .error f!"{sourceLoc}[{proc.header.name}]: This procedure modifies variables it \
+              is not allowed to!\n\
+              Variables actually modified: {modifiedVars}\n\
+              Modification allowed for these variables: {allowedVars}"
+
+private def setupInputEnv (C : Core.Expression.TyContext) (Env : Core.Expression.TyEnv)
+    (proc : Procedure) (errorWithSourceLoc : Format → Format) :
+    Except Format (@Lambda.LMonoTySignature Visibility × Core.Expression.TyEnv) := do
+  let Env := Env.pushEmptyContext
+  let (inp_mty_sig, Env) ← Lambda.LMonoTySignature.instantiate C Env proc.header.typeArgs
+                            proc.header.inputs |>.mapError errorWithSourceLoc
+  let inp_lty_sig := Lambda.LMonoTySignature.toTrivialLTy inp_mty_sig
+  let Env := Env.addToContext inp_lty_sig
+  return (inp_mty_sig, Env)
+
+-- Error message prefix for errors in processing procedure pre/post conditions.
+def conditionErrorMsgPrefix (procName : CoreIdent) (condName : CoreLabel)
+    (md : MetaData Expression) : Format :=
+  let sourceLoc := MetaData.formatFileRangeD md (includeEnd? := true)
+  f!"{sourceLoc} [{procName}:{condName}]:"
+
+-- Type checking procedure pre/post conditions.
+-- We flag occurrences of `old` expressions in the preconditions and normalize
+-- them in the postconditions.
+open Lambda.LTy.Syntax in
+private def typeCheckConditions (C : Core.Expression.TyContext) (Env : Core.Expression.TyEnv)
+    (conditions : ListMap CoreLabel Check) (procName : CoreIdent) (checkOldExprs : Bool) :
+    Except Format (Array Expression.Expr × Core.Expression.TyEnv) := do
+  let mut results := #[]
+  let mut currentEnv := Env
+  for (name, condition) in (conditions.keys, conditions.values) do
+    let errorPrefix := conditionErrorMsgPrefix procName name condition.md
+    if checkOldExprs && OldExpressions.containsOldExpr condition.expr then
+      .error f!"{errorPrefix} Preconditions cannot contain applications of the `old` function!"
+    let expr := if checkOldExprs then condition.expr else OldExpressions.normalizeOldExpr condition.expr
+    let (annotatedExpr, newEnv) ← Lambda.LExpr.resolve C currentEnv expr
+                                    |>.mapError (fun e => f!"{errorPrefix} {e}")
+    if annotatedExpr.toLMonoTy != mty[bool] then
+      .error f!"{errorPrefix}: Expected condition to be of type Bool,\
+                but got {annotatedExpr.toLMonoTy}!"
+    results := results.push annotatedExpr.unresolved
+    currentEnv := newEnv
+  return (results, currentEnv)
+
+def typeCheck (C : Core.Expression.TyContext) (Env : Core.Expression.TyEnv) (p : Program)
+    (proc : Procedure) (md : MetaData Expression) : Except Format (Procedure × Core.Expression.TyEnv) := do
+  let sourceLoc := MetaData.formatFileRangeD md (includeEnd? := false)
+  let sourceLoc := if sourceLoc.isEmpty then sourceLoc else f!"{sourceLoc} "
+  let errorWithSourceLoc := fun e => if sourceLoc.isEmpty then e else f!"{sourceLoc} {e}"
+
+  -- Validate well-formedness of formals, returns, and modifies clause.
+  checkNoDuplicates proc sourceLoc
+  checkVariableScoping proc sourceLoc
+  checkModifiesClause proc Env sourceLoc
+  checkModificationRights proc sourceLoc
+
+  -- Temporarily add the formals into the context.
+  let (inp_mty_sig, envWithInputs) ← setupInputEnv C Env proc errorWithSourceLoc
+
+  -- Type check preconditions.
+  -- Note: `envWithInputs` does not have the return variables in the context,
+  -- which means that the presence of any return variables in the preconditions
+  -- will rightfully flag an error.
+  let (preconditions, envAfterPreconds) ← typeCheckConditions C envWithInputs
+                                            proc.spec.preconditions proc.header.name
+                                            (checkOldExprs := true)
+
+  -- Temporarily add returns into the context.
+  let (out_mty_sig, envWithOutputs) ← Lambda.LMonoTySignature.instantiate C
+                                        envAfterPreconds proc.header.typeArgs
+                                        proc.header.outputs |>.mapError errorWithSourceLoc
+  let out_lty_sig := Lambda.LMonoTySignature.toTrivialLTy out_mty_sig
+  let envWithOutputs := envWithOutputs.addToContext out_lty_sig
+
+  -- Type check postconditions.
+  let (postconditions, envAfterPostconds) ← typeCheckConditions C envWithOutputs
+                                              proc.spec.postconditions proc.header.name
+                                              (checkOldExprs := false)
+
+  -- Type check body.
+  -- Note that `Statement.typeCheck` already reports source locations in
+  -- error messages.
+  let (annotated_body, finalEnv) ← Statement.typeCheck C envAfterPostconds p (.some proc) proc.body
+
+  -- Remove formals and returns from the context -- they ought to be local to
+  -- the procedure body.
+  let finalEnv := finalEnv.popContext
+
+  -- Construct final result.
+  let finalPreconditions := Procedure.Spec.updateCheckExprs preconditions.toList proc.spec.preconditions
+  let finalPostconditions := Procedure.Spec.updateCheckExprs postconditions.toList proc.spec.postconditions
+  -- Type arguments are empty below because we've replaced polytypes with monotypes.
+  let new_hdr := { proc.header with typeArgs := [],
+                                    inputs := inp_mty_sig,
+                                    outputs := out_mty_sig }
+  let new_spec := { proc.spec with preconditions := finalPreconditions,
+                                   postconditions := finalPostconditions }
+  let new_proc := { proc with header := new_hdr, spec := new_spec, body := annotated_body }
+
+  return (new_proc, finalEnv)
 
 ---------------------------------------------------------------------
+
 end Procedure
 end Core