Add unified options for Velvet (#21)

* add a file with Loom options

* use options info for sematics and solver control

* refactor Velvet case studies for new options

Author: volodeyka

CaseStudies/Velvet/Std.lean

@@ -7,14 +7,12 @@ import Mathlib.Algebra.Ring.Int.Defs
 
 import Loom.MonadAlgebras.NonDetT.Extract
 import Loom.MonadAlgebras.WP.Tactic
+import Loom.MonadAlgebras.WP.Options
 import Loom.MonadAlgebras.WP.DoNames'
 
 import CaseStudies.Extension
 import CaseStudies.Velvet.Syntax
 
-macro_rules
-  | `(tactic|loom_solver) =>
-    `(tactic|try grind (splits := 20))
 
 macro_rules
   | `(doElem|$id:ident[$idx:term] := $val:term) =>

CaseStudies/Velvet/Syntax.lean

@@ -270,7 +270,10 @@ elab_rules : command
       for mutType in mutTypes do
         mutTypeProd <- `($mutType × $mutTypeProd)
       retType <- `($retType × $mutTypeProd)
+    /- We need Velvet methods to be elaborated in a modified `do`-notation.
+      For that we localy open the `DoNames` namespace which contains the extensioned `do`-notation. -/
     let defCmd <- `(command|
+      open Lean.Elab.Term.DoNames in
       set_option linter.unusedVariables false in
       def $name $bindersIdents* : VelvetM $retType:term := do $mods* $doSeq*
       $suf:suffix)
@@ -340,6 +343,37 @@ elab_rules : command
         $pre
         ($name $ids*)
         (fun $ret => $post) := by $proofSeq $suf:suffix)
+    let opts <- getOptions
+
+    /- We need to check the termination and choice semantics options before
+      stating the proof. -/
+    if opts.getString (defVal := "unspecified") `loom.semantics.choice = "unspecified" then
+      throwError "First, you need to specify the choice semantics using `set_option loom.semantics.choice <demonic/angelic>`"
+
+    if opts.getString (defVal := "unspecified") `loom.semantics.termination = "unspecified" then
+      throwError "First, you need to specify the termination semantics using `set_option loom.semantics.termination <partial/total>`"
+
+    /- Now, depending on the solver option, we will locally define the `loom_solver` tactic. -/
+    let solver := opts.getString (defVal := "grind") `loom.solver
+    let thmCmd <- match solver with
+      | "grind" =>
+        /- In case of `grind` solver, we need  to fetch the number of splits from the options first. -/
+        let splits := Lean.Syntax.mkNatLit <| (opts.getNat (defVal := 20) `loom.solver.grind.splits)
+        `(command|
+          macro_rules | `(tactic| loom_solver) => do `(tactic| try grind (splits := $splits)) in
+          $thmCmd)
+      | "custom" => pure thmCmd
+      | _ =>
+        /- This is the case of `cvc5` or `z3` solver. We also need to fetch the timeout from the options. -/
+        let timeout := Syntax.mkNatLit <| (opts.getNat (defVal := 1) `loom.solver.smt.timeout)
+        let solver := Syntax.mkStrLit <| (opts.getString (defVal := "cvc5") `loom.solver.smt.solver)
+        `(command|
+          set_option auto.smt.trust true in
+          set_option auto.smt true in
+          set_option auto.smt.solver.name $solver in
+          set_option auto.smt.timeout $timeout in
+          macro_rules | `(tactic| loom_solver) => do `(tactic| loom_auto) in
+          $thmCmd)
     trace[Loom] "{thmCmd}"
     Command.elabCommand thmCmd
     velvetObligations.modify (·.erase name.getId)

CaseStudies/Velvet/VelvetExamples/EncodeDecodeStr.lean

@@ -7,8 +7,10 @@ import Loom.MonadAlgebras.WP.DoNames'
 import CaseStudies.Velvet.Std
 import CaseStudies.TestingUtil
 
-open PartialCorrectness DemonicChoice Lean.Elab.Term.DoNames
+set_option loom.semantics.termination "partial"
+set_option loom.semantics.choice "demonic"
 
+open PartialCorrectness DemonicChoice
 section RunLengthEncoding
 
 structure Encoding where
@@ -60,7 +62,6 @@ method decodeStr' (encoded_str: Array Encoding)
             i := i + 1
        return decoded
 
-
 prove_correct decodeStr' by
   loom_solve
   · simp[*] at *

CaseStudies/Velvet/VelvetExamples/Examples.lean

@@ -11,7 +11,8 @@ import Loom.MonadAlgebras.WP.DoNames'
 import CaseStudies.Velvet.Std
 import CaseStudies.TestingUtil
 
-open PartialCorrectness DemonicChoice Lean.Elab.Term.DoNames
+set_option loom.semantics.termination "partial"
+set_option loom.semantics.choice "demonic"
 
 section insertionSort
 

CaseStudies/Velvet/VelvetExamples/Examples_Total.lean

@@ -10,7 +10,8 @@ import Loom.MonadAlgebras.WP.DoNames'
 
 import CaseStudies.Velvet.Std
 
-open TotalCorrectness DemonicChoice Lean.Elab.Term.DoNames
+set_option loom.semantics.termination "total"
+set_option loom.semantics.choice "demonic"
 
 attribute [grind] Array.multiset_swap
 

CaseStudies/Velvet/VelvetExamples/GCD.lean

@@ -8,7 +8,8 @@ import Loom.MonadAlgebras.WP.DoNames'
 import CaseStudies.Velvet.Std
 import CaseStudies.TestingUtil
 
-open TotalCorrectness DemonicChoice Lean.Elab.Term.DoNames
+set_option loom.semantics.termination "total"
+set_option loom.semantics.choice "demonic"
 
 -- The Euclidean algorithm for GCD is a classic example of a function requiring
 -- explicit termination measures due to the modulo operation

CaseStudies/Velvet/VelvetExamples/IsSorted.lean

@@ -7,7 +7,8 @@ import Loom.MonadAlgebras.WP.DoNames'
 import CaseStudies.Velvet.Std
 import CaseStudies.TestingUtil
 
-open PartialCorrectness DemonicChoice Lean.Elab.Term.DoNames
+set_option loom.semantics.termination "partial"
+set_option loom.semantics.choice "demonic"
 
 
 method IsSorted(a: Array Int) return (sorted: Bool)

CaseStudies/Velvet/VelvetExamples/MaxElem.lean

@@ -7,7 +7,8 @@ import Loom.MonadAlgebras.WP.DoNames'
 import CaseStudies.Velvet.Std
 import CaseStudies.TestingUtil
 
-open PartialCorrectness DemonicChoice Lean.Elab.Term.DoNames
+set_option loom.semantics.termination "partial"
+set_option loom.semantics.choice "demonic"
 
 section MaxElem
 
@@ -36,7 +37,6 @@ method maxElem (arr: Array Int) return (res: Int)
     return mx
 
 prove_correct maxElem by
-  unfold isMax
   loom_solve
 
 end MaxElem

CaseStudies/Velvet/VelvetExamples/Recursion.lean

@@ -11,7 +11,8 @@ import Loom.MonadAlgebras.WP.DoNames'
 import CaseStudies.Velvet.Std
 import CaseStudies.TestingUtil
 
-open TotalCorrectness DemonicChoice Lean.Elab.Term.DoNames
+set_option loom.semantics.termination "total"
+set_option loom.semantics.choice "demonic"
 
 method simple_recursion (x : Nat) return (res: Nat)
   require True

CaseStudies/Velvet/VelvetExamples/SpMSpV_Example.lean

@@ -11,14 +11,15 @@ import Loom.MonadAlgebras.WP.DoNames'
 
 import CaseStudies.Velvet.Std
 
-open PartialCorrectness DemonicChoice Lean.Elab.Term.DoNames
 
 set_option auto.smt.trust true
 set_option auto.smt true
---try increasing this parameter if verification fails
 set_option auto.smt.timeout 4
 set_option auto.smt.solver.name "cvc5"
 
+set_option loom.semantics.termination "partial"
+set_option loom.semantics.choice "demonic"
+
 
 attribute [solverHint] Array.get_set_c
 section SpMV