Unpolished tactics for extrinsic (Curry-style) lambda calculus

Tactic.hs

module Tactic where

import Data.List

-- https://totbwf.github.io/posts/tactic-haskell.html

data Type
  = Var Int
  | Arrow Type Type
  | Prod Type Type
  deriving (Eq, Show)

type Context = [Type]

type Goal = (Context, Type)

data Term
  = Ref Int
  | Lam Term
  | App Term Term
  | Pair Term Term
  | Fst Term
  | Snd Term
  | Goal Goal
  deriving Show

data Result
  = Term Term
  | Error String
  deriving Show

type Tactic = Goal -> Result

split :: Tactic
split (ctx, Prod a b) =
  Term $ Pair (Goal (ctx, a)) (Goal (ctx, b))
split _ = Error "split"

intro :: Tactic
intro (ctx, Arrow a b) =
  Term $ Lam (Goal (a:ctx, b))
intro _ = Error "intro"

assumption :: Tactic
assumption (ctx, a) =
  case elemIndex a ctx of
    Just x -> Term (Ref x)
    Nothing -> Error "assumption"

-- `singleGoal` tries to apply `tac` to every goal. If `tac` fails, it goes to
-- the next goal. If `tac` succeeds, it stops and returns the result. If `tac`
-- fails every goal or there are no goals, `singleGoal` fails.
singleGoal :: Tactic -> Term -> Result
singleGoal tac = go
  where
  go (Lam b) | Term b <- go b = Term (Lam b)
  go (App f a)
    | Term f <- go f = Term (App f a)
    | Term a <- go a = Term (App f a)
  go (Pair l r)
    | Term l <- go l = Term (Pair l r)
    | Term r <- go r = Term (Pair l r)
  go (Fst p) | Term p <- go p = Term (Fst p)
  go (Snd p) | Term p <- go p = Term (Snd p)
  go (Goal goal) = tac goal
  go _ = Error "single goal"

-- Because of how `singleGoal` works, `tac2` is not necessarily be applied to
-- the first goal `tac1` creates (if it creates any).
compose :: Tactic -> Tactic -> Tactic
compose tac1 tac2 goal =
  case tac1 goal of
    Term t -> singleGoal tac2 t
    err -> err

extract :: Result -> Term
extract (Term t) = t
extract (Error msg) = error msg

goal1 :: Goal
goal1 = ([], Arrow (Var 0) (Var 0))

term1 :: Term
term1 = extract $ compose intro assumption goal1

goal2 :: Goal
goal2 = ([Var 0], Prod (Var 0) (Var 0))

term2 :: Term
term2 = extract $ compose (compose split assumption) assumption goal2

goal3 :: Goal
goal3 = ([Var 0], Prod (Var 0) (Arrow (Var 1) (Var 1)))

-- Note the order the tactics are applied:
-- 1. `split` creates two goals
-- 2. `intro` introduces a variable in the second goal
-- 3. `assumption` closes the first goal
-- 4. `assumption` closes the second goal
term3 :: Term
term3 = extract $ compose (compose (compose split intro) assumption) assumption goal3