lcs.sml

signature LCS_SORT =
sig
  structure AtomicSort : SORT

  type atomic = AtomicSort.t

  datatype t =
      VAL of atomic
    | KONT of atomic * atomic
    | CMD of atomic

  val eq : t * t -> bool
  val toString : t -> string
end

signature KONT_OPERATOR =
sig
  include OPERATOR
  val input : 'i t -> Arity.Valence.sort
end

signature LCS_OPERATOR =
sig
  structure Sort : LCS_SORT

  structure Val : OPERATOR
  sharing type Val.Arity.Valence.Sort.t = Sort.AtomicSort.t

  structure Kont : KONT_OPERATOR
  sharing type Kont.Arity.Valence.Sort.t = Sort.AtomicSort.t
  sharing type Kont.Arity.Valence.Spine.t = Val.Arity.Valence.Spine.t

   datatype 'i cmd =
      RET of Sort.atomic
    | CUT of Sort.atomic * Sort.atomic

   datatype 'i operator =
      V of 'i Val.t
    | K of 'i Kont.t
    | C of 'i cmd

  include OPERATOR
    where type 'i t = 'i operator
    where type Arity.Valence.Sort.t = Sort.t
    where type 'a Arity.Valence.Spine.t = 'a Val.Arity.Valence.Spine.t
end

functor LcsSort (AtomicSort : SORT) : LCS_SORT =
struct
  structure AtomicSort = AtomicSort
  type atomic = AtomicSort.t

  datatype t =
     VAL of atomic
   | KONT of atomic * atomic
   | CMD of atomic

  val eq =
    fn (VAL sigma1, VAL sigma2) => AtomicSort.eq (sigma1, sigma2)
     | (KONT (sigma1, tau1) , KONT (sigma2, tau2)) => AtomicSort.eq (sigma1, sigma2) andalso AtomicSort.eq (tau1, tau2)
     | (CMD sigma1, CMD sigma2) => AtomicSort.eq (sigma1, sigma2)
     | _ => false

  val toString =
    fn VAL sigma => AtomicSort.toString sigma
     | KONT (sigma, tau) => "[" ^ AtomicSort.toString sigma ^ " > " ^ AtomicSort.toString tau ^ "]"
     | CMD sigma => "{" ^ AtomicSort.toString sigma ^ "}"
end

functor LcsOperator
  (structure Sort : LCS_SORT
   structure Val : OPERATOR where type 'a Arity.Valence.Spine.t = 'a list
   structure Kont : KONT_OPERATOR where type 'a Arity.Valence.Spine.t = 'a list
   sharing type Val.Arity.Valence.Sort.t = Sort.AtomicSort.t
   sharing type Kont.Arity.Valence.Sort.t = Sort.AtomicSort.t) : LCS_OPERATOR =
struct
  datatype 'i cmd =
     RET of Sort.atomic
   | CUT of Sort.atomic * Sort.atomic

  datatype 'i operator =
     V of 'i Val.t
   | K of 'i Kont.t
   | C of 'i cmd

  structure Sort = Sort and Val = Val and Kont = Kont
  structure Arity = ListArity (Sort)

  type 'i t = 'i operator
  type sort = Sort.t

  fun mapValence f ((sigmas, taus), tau) =
    ((List.map f sigmas, List.map f taus), f tau)

  val arity =
    fn V theta =>
         let
           val (vls, sigma) = Val.arity theta
         in
           (List.map (mapValence Sort.CMD) vls, Sort.VAL sigma)
         end
     | K theta =>
         let
           val sigma = Kont.input theta
           val (vls, tau) = Kont.arity theta
         in
           (List.map (mapValence Sort.CMD) vls, Sort.KONT (sigma, tau))
         end
     | C (RET sigma) => ([], Sort.VAL sigma)
     | C (CUT (sigma, tau)) =>
       ([(([],[]), Sort.KONT (sigma, tau)),
         (([],[]), Sort.CMD sigma)],
        Sort.CMD tau)

  val support =
    fn V theta => List.map (fn (u, sigma) => (u, Sort.VAL sigma)) (Val.support theta)
     | K theta => List.map (fn (u, sigma) => (u, Sort.VAL sigma)) (Kont.support theta)
     | C _ => []

  fun eq f =
    fn (V theta1, V theta2) => Val.eq f (theta1, theta2)
     | (K theta1, K theta2) => Kont.eq f (theta1, theta2)
     | (C (CUT (sigma1, tau1)), C (CUT (sigma2, tau2))) =>
         Sort.AtomicSort.eq (sigma1, sigma2)
           andalso Sort.AtomicSort.eq (tau1, tau2)
     | (C (RET sigma1), C (RET sigma2)) =>
        Sort.AtomicSort.eq (sigma1, sigma2)
     | _ => false

  fun toString f =
    fn V theta => Val.toString f theta
     | K theta => Kont.toString f theta
     | C (RET _) => "ret"
     | C (CUT _) => "cut"

  fun map f =
    fn V theta => V (Val.map f theta)
     | K theta => K (Kont.map f theta)
     | C (RET sigma) => C (RET sigma)
     | C (CUT (sigma, tau)) => C (CUT (sigma, tau))
end


signature LCS_PATTERN =
sig
  (* Commands *)
  datatype ('s, 'v, 'a) closure =
     RETURN of 'a
   | SUBST of ('v * ('s, 'v, 'a) closure) * ('s, 'v, 'a) closure
   | REN of ('s * 's) * ('s, 'v, 'a) closure

  (* A term pattern is an operator and a spine of abstractions *)
  datatype ('s, 'v, 'o, 't) pat = $ of 'o * ('s, 'v, 't) bpat list
  and ('s, 'v, 't) bpat = \ of ('s list * 'v list) * 't
end

structure LcsPattern :> LCS_PATTERN =
struct
  (* Instructions, with symbols in 's, variables in 'v, terms in 'a. *)
  datatype ('s, 'v, 'a) closure =
     RETURN of 'a
   | SUBST of ('v * ('s, 'v, 'a) closure) * ('s, 'v, 'a) closure
   | REN of ('s * 's) * ('s, 'v, 'a) closure

  (* A term pattern is an operator and a spine of abstractions *)
  datatype ('s, 'v, 'o, 't) pat = $ of 'o * ('s, 'v, 't) bpat list
  and ('s, 'v, 't) bpat = \ of ('s list * 'v list) * 't
end

signature LCS_DEFINTION =
sig
  structure O : LCS_OPERATOR
  structure P : LCS_PATTERN

  (* signature *)
  type sign

  type ('s, 'v, 't) value = ('s, 'v, 's O.Val.t, 't) P.pat
  type ('s, 'v, 't) kont = ('s, 'v, 's O.Kont.t, 't) P.pat

  val plug : ('s, 'v, 't) kont -> ('s, 'v, 't) value -> ('s, 'v, 't) P.closure
end

structure Sort : SORT =
struct
  type t = unit
  fun eq _ = true
  fun toString _ = "CMD"
end

structure Arity = ListArity (Sort)

structure LambdaVal =
struct
  structure Arity = Arity
  datatype 'i t = LAM | AX | PAIR

  val arity =
    fn LAM => ([(([],[]), ())], ())
     | PAIR => ([(([],[]), ()), (([],[]), ())], ())
     | AX => ([], ())

  fun support _ = []

  fun eq _ =
    fn (LAM, LAM) => true
     | (PAIR, PAIR) => true
     | (AX, AX) => true
     | _ => false

  fun toString _ =
    fn LAM => "lam"
     | PAIR => "pair"
     | AX => "ax"

  fun map f =
    fn LAM => LAM
     | PAIR => PAIR
     | AX => AX
end

structure LambdaKont =
struct
  structure Arity = Arity
  datatype 'i t = AP | SPREAD

  val arity =
    fn AP => ([(([],[]), ())], ())
     | SPREAD => ([(([], [(),()]), ())], ())

  val input =
    fn AP => ()
     | SPREAD => ()

  fun support _ = []

  fun eq _ =
    fn (AP, AP) => true
     | (SPREAD, SPREAD) => true
     | _ => false

  fun toString _ =
    fn AP => "ap"
     | SPREAD => "spread"

  fun map _ =
    fn AP => AP
     | SPREAD => SPREAD
end


structure LambdaSort = LcsSort (Sort)
structure LambdaOperator = LcsOperator (structure Sort = LambdaSort and Val = LambdaVal and Kont = LambdaKont)

structure LambdaLcs : LCS_DEFINTION =
struct
  structure O = LambdaOperator and P = LcsPattern
  type sign = unit

  open P O

  type ('s, 'v, 't) value = ('s, 'v, 's O.Val.t, 't) P.pat
  type ('s, 'v, 't) kont = ('s, 'v, 's O.Kont.t, 't) P.pat

  infix $ \

  nonfix ^
  val ^ = RETURN

  fun plug (LAM $ [(_, [x]) \ mx]) (AP $ [_ \ n]) =
       SUBST ((x, ^ n), ^ mx)
    | plug (PAIR $ [_ \ m1, _ \ m2]) (SPREAD $ [(_, [x,y]) \ nxy]) =
       SUBST ((x, ^ m1), SUBST ((y, ^ m2), ^ nxy))
    | plug _ _ = raise Match

end