structure ILSplit =
   struct

      type variable = Variable.variable

      datatype kind =
         Ktype
       | Ksing of con
       | Kpi of variable * kind * kind
       | Ksigma of variable * kind * kind

      and con =
         Cvar of variable
       | Clam of variable * kind * con
       | Capp of con * con
       | Cpair of con * con
       | Cpi1 of con
       | Cpi2 of con
       | Carrow of con * con
       | Cforall of variable * kind * con

      datatype term =
         Tvar of variable

       | Tlam of variable * con * term
       | Tapp of term * term

       | Tplam of variable * kind * term
       | Tpapp of term * con

   end


signature OPS_SPLIT =
   sig

      type variable = Variable.variable
      type kind
      type con
      type term

      val Ktype   : kind
      val Ksing   : con -> kind
      val Kpi     : variable * kind * kind -> kind
      val Ksigma  : variable * kind * kind -> kind

      val Cvar    : variable -> con
      val Clam    : variable * kind * con -> con
      val Capp    : con * con -> con
      val Cpair   : con * con -> con
      val Cpi1    : con -> con
      val Cpi2    : con -> con
      val Carrow  : con * con -> con
      val Cforall : variable * kind * con -> con

      val Tvar    : variable -> term
      val Tlam    : variable * con * term -> term
      val Tapp    : term * term -> term
      val Tplam   : variable * kind * term -> term
      val Tpapp   : term * con -> term

      val destKtype   : kind -> bool
      val destKsing   : kind -> con option
      val destKpi     : kind -> (variable * kind * kind) option
      val destKsigma  : kind -> (variable * kind * kind) option

      val destCarrow  : con -> (con * con) option
      val destCforall : con -> (variable * kind * con) option

   end


structure OpsSplit 
   :
   OPS_SPLIT
   =
   struct
      open ILSplit

      fun destKtype k =
          (case k of
              Ktype => true
            | _ => false)

      fun destKsing k =
          (case k of
              Ksing x => SOME x
            | _ => NONE)

      fun destKpi k =
          (case k of
              Kpi x => SOME x
            | _ => NONE)

      fun destKsigma k =
          (case k of
              Ksigma x => SOME x
            | _ => NONE)

      fun destCarrow c =
         (case c of
             Carrow x => SOME x
           | _ => NONE)

      fun destCforall c =
         (case c of
             Cforall x => SOME x
           | _ => NONE)

   end



signature PASS_SPLIT =
   sig

      type variable = Variable.variable
      type kind
      type con
      type term

      type kindresult
      type conresult
      type termresult

      type self

      val caseKtype   : self -> unit -> kindresult
      val caseKsing   : self -> con -> kindresult
      val caseKpi     : self -> variable * kind * kind -> kindresult
      val caseKsigma  : self -> variable * kind * kind -> kindresult

      val caseCvar    : self -> variable -> conresult
      val caseClam    : self -> variable * kind * con -> conresult
      val caseCapp    : self -> con * con -> conresult
      val caseCpair   : self -> con * con -> conresult
      val caseCpi1    : self -> con -> conresult
      val caseCpi2    : self -> con -> conresult
      val caseCarrow  : self -> con * con -> conresult
      val caseCforall : self -> variable * kind * con -> conresult

      val caseTvar    : self -> variable -> termresult
      val caseTlam    : self -> variable * con * term -> termresult
      val caseTapp    : self -> term * term -> termresult
      val caseTplam   : self -> variable * kind * term -> termresult
      val caseTpapp   : self -> term * con -> termresult

   end


signature TRAVERSE_SPLIT =
   sig

      type kind
      type con
      type term

      type kindresult
      type conresult
      type termresult

      val traverseKind : kind -> kindresult
      val traverseCon : con -> conresult
      val traverseTerm : term -> termresult

   end


functor SelfSplit (structure Ops : OPS_SPLIT
                   type kindresult
                   type conresult
                   type termresult)
   :
   sig
      type self
      val kself : self -> Ops.kind -> kindresult
      val cself : self -> Ops.con -> conresult
      val tself : self -> Ops.term -> termresult
   end
   =
   struct

      type self = { kself : Ops.kind -> kindresult,
                    cself : Ops.con -> conresult,
                    tself : Ops.term -> termresult }

      fun kself ({kself=f, ...}:self) = f
      fun cself ({cself=f, ...}:self) = f
      fun tself ({tself=f, ...}:self) = f

   end


functor TraverseSplit 
   (structure Pass : PASS_SPLIT 
                     where type kind = ILSplit.kind
                     where type con = ILSplit.con
                     where type term = ILSplit.term
    val mkself : { kself : Pass.kind -> Pass.kindresult,
                   cself : Pass.con -> Pass.conresult,
                   tself : Pass.term -> Pass.termresult } -> Pass.self) 
   :
   TRAVERSE_SPLIT
   =
   struct

      open Pass
      open ILSplit

      fun traverseKind k =
          let val self = mkself { kself = traverseKind,
                                  cself = traverseCon,
                                  tself = traverseTerm }
          in
             (case k of
                 Ktype => 
                    caseKtype self ()
               | Ksing x => 
                    caseKsing self x
               | Kpi x => 
                    caseKpi self x
               | Ksigma x => 
                    caseKsigma self x)
          end

      and traverseCon c =
          let val self = mkself { kself = traverseKind,
                                  cself = traverseCon,
                                  tself = traverseTerm }
          in
             (case c of
                 Cvar x =>
                    caseCvar self x
               | Clam x =>
                    caseClam self x
               | Capp x =>
                    caseCapp self x
               | Cpair x =>
                    caseCpair self x
               | Cpi1 x =>
                    caseCpi1 self x
               | Cpi2 x =>
                    caseCpi2 self x
               | Carrow x =>
                    caseCarrow self x
               | Cforall x =>
                    caseCforall self x)
          end

      and traverseTerm t =
          let val self = mkself { kself = traverseKind,
                                  cself = traverseCon,
                                  tself = traverseTerm }
          in
             (case t of
                 Tvar x =>
                    caseTvar self x
               | Tlam x =>
                    caseTlam self x
               | Tapp x =>
                    caseTapp self x
               | Tplam x =>
                    caseTplam self x
               | Tpapp x =>
                    caseTpapp self x)
          end

   end


functor IdPassSplit
   (type arg
    structure Src : OPS_SPLIT
    structure Dst : OPS_SPLIT
    structure Self :
       sig
          type self
          val kself : self -> Src.kind -> arg -> Dst.kind
          val cself : self -> Src.con -> arg -> Dst.con
          val tself : self -> Src.term -> arg -> Dst.term
       end)
   :
   PASS_SPLIT
   =
   struct

      type variable = Variable.variable
      type kind = Src.kind
      type con = Src.con
      type term = Src.term

      type kindresult = arg -> Dst.kind
      type conresult = arg -> Dst.con
      type termresult = arg -> Dst.term

      open Self

      fun caseKbind f self (v, k1, k2) arg =
          f (v, kself self k1 arg, kself self k2 arg)

      fun caseKtype _ () _ = 
          Dst.Ktype

      fun caseKsing self c arg = 
          Dst.Ksing (cself self c arg)

      val caseKpi = caseKbind Dst.Kpi
      val caseKsigma = caseKbind Dst.Ksigma

      fun caseCbind f self (v, k, c) arg =
          f (v, kself self k arg, cself self c arg)
             
      fun caseC1 f self c arg =
          f (cself self c arg)

      fun caseC2 f self (c1, c2) arg =
          f (cself self c1 arg, cself self c2 arg)

      fun caseCvar _ v _ = Dst.Cvar v

      val caseClam = caseCbind Dst.Clam
      val caseCapp = caseC2 Dst.Capp
      val caseCpair = caseC2 Dst.Cpair
      val caseCpi1 = caseC1 Dst.Cpi1
      val caseCpi2 = caseC1 Dst.Cpi2

      fun caseCarrow self (c1, c2) arg =
          Dst.Carrow (cself self c1 arg, cself self c2 arg)

      fun caseCforall self (v, k, c) arg =
          Dst.Cforall (v, kself self k arg, cself self c arg)


      fun caseTvar _ v _ = Dst.Tvar v

      fun caseTlam self (v, c, t) arg =
          Dst.Tlam (v, cself self c arg, tself self t arg)

      fun caseTapp self (t1, t2) arg =
          Dst.Tapp (tself self t1 arg, tself self t2 arg)

      fun caseTplam self (v, k, t) arg =
          Dst.Tplam (v, kself self k arg, tself self t arg)

      fun caseTpapp self (t, c) arg =
          Dst.Tpapp (tself self t arg, cself self c arg)

   end


functor SubstPassSplit
   (structure Ops : OPS_SPLIT
    structure Self :
       sig
          type self
          val kself : self -> Ops.kind -> Ops.con Variable.map -> Ops.kind
          val cself : self -> Ops.con -> Ops.con Variable.map -> Ops.con
          val tself : self -> Ops.term -> Ops.con Variable.map -> Ops.term
       end)
   :
   PASS_SPLIT
   =
   struct

      open Ops

      structure Super = 
         IdPassSplit (type arg = Ops.con Variable.map
                      structure Src = Ops
                      structure Dst = Ops
                      structure Self = Self)
         
      open Super  (* Inherit cases. *)

      fun caseKbind f self (v, k1, k2) s =
          let val v' = Variable.newvar ()
          in
             f (v', Self.kself self k1 s, Self.kself self k2 (Variable.extend s v (Cvar v')))
          end 

      val caseKpi = caseKbind Kpi
      val caseKsigma = caseKbind Ksigma

      fun caseCvar _ v s =
          (case Variable.find s v of
              NONE =>
                 Cvar v
            | SOME c =>
                 c)

      fun caseCbind f self (v, k, c) s =
          let val v' = Variable.newvar ()
          in
             f (v', Self.kself self k s, Self.cself self c (Variable.extend s v (Cvar v')))
          end 

      val caseClam = caseCbind Clam
      val caseCforall = caseCbind Cforall

      fun caseTplam self (v, k, t) s =
          let val v' = Variable.newvar ()
          in
             Tplam (v', Self.kself self k s, Self.tself self t (Variable.extend s v (Cvar v')))
          end

   end


signature SUBST_SPLIT =
   sig

      type kind
      type con
      type term

      val ksubst : con Variable.map -> kind -> kind
      val csubst : con Variable.map -> con -> con
      val tsubst : con Variable.map -> term -> term
        
      val ksubst1 : con -> Variable.variable -> kind -> kind
      val csubst1 : con -> Variable.variable -> con -> con
      val tsubst1 : con -> Variable.variable -> term -> term

      val krename : Variable.variable -> Variable.variable -> kind -> kind
      val crename : Variable.variable -> Variable.variable -> con -> con
      val trename : Variable.variable -> Variable.variable -> term -> term

   end


functor SubstSplitFun
   (structure Ops : OPS_SPLIT
    structure Traverse : TRAVERSE_SPLIT
                         where type kind = Ops.kind
                         where type con = Ops.con
                         where type term = Ops.term
                         where type kindresult = Ops.con Variable.map -> Ops.kind
                         where type conresult = Ops.con Variable.map -> Ops.con
                         where type termresult = Ops.con Variable.map -> Ops.term)
   :
   SUBST_SPLIT
   =
   struct

      type kind = Ops.kind
      type con = Ops.con
      type term = Ops.term

      fun ksubst s k = Traverse.traverseKind k s
      fun csubst s c = Traverse.traverseCon c s
      fun tsubst s t = Traverse.traverseTerm t s

      fun ksubst1 c v k = ksubst (Variable.extend Variable.null v c) k
      fun csubst1 c1 v c2 = csubst (Variable.extend Variable.null v c1) c2
      fun tsubst1 c v t = tsubst (Variable.extend Variable.null v c) t

      fun krename v' v k = ksubst1 (Ops.Cvar v') v k
      fun crename v' v c = csubst1 (Ops.Cvar v') v c
      fun trename v' v t = tsubst1 (Ops.Cvar v') v t

   end


local
   structure Self = SelfSplit (structure Ops = OpsSplit
                               type kindresult = ILSplit.con Variable.map -> ILSplit.kind
                               type conresult = ILSplit.con Variable.map -> ILSplit.con
                               type termresult = ILSplit.con Variable.map -> ILSplit.term)
   structure Pass = SubstPassSplit (structure Ops = OpsSplit
                                    structure Self = Self)
   structure Traverse = TraverseSplit (structure Pass = Pass
                                       fun mkself x = x)
in
   structure SubstSplit = SubstSplitFun (structure Ops = OpsSplit
                                         structure Traverse = Traverse)
end


structure ILDirect =
   struct

      type variable = Variable.variable

      datatype kind =
         Ktype
       | Karrow of kind * kind
       | Kprod of kind * kind

      datatype con =
         Cvar of variable
       | Clam of variable * kind * con
       | Capp of con * con
       | Cpair of con * con
       | Cpi1 of con
       | Cpi2 of con
       | Carrow of con * con
       | Cforall of variable * kind * con

      datatype term =
         Tvar of variable

       | Tlam of variable * con * term
       | Tapp of term * term

       | Tplam of variable * kind * term
       | Tpapp of term * con

   end


signature OPS_DIRECT =
   sig

      type variable = Variable.variable
      type kind
      type con
      type term

      val Ktype   : kind
      val Karrow  : kind * kind -> kind
      val Kprod   : kind * kind -> kind

      val Cvar    : variable -> con
      val Clam    : variable * kind * con -> con
      val Capp    : con * con -> con
      val Cpair   : con * con -> con
      val Cpi1    : con -> con
      val Cpi2    : con -> con
      val Carrow  : con * con -> con
      val Cforall : variable * kind * con -> con

      val Tvar    : variable -> term
      val Tlam    : variable * con * term -> term
      val Tapp    : term * term -> term
      val Tplam   : variable * kind * term -> term
      val Tpapp   : term * con -> term

      val destKtype   : kind -> bool
      val destKarrow  : kind -> (kind * kind) option
      val destKprod   : kind -> (kind * kind) option

      val destCvar    : con -> variable option
      val destClam    : con -> (variable * kind * con) option
      val destCapp    : con -> (con * con) option
      val destCpair   : con -> (con * con) option
      val destCpi1    : con -> con option
      val destCpi2    : con -> con option
      val destCarrow  : con -> (con * con) option
      val destCforall : con -> (variable * kind * con) option

   end


structure OpsDirect 
   :
   OPS_DIRECT
   =
   struct
      open ILDirect

      fun destKtype k =
          (case k of
              Ktype => true
            | _ => false)

      fun destKarrow k =
          (case k of
              Karrow x => SOME x
            | _ => NONE)

      fun destKprod k =
          (case k of
              Kprod x => SOME x
            | _ => NONE)

      fun destClam c =
          (case c of
              Clam x => SOME x
            | _ => NONE)

      fun destCvar c =
          (case c of
              Cvar x => SOME x
            | _ => NONE)

      fun destCapp c =
          (case c of
              Capp x => SOME x
            | _ => NONE)

      fun destCpair c =
          (case c of
              Cpair x => SOME x
            | _ => NONE)

      fun destCpi1 c =
          (case c of
              Cpi1 x => SOME x
            | _ => NONE)

      fun destCpi2 c =
          (case c of
              Cpi2 x => SOME x
            | _ => NONE)

      fun destCarrow c =
         (case c of
             Carrow x => SOME x
           | _ => NONE)

      fun destCforall c =
         (case c of
             Cforall x => SOME x
           | _ => NONE)

   end


functor CoerceOpsDirectToSplit
   (structure Ops : OPS_DIRECT)
   :
   OPS_SPLIT
   =
   struct
      
      open Ops

      fun obsolete method = raise (Fail ("Obsolete method: "^method))

      fun Ksing _ = obsolete "Ksing"
      fun Kpi _ = obsolete "Kpi"
      fun Ksigma _ = obsolete "Ksigma"
      fun destKsing _ = obsolete "destKsing"
      fun destKpi _ = obsolete "destKpi"
      fun destKsigma _ = obsolete "destKsigma"

   end


signature PASS_DIRECT =
   sig

      type variable = Variable.variable
      type kind
      type con
      type term

      type kindresult
      type conresult
      type termresult

      type self

      val caseKtype   : self -> unit -> kindresult
      val caseKarrow  : self -> kind * kind -> kindresult
      val caseKprod   : self -> kind * kind -> kindresult

      val caseCvar    : self -> variable -> conresult
      val caseClam    : self -> variable * kind * con -> conresult
      val caseCapp    : self -> con * con -> conresult
      val caseCpair   : self -> con * con -> conresult
      val caseCpi1    : self -> con -> conresult
      val caseCpi2    : self -> con -> conresult
      val caseCarrow  : self -> con * con -> conresult
      val caseCforall : self -> variable * kind * con -> conresult

      val caseTvar    : self -> variable -> termresult
      val caseTlam    : self -> variable * con * term -> termresult
      val caseTapp    : self -> term * term -> termresult
      val caseTplam   : self -> variable * kind * term -> termresult
      val caseTpapp   : self -> term * con -> termresult

   end


signature TRAVERSE_DIRECT =
   sig

      type kind
      type con
      type term

      type kindresult
      type conresult
      type termresult

      val traverseKind : kind -> kindresult
      val traverseCon : con -> conresult
      val traverseTerm : term -> termresult

   end


functor SelfDirect (structure Ops : OPS_DIRECT
                    type kindresult
                    type conresult
                    type termresult)
   :
   sig
      type self
      val kself : self -> Ops.kind -> kindresult
      val cself : self -> Ops.con -> conresult
      val tself : self -> Ops.term -> termresult
   end
   =
   SelfSplit (structure Ops = CoerceOpsDirectToSplit (structure Ops = Ops)
              type kindresult = kindresult
              type conresult = conresult
              type termresult = termresult)


functor TraverseDirect
   (structure Pass : PASS_DIRECT
                     where type kind = ILDirect.kind
                     where type con = ILDirect.con
                     where type term = ILDirect.term
    val mkself : { kself : Pass.kind -> Pass.kindresult,
                   cself : Pass.con -> Pass.conresult,
                   tself : Pass.term -> Pass.termresult } -> Pass.self) 
   :
   TRAVERSE_DIRECT
   =
   struct

      open Pass
      open ILDirect

      fun traverseKind k =
          let val self = mkself { kself = traverseKind,
                                  cself = traverseCon,
                                  tself = traverseTerm }
          in
             (case k of
                 Ktype => 
                    caseKtype self ()
               | Karrow x => 
                    caseKarrow self x
               | Kprod x => 
                    caseKprod self x)
          end

      and traverseCon c =
          let val self = mkself { kself = traverseKind,
                                  cself = traverseCon,
                                  tself = traverseTerm }
          in
             (case c of
                 Cvar x =>
                    caseCvar self x
               | Clam x =>
                    caseClam self x
               | Capp x =>
                    caseCapp self x
               | Cpair x =>
                    caseCpair self x
               | Cpi1 x =>
                    caseCpi1 self x
               | Cpi2 x =>
                    caseCpi2 self x
               | Carrow x =>
                    caseCarrow self x
               | Cforall x =>
                    caseCforall self x)
          end

      and traverseTerm t =
          let val self = mkself { kself = traverseKind,
                                  cself = traverseCon,
                                  tself = traverseTerm }
          in
             (case t of
                 Tvar x =>
                    caseTvar self x
               | Tlam x =>
                    caseTlam self x
               | Tapp x =>
                    caseTapp self x
               | Tplam x =>
                    caseTplam self x
               | Tpapp x =>
                    caseTpapp self x)
          end

   end


functor SubstPassDirect
   (structure Ops : OPS_DIRECT
    structure Self :
       sig
          type self
          val kself : self -> Ops.kind -> Ops.con Variable.map -> Ops.kind
          val cself : self -> Ops.con -> Ops.con Variable.map -> Ops.con
          val tself : self -> Ops.term -> Ops.con Variable.map -> Ops.term
       end)
   :
   PASS_DIRECT
   =
   struct

      open Ops

      structure Super = 
         SubstPassSplit (structure Ops = CoerceOpsDirectToSplit (structure Ops = Ops)
                         structure Self = Self)

      open Super  (* Inherit cases. *)

      fun caseK2 f (_:self) (c1, c2) (_:con Variable.map) =
          f (c1, c2)

      val caseKarrow = caseK2 Karrow
      val caseKprod = caseK2 Kprod

      (* No need to traverse kinds any more. *)

      fun caseClam self (v, k, c) s =
          let val v' = Variable.newvar ()
          in
             Clam (v', k, Self.cself self c (Variable.extend s v (Cvar v')))
          end 

      fun caseCforall self (v, k, c) s =
          let val v' = Variable.newvar ()
          in
             Cforall (v', k, Self.cself self c (Variable.extend s v (Cvar v')))
          end 

      fun caseTplam self (v, k, t) s =
          let val v' = Variable.newvar ()
          in
             Tplam (v', k, Self.tself self t (Variable.extend s v (Cvar v')))
          end

   end


signature SUBST_DIRECT =
   sig

      type con
      type term

      val csubst : con Variable.map -> con -> con
      val tsubst : con Variable.map -> term -> term

      val csubst1 : con -> Variable.variable -> con -> con
      val tsubst1 : con -> Variable.variable -> term -> term

      val crename : Variable.variable -> Variable.variable -> con -> con
      val trename : Variable.variable -> Variable.variable -> term -> term

   end


functor SubstDirectFun
   (structure Ops : OPS_DIRECT
    structure Traverse : TRAVERSE_DIRECT
                         where type kind = Ops.kind
                         where type con = Ops.con
                         where type term = Ops.term
                         where type kindresult = Ops.con Variable.map -> Ops.kind
                         where type conresult = Ops.con Variable.map -> Ops.con
                         where type termresult = Ops.con Variable.map -> Ops.term)
   :>
   SUBST_DIRECT
   where type con = Ops.con
   where type term = Ops.term
   =
   SubstSplitFun (structure Ops = CoerceOpsDirectToSplit (structure Ops = Ops)
                  structure Traverse = Traverse)



local
   open ILDirect
   structure Self = SelfDirect (structure Ops = OpsDirect
                                type kindresult = con Variable.map -> kind
                                type conresult = con Variable.map -> con
                                type termresult = con Variable.map -> term)
   structure Pass = SubstPassDirect (structure Ops = OpsDirect
                                     structure Self = Self)
   structure Traverse = TraverseDirect (structure Pass = Pass
                                        fun mkself x = x)
in
   structure SubstDirect = SubstDirectFun (structure Ops = OpsDirect
                                           structure Traverse = Traverse)
end