macaroon.lean

import tactic.core

structure cnf :=
(ands_of_ors_of_maybe_nots : list (list (name × bool × string)))

def cnf.false : cnf := ⟨[[]]⟩
def cnf.true : cnf := ⟨[]⟩
def cnf.and : cnf → cnf → cnf
| ⟨c₁⟩ ⟨c₂⟩ := ⟨c₁ ++ c₂⟩
def cnf.or : cnf → cnf → cnf
| ⟨c₁⟩ ⟨c₂⟩ := ⟨do a ← c₁, b ← c₂, [a ++ b]⟩
def cnf.new (n : name) (pos : bool) (s : string) : cnf :=
⟨[[(n, pos, s)]]⟩

instance : has_repr cnf :=
⟨λ ⟨m⟩, string.intercalate " ∧\n "
  ((λ x : list (name × bool × string),
    "(" ++ (string.intercalate " ∨ " $ x.map $ λ ⟨n, pos, s⟩,
        to_string n ++ (if pos then " = " else " ≠ ") ++ repr s)
        ++ ")")
    <$> m)⟩

section
  open tactic interactive interactive.types

  meta def cnfify_core (args : list expr) : expr → bool → tactic expr
  | e pos := do
    e ← whnf e transparency.all,
    match e with
    | `(%%e₁ ∧ %%e₂) := do
      a ← cnfify_core e₁ pos,
      b ← cnfify_core e₂ pos,
      return $ if pos then `(cnf.and %%a %%b) else `(cnf.or %%a %%b)
    | `(%%e₁ ∨ %%e₂) := do
      a ← cnfify_core e₁ pos,
      b ← cnfify_core e₂ pos,
      return $ if pos then `(cnf.or %%a %%b) else `(cnf.and %%a %%b)
    | `(%%e₁ → %%e₂) := do
      a ← cnfify_core e₁ (bnot pos),
      b ← cnfify_core e₂ pos,
      return $ if pos then `(cnf.or %%a %%b) else `(cnf.and %%a %%b)
    | `(%%e₁ ↔ %%e₂) := do
      a ← cnfify_core e₁ (bnot pos),
      b ← cnfify_core e₂ tt,
      c ← cnfify_core e₁ pos,
      d ← cnfify_core e₂ ff,
      return $ `(cnf.and (cnf.or %%a %%b) (cnf.or %%c %%d))
    | `(false) := return $ if pos then `(cnf.false) else `(cnf.true)
    | `(true) := return $ if pos then `(cnf.true) else `(cnf.false)
    | `(%%a = %%b) :=
      if a ∈ args then do
        type ← infer_type b,
        if type = `(string) then
          let n := a.local_pp_name in
          return `(cnf.new %%`(n) %%`(pos) %%b)
        else do
          pb <- to_string <$> pp b,
          pt <- to_string <$> pp type,
          fail $ "Expected string; found: " ++ pb ++ " of type " ++ pt
      else
        fail $ "Invalid variable; expected one of: "
          ++ string.intercalate ", " (args.map to_string)
          ++ "; found: " ++ a.local_pp_name.to_string
    | e := do
      pe <- to_string <$> pp e,
      fail $ "Unhandled proposition! " ++ pe
    end

  meta def tactic.interactive.cnfify (p : parse texpr) : tactic unit :=
  to_expr p >>= open_lambdas >>= λ ⟨args, e⟩, cnfify_core args e tt >>= exact
end

example (s : string) := by cnfify λ fn arg1,
  fn ∈ ["f", "g", s] ∧
  (fn = "f" → arg1 = "1")

example (n : nat) := let q := [1, n, 3].map to_string in by cnfify λ fn, fn ∈ q

example := by cnfify λ fn target message,
  -- we may send and receive messages
  fn ∈ ["send", "recv"] ∧
  -- if we send a message to alice, the message must be "Hello"
  (fn = "send" ∧ target = "alice" → message = "Hello") ∧
  -- we can only receive messages as bob;
  -- but cannot send messages to bob.
  (fn = "recv" → target = "bob")