open-operators.sml

signature OPERATIONS =
sig
  type 'a t
  val default : unit -> 'a t
  val enrich : ('b -> 'a option) -> 'b t * 'a t -> 'b t
end

structure UnitOperations : OPERATIONS =
struct
  type 'a t = unit
  fun default () = ()
  fun enrich _ _ = ()
end

functor OperationsProduct
  (structure Left : OPERATIONS
   structure Right : OPERATIONS) : OPERATIONS =
struct
  type 'a t = 'a Left.t * 'a Right.t

  fun default () =
    (Left.default (), Right.default ())

  fun enrich project ((fallbackLeft, fallbackRight), (left, right)) =
    (Left.enrich project (fallbackLeft, left),
     Right.enrich project (fallbackRight, right))
end


signature OPEN =
sig
  type t
  structure Operations : OPERATIONS
  val embed : 'a Operations.t -> ('a -> t) * (t -> 'a option)
  val operations : unit -> t Operations.t
end

functor EnrichOpen (structure Open : OPEN and Operations : OPERATIONS) : OPEN =
struct
  type t = Open.t

  structure Left = Open.Operations
  structure Right = Operations

  structure Operations = OperationsProduct
    (structure Left = Left and Right = Right)

  val operationsRef : t Operations.t ref = ref (Operations.default ())

  fun operations () = ! operationsRef

  fun embed (operation : 'a Operations.t) =
    let
      val (inject, project) = Open.embed (Left.default ())
      val fallback = !operationsRef
    in
      operationsRef := Operations.enrich project (!operationsRef, operation);
      (inject, project)
    end
end

structure UnitOpen :> OPEN where type 'a Operations.t = unit =
struct
  type t = exn
  structure Operations = UnitOperations

  fun operations () = ()

  fun 'a embed () =
   let
     exception E of 'a
     fun project (e : t) : 'a option =
       case e of
           E a => SOME a
         | _ => NONE
   in
     (E, project)
   end
end

structure OperatorOperations : OPERATIONS =
struct
  type 'a t =
    {toString : 'a -> string,
     eq : 'a * 'a -> bool,
     arity : 'a -> Arity.t}

  exception Unregistered

  fun default () =
    {toString = fn _ => raise Unregistered,
     eq = fn _ => raise Unregistered,
     arity = fn _ => raise Unregistered}

  fun enrich project (fallback : 'b t, operation : 'a t) =
    {toString =
       (fn theta =>
         case project theta of
              SOME a => #toString operation a
            | NONE => #toString fallback theta),
     eq =
       (fn (theta, theta') =>
         case (project theta, project theta') of
              (SOME a, SOME a') => #eq operation (a, a')
            | (NONE, NONE) => #eq fallback (theta, theta')
            | _ => false),
     arity =
       (fn theta =>
         case project theta of
              SOME a => #arity operation a
            | NONE => #arity fallback theta) }
end


structure OperatorOpen = EnrichOpen
  (structure Open = UnitOpen and Operations = OperatorOperations)

structure UniversalOperator : OPERATOR =
struct
  type t = OperatorOpen.t

  val operations = #2 o OperatorOpen.operations

  fun eq (theta, theta') = #eq (operations ()) (theta, theta')
  fun arity theta = #arity (operations ()) theta
  fun toString theta = #toString (operations ()) theta
end

signature INJECTION =
sig
  type t
  type ambient

  (* inject a [t] into [ambient] *)
  val `> : t -> ambient

  exception Mismatch

  (* project an [ambient] into [t], possibly raising [Mismatch] *)
  val `< : ambient -> t
end

functor OperatorInjection (O : OPERATOR) : INJECTION =
struct
  type ambient = OperatorOpen.t
  exception Mismatch
  open O

  local
    val operations = {toString = toString, eq = eq, arity = arity}
    val (inject : t -> ambient, project) = OperatorOpen.embed ((), operations)
  in
    val `> = inject
    fun `< t =
      case project t of
           SOME a => a
         | NONE => raise Mismatch
  end
end

structure Nat =
struct
  datatype t = ZE | SUCC

  val eq : t * t -> bool = op=
  fun toString ZE = "ze"
    | toString SUCC = "succ"
  fun arity ZE = #[]
    | arity SUCC = #[0]
end

structure Lam =
struct
  datatype t = LAM | AP
  val eq : t * t -> bool = op=
  fun toString LAM = "λ"
    | toString AP = "ap"
  fun arity LAM = #[1]
    | arity AP = #[0,0]
end

structure NatInj = OperatorInjection (Nat)
structure LamInj = OperatorInjection (Lam)

structure Test =
struct
  structure Abt = AbtUtil(Abt(structure Operator = UniversalOperator and Variable = StringVariable))
  structure N = NatInj and L = LamInj
  open Nat Lam Abt
  infix $ $$ \ \\

  val test =
    L.`> LAM $$ #["x" \\ (N.`> ZE $$ #[])]

  val _ = print (toString test^ "\n")
end