nextgen-dependent-lcf.sml

signature THEORY =
sig
  type sort
  type term

  structure Var :
  sig
    include ORDERED
    val toString : t -> string
  end

  type var = Var.t

  structure Env : DICT where type key = var

  datatype closure = <: of term * closure Env.dict
  type env = closure Env.dict

  val fresh : unit -> var
  val var : var -> sort -> term
  val force : closure -> term
end

signature LCF =
sig
  structure Th : THEORY
  structure Tl : TELESCOPE
    where type Label.t = Th.var

  datatype 'a state = |> of 'a Tl.telescope * Th.term

  type 'a isjdg =
    {sort : 'a -> Th.sort,
     subst : Th.env -> 'a -> 'a}

  val map : ('a -> 'b) -> 'a state -> 'b state
  val ret : 'a isjdg -> 'a -> 'a state
  val mul : 'a isjdg -> 'a state state -> 'a state
end

signature LCF_UTIL =
sig
  include LCF

  type 'a tactic = 'a -> 'a state

  (* refine subgoals simultaneously *)
  val THEN : 'a isjdg -> 'a tactic * 'a tactic -> 'a tactic

  (* refine sequentially / one subgoal at a time to take advantage of substitutions *)
  val SEQ_THEN : 'a isjdg -> 'a tactic * 'a tactic -> 'a tactic
end

functor Lcf (Th : THEORY) : LCF =
struct
  structure Th = Th
  structure Tl = Telescope (Th.Var)

  datatype 'a state = |> of 'a Tl.telescope * Th.term
  infix |>

  type 'a isjdg =
    {sort : 'a -> Th.sort,
     subst : Th.env -> 'a -> 'a}

  fun map f (psi |> m) =
    Tl.map f psi |> m

  fun ret (kit : 'a isjdg) jdg =
    let
      val x = Th.fresh ()
    in
      Tl.singleton x jdg |> Th.var x (#sort kit jdg)
    end

  fun prepend psi (psi' |> ev) =
    Tl.append psi psi' |> ev

  structure MulMachine =
  struct
    open Th infix <:
    type 'a mul = 'a Tl.telescope * Th.closure * 'a state Tl.telescope

    fun init (psi |> ev) : 'a mul =
      (Tl.empty, ev <: Th.Env.empty, psi)

    datatype 'a step =
       UNLOAD of 'a state
     | STEP of 'a mul

    fun step (kit : 'a isjdg) ((psi, cl, ppsi) : 'a mul) =
      let
        open Tl.ConsView
        val ev <: env = cl
      in
        case out ppsi of
           EMPTY => UNLOAD (psi |> Th.force cl)
         | CONS (x, psix |> evx, ppsi') =>
             let
               val psix' = Tl.map (#subst kit env) psix
               val psi' = Tl.append psi psix'
               val env' = Th.Env.insert env x (evx <: env)
             in
               STEP (psi', ev <: env', ppsi')
             end
      end
  end

  fun mul kit =
    let
      open MulMachine
      fun go m =
        case step kit m of
           UNLOAD st => st
         | STEP m' => go m'
    in
      go o init
    end

end

functor LcfUtil (Lcf : LCF) : LCF_UTIL =
struct
  open Lcf

  infix |>

  fun bind (kit : 'b isjdg) (f : 'a -> 'b state) (st : 'a state) : 'b state =
    mul kit (map f st)

  type 'a tactic = 'a -> 'a state

  fun label (psi |> m) =
    Tl.foldr (fn (x, a, r) => Tl.cons x (x, a) r) Tl.empty psi |> m

  fun subgoals (psi |> m) =
    psi

  fun bindDict (kit : 'a isjdg) (fs : 'a tactic Th.Env.dict) (st : 'a state) : 'a state =
    bind kit (fn (x, a) => (Th.Env.lookup fs x handle _ => ret kit) a) (label st)

  fun focus (kit : 'a isjdg) (x : Th.var) (f : 'a -> 'a state) (st : 'a state) : 'a state =
    bindDict kit (Th.Env.insert Th.Env.empty x f) st

  (* "sequential" Kleisli extension: refine one subgoal, propagate the results, refine another subgoal, etc. *)
  fun seqBind (kit : 'a isjdg) (f : 'a tactic) (st : 'a state) : 'a state =
    let
      open Tl.ConsView
      fun go psi =
        case out psi of
           EMPTY => (fn st => st)
         | CONS (x, a, psi') => go psi' o focus kit x f
    in
      go (subgoals st) st
    end

  fun THEN kit (t1, t2) =
    bind kit t2 o t1

  fun SEQ_THEN kit (t1, t2) =
    seqBind kit t2 o t1
end