Check.lean

/-
Copyright (c) 2021 Jannis Limperg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jannis Limperg
-/

import Lean.Data.Options

open Lean

namespace Aesop

initialize Check.all : Lean.Option Bool ←
  Option.register `aesop.check.all
    { defValue := false
      descr := "(aesop) Enable all runtime checks. Individual checks can still be disabled."
      group := "tactic" }

structure Check where
  toOption : Lean.Option Bool

namespace Check

def get (opts : Options) (opt : Check) : Bool :=
  if let some val := opt.toOption.get? opts then
    val
  else
    Check.all.get opts

def isEnabled [Monad m] [MonadOptions m] (opt : Check) : m Bool :=
  return opt.get (← getOptions)

def name (opt : Check) : Name :=
  opt.toOption.name

end Check

-- Inspired by `Lean.Data.Options`.
local macro "register_aesop_check_option" optName:ident descr:str : command =>
  `(initialize option : Lean.Option Bool ←
      Lean.Option.register $(quote $ `aesop.check ++ optName.getId)
        { defValue := false, descr := $descr, group := "tactic" }

    def $(mkIdent $ `Check ++ optName.getId) : Aesop.Check := ⟨option⟩)

register_aesop_check_option proofReconstruction
    "(aesop) Typecheck partial proof terms during proof reconstruction."

register_aesop_check_option tree
    "(aesop) Check search tree invariants after every iteration of the search loop. Quite expensive."

register_aesop_check_option rules
    "(aesop) Check that information reported by rules is correct."

register_aesop_check_option script
    "(aesop) Check that the tactic script generated by Aesop proves the goal. When this check is active, Aesop generates a tactic script even if the user did not request one."

register_aesop_check_option script.steps
    "(aesop) Check each step of the tactic script generated by Aesop. When this check is active, Aesop generates a tactic script even if the user did not request one."

end Aesop