fix: don't pollute other namespaces to avoid conflicts

Author: dranov

Veil/DSL/Action/Lang.lean

@@ -204,7 +204,7 @@ partial def expandDoElemVeil (stx : doSeqItem) : VeilM (Array doSeqItem) := do
     modify (·.push ⟨fr, typeStx.getD (<- `(_))⟩)
     expandDoElemVeil $ <- `(Term.doSeqItem|$id:ident := $fr)
   | `(Term.doSeqItem| $idts:term := *) =>
-    let some (id, ts) := idts.isApp? | throwErrorAt stx "wrong syntax for non-deterministic assignment {stx}"
+    let some (id, ts) := TSyntax.isApp? idts | throwErrorAt stx "wrong syntax for non-deterministic assignment {stx}"
     let typeStx ← (<- localSpecCtx.get) |>.spec.getStateComponentTypeStx (id.getId)
     let fr := mkIdent <| <- mkFreshUserName `fresh
     modify (·.push ⟨fr, typeStx.getD (<- `(_))⟩)
@@ -232,7 +232,7 @@ partial def expandDoElemVeil (stx : doSeqItem) : VeilM (Array doSeqItem) := do
       expandDoElemVeil $ <- withRef stx `(Term.doSeqItem| $base:ident := { $base with $suff:ident := $t })
   | `(Term.doSeqItem| $idts:term := $t:term) =>
     trace[veil.debug] "[expand assignment with args] {stx}"
-    let some (id, ts) := idts.isApp? | return #[stx]
+    let some (id, ts) := TSyntax.isApp? idts | return #[stx]
     let stx' <- withRef t `(term| $id[ $[$ts],* ↦ $t:term ])
     let stx <- withRef stx `(Term.doSeqItem| $id:ident := $stx')
     expandDoElemVeil stx

Veil/DSL/Check/InvariantManipulation.lean

@@ -64,8 +64,8 @@ def theoremSuggestionsForIndicators' (actIndicators invIndicators : List (Name 
 -- FIXME: enhance this function, and all related functions, by handling error better, avoiding repeating code, etc.
 def recoverInvariantsInTrStyle : CommandElabM Unit := do
   let (_, invChecks) ← getAllChecks
-  let actIndicators := (invChecks.map (fun (_, (act_name, ind_name)) => (act_name, ind_name))).toList.removeDuplicates
-  let invIndicators := (invChecks.map (fun ((inv_name, ind_name), _) => (inv_name, ind_name))).toList.removeDuplicates
+  let actIndicators := (invChecks.map (fun (_, (act_name, ind_name)) => (act_name, ind_name))).toList |> List.removeDuplicates
+  let invIndicators := (invChecks.map (fun ((inv_name, ind_name), _) => (inv_name, ind_name))).toList |> List.removeDuplicates
   let allTheorems ← theoremSuggestionsForIndicators' actIndicators invIndicators
   for (thmId, cmd) in allTheorems do
     -- if the `tr` theorem hasn't been proven yet, we can recover it from `wp`

Veil/DSL/Check/Main.lean

@@ -10,9 +10,6 @@ import Veil.DSL.Specification.SpecDef
 
 open Lean Elab Command Term Meta Lean.Parser Tactic.TryThis Lean.Core
 
-def Lean.MessageLog.containsSubStr (msgs : MessageLog) (substr : String) : CommandElabM Bool := do
-  msgs.toList.anyM (fun msg => return String.isSubStrOf substr (← msg.data.toString))
-
 namespace Veil
 
 inductive CheckStyle
@@ -228,10 +225,17 @@ def parseStrAsJson [Monad m] [MonadError m] (str : String) : m Json := do
   | .ok json => return json
   | .error err => throwError s!"could not parse {str} as Json: {err}"
 
+def MessageLog.containsSubStr (msgs : MessageLog) (substr : String) : CommandElabM Bool := do
+  msgs.toList.anyM (fun msg => return String.isSubStrOf substr (← msg.data.toString))
+
+def List.removeDuplicates [BEq α] (xs : List α) : List α :=
+  xs.foldl (init := []) fun acc x =>
+    if acc.contains x then acc else x :: acc
+
 def checkTheorems (stx : Syntax) (initChecks: Array (Name × Expr)) (invChecks: Array ((Name × Expr) × (Name × Expr))) (behaviour : CheckInvariantsBehaviour) :
   CommandElabM Unit := do
-  let actIndicators := (invChecks.map (fun (_, (act_name, ind_name)) => (act_name, ind_name))).toList.removeDuplicates
-  let invIndicators := (invChecks.map (fun ((inv_name, ind_name), _) => (inv_name, ind_name))).toList.removeDuplicates
+  let actIndicators := (invChecks.map (fun (_, (act_name, ind_name)) => (act_name, ind_name))).toList |> List.removeDuplicates
+  let invIndicators := (invChecks.map (fun ((inv_name, ind_name), _) => (inv_name, ind_name))).toList |> List.removeDuplicates
   let (vcStyle, _checkStyle, suggestionStyle) := behaviour
   let allTheorems ← theoremSuggestionsForIndicators (!initChecks.isEmpty) actIndicators invIndicators vcStyle
   match behaviour with
@@ -252,7 +256,7 @@ def checkTheorems (stx : Syntax) (initChecks: Array (Name × Expr)) (invChecks:
         -- The theorem is not proven; we need to figure out why:
         -- either solver returned `sat`, `unknown`, or there was an error
         let msgsTxt := String.intercalate "\n" (← msgs.toList.filterMapM (fun msg => if msg.severity == .error then msg.toString else pure none))
-        let (hasSat, hasUnknown, hasFailure) := (← msgs.containsSubStr Veil.SMT.satGoalStr, ← msgs.containsSubStr Veil.SMT.unknownGoalStr, ← msgs.containsSubStr Veil.SMT.failureGoalStr)
+        let (hasSat, hasUnknown, hasFailure) := (← MessageLog.containsSubStr msgs Veil.SMT.satGoalStr, ← MessageLog.containsSubStr msgs Veil.SMT.unknownGoalStr, ← MessageLog.containsSubStr msgs Veil.SMT.failureGoalStr)
         modelStr := if hasSat then .some $ (s!"{theoremId.theoremName}" ++ (getModelStr msgsTxt) ++ "\n") else .none
         pure $ match hasSat, hasUnknown, hasFailure with
         | true, false, false => SmtResult.Sat .none

Veil/DSL/Specification/ActionDef.lean

@@ -123,7 +123,7 @@ where
     | Mode.internal => do `(fun $funBinders* => do' .internal in $l)
     | Mode.external => do `(fun $funBinders* => do' .external in $l)
     let genExp <- withDeclName genName do elabTermAndSynthesize genl none
-    let ⟨genExp, _, _⟩ <- genExp.simpWp
+    let ⟨genExp, _, _⟩ <- simpWp genExp
     let genExp <- instantiateMVars <| <- mkLambdaFVarsImplicit vs genExp
     simpleAddDefn genName genExp (attr := #[{name := `generatorSimp}, {name := `actSimp}, {name := `reducible}])
     return (genName, genExp)
@@ -143,8 +143,8 @@ where
     | Mode.internal => baseName
     | Mode.external => toExtName baseName
     let genExp := Lean.mkConst genName
-    let act ← genExp |>.runUnfold (genName :: wpUnfold)
-    let ⟨act, _actPf, _⟩ <- act.simpAction
+    let act ← runUnfold genExp (genName :: wpUnfold)
+    let ⟨act, _actPf, _⟩ <- simpAction act
     let mut attr : Array Attribute := #[{name := `initSimp}, {name := `actSimp}]
     simpleAddDefn actName act (attr := attr) («type» := ← inferType genExp)
     return actName
@@ -183,9 +183,9 @@ where
     -- Here, to account for the case when the action is generated from a transition,
     -- we also unfold `Function.toWp` and the original definition of the transition.
     let origName := toOriginalName baseName
-    let act ← genExp |>.runUnfold (genName :: wpUnfold)
-    let act ← act |>.runUnfold [``Function.toWp, origName]
-    let ⟨act, actPf, _⟩ <- act.simpAction
+    let act ← runUnfold genExp (genName :: wpUnfold)
+    let act ← runUnfold act [``Function.toWp, origName]
+    let ⟨act, actPf, _⟩ <- simpAction act
     let mut attr : Array Attribute := #[{name := `actSimp}]
     simpleAddDefn actName act (attr := attr) («type» := ← inferType genExp)
     return (actName, actPf)
@@ -204,9 +204,9 @@ where
     -- transition that existentially quantifies over the state of the
     -- dependency, which is bad. Instead, we apply the `lift_transition`
     -- theorem, giving us a nicer lifted transition.
-    let ⟨actTr, _, _⟩ <- actTr.runSimp `(tactic| simp only [$(mkIdent `generatorSimp):ident, setIn, getFrom, lift_transition])
+    let ⟨actTr, _, _⟩ <- runSimp actTr `(tactic| simp only [$(mkIdent `generatorSimp):ident, setIn, getFrom, lift_transition])
     -- After (potentially) `lift_transition` theorem, we simplify as usual
-    let ⟨actTr, _, _⟩ <- actTr.simpAction
+    let ⟨actTr, _, _⟩ <- simpAction actTr
     let actTr <- mkLambdaFVarsImplicit vs actTr
     let actTr <- instantiateMVars actTr
     simpleAddDefn actTrName actTr (attr := #[{name := `actSimp}])
@@ -224,7 +224,7 @@ where
     let actTrStx <- `(fun st st' => exists? $br ?, (@$(mkIdent actEName) $sectionArgs* $args*).toTwoState st st')
     let trActThmStatement ← `(forall? $[$vd]* , ($actTrStx) = (@$(mkIdent actTrName) $sectionArgs*))
     let trActThm ← elabTermAndSynthesize trActThmStatement mkProp
-    let ⟨afterSimp, thmPf, _⟩ <- trActThm.simpAction
+    let ⟨afterSimp, thmPf, _⟩ <- simpAction trActThm
     if !afterSimp.isTrue then
       throwError "[genSoundness] {trActThmStatement} could not be proven by `simp`"
     let proof ← match thmPf with
@@ -268,9 +268,9 @@ where
   genProcedure (baseName : Name) (genIName : Name) := do
     let procName := baseName
     let genExp := Lean.mkConst genIName
-    let act ← genExp |>.runUnfold (genIName :: wpUnfold)
-    let act ← act |>.runUnfold [``Function.toWp]
-    let ⟨act, actPf, _⟩ <- act.simpAction
+    let act ← runUnfold genExp (genIName :: wpUnfold)
+    let act ← runUnfold act [``Function.toWp]
+    let ⟨act, actPf, _⟩ <- simpAction act
     let mut attr : Array Attribute := #[{name := `actSimp}]
     simpleAddDefn procName act (attr := attr) («type» := ← inferType genExp)
     return (procName, actPf)
@@ -345,7 +345,7 @@ where
     let liftedGenName := toGenName liftedActName mode
     trace[veil.info] "{liftedGenName} := {liftedGenStx}"
     let genExp <- withDeclName liftedGenName do elabTermAndSynthesize liftedGenStx .none
-    let ⟨genExp, _, _⟩ <- genExp.simpWp
+    let ⟨genExp, _, _⟩ <- simpWp genExp
     let genExp <- instantiateMVars <| <- mkLambdaFVarsImplicit actVs genExp
     let initAttr := if isInitialAction then #[{name := `initSimp}] else #[]
     simpleAddDefn liftedGenName genExp (attr := #[{name := `generatorSimp}, {name := `actSimp}, {name := `reducible}] ++ initAttr)

Veil/Util/DSL.lean

@@ -3,18 +3,15 @@ import Veil.Model.State
 import Veil.DSL.Internals.StateExtensions
 import Veil.DSL.Action.Theory
 
-def Lean.TSyntax.isApp? (stx : Term) : Option (Ident × Array Term) := do
+namespace Veil
+
+open Lean Elab Command Term Meta Lean.Parser
+
+def TSyntax.isApp? (stx : Term) : Option (Ident × Array Term) := do
   let #[f, args] := stx.raw.getArgs | failure
   let `(term| $f:ident) := f | failure
   return (⟨f⟩, args.getArgs.map (⟨·⟩))
 
-def List.removeDuplicates [BEq α] (xs : List α) : List α :=
-  xs.foldl (init := []) fun acc x =>
-    if acc.contains x then acc else x :: acc
-
-namespace Veil
-
-open Lean Elab Command Term Meta Lean.Parser
 
 def isTypeClassBinder : TSyntax `Lean.Parser.Term.bracketedBinder → Bool
   | `(bracketedBinder| $_:instBinder) => true

Veil/Util/Display.lean

@@ -87,8 +87,4 @@ def getModelStr (msg : String) : String :=
   | [model, _] => model
   | _ => resWithErr
 
-
-def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
-  { unreported := log.unreported.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false }
-
 end Veil

Veil/Util/Quantifiers.lean

@@ -70,7 +70,7 @@ private partial def isClassQuick? : Expr → MetaM (LOption Name)
       | _ => return .undef
     | _            => return .none
 
-def _root_.Lean.Expr.isExists (e : Expr) : Bool :=
+def isExists (e : Expr) : Bool :=
   match_expr e with
   | Exists _ _ => true
   | _          => false
@@ -146,7 +146,7 @@ mutual
           withNewLocalInstancesImp fvars j do
             if reducing then
               let newType ← whnf type
-              if newType.isExists then
+              if isExists newType then
                 process lctx fvars fvars.size newType
               else
                 k fvars type
@@ -156,7 +156,7 @@ mutual
 
   private partial def existsTelescopeReducingAux (type : Expr) (k : Array Expr → Expr → MetaM α) (cleanupAnnotations : Bool) : MetaM α := do
       let newType ← whnf type
-      if newType.isExists then
+      if isExists newType then
         existsTelescopeReducingAuxAux true newType k cleanupAnnotations
       else
         k #[] type

Veil/Util/TermSimp.lean

@@ -1,5 +1,8 @@
 import Lean
 
+
+namespace Veil
+
 /-
   This file provides facilities for running tactics on terms. In
   particular, it provides a version of `Tactic.run` that returns a
@@ -39,8 +42,8 @@ end Tactic
 
 def veilSimpMaxSteps := 10 * Lean.Meta.Simp.defaultMaxSteps
 
-open Lean.Elab Tactic Lean.Meta
-def Lean.Expr.runSimp (e : Expr) (stx : TermElabM (TSyntax `tactic)) : TermElabM Simp.Result := do
+open Lean Lean.Elab Tactic Lean.Meta
+def runSimp (e : Expr) (stx : TermElabM (TSyntax `tactic)) : TermElabM Simp.Result := do
   let stx ← stx
   let mv := (← mkFreshExprMVar e)
   let (res, [_l]) ← Tactic.run mv.mvarId! (do
@@ -52,15 +55,17 @@ def Lean.Expr.runSimp (e : Expr) (stx : TermElabM (TSyntax `tactic)) : TermElabM
   ) | throwError "[runSimp] expected exactly one goal after simplification"
   return res.1
 
-def Lean.Expr.simpWp (e : Expr) : TermElabM Simp.Result := do
+def simpWp (e : Expr) : TermElabM Simp.Result := do
   let stx := `(tactic| simp only [wpSimp])
-  e.runSimp stx
+  runSimp e stx
 
-def Lean.Expr.simpAction (e : Expr) : TermElabM Simp.Result := do
+def simpAction (e : Expr) : TermElabM Simp.Result := do
   let stx := `(tactic| simp only [actSimp, smtSimp, quantifierSimp])
-  e.runSimp stx
+  runSimp e stx
 
-def Lean.Expr.runUnfold (e : Expr) (defs : List Name) : TermElabM Expr := do
+def runUnfold (e : Expr) (defs : List Name) : TermElabM Expr := do
   let mut eu := e
   for name in defs do eu := (<- unfold eu name).expr
   return eu
+
+end Veil