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
   where type kind = ILSplit.kind
   where type con = ILSplit.con
   where type term = ILSplit.term
   =
   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 = { kself : kind -> kindresult,
                    cself : con -> conresult,
                    tself : term -> termresult }

      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 TraverseSplit
   (structure Pass : PASS_SPLIT
                     where type kind = ILSplit.kind
                     where type con = ILSplit.con
                     where type term = ILSplit.term)
   :>
   TRAVERSE_SPLIT
   where type kind = ILSplit.kind
   where type con = ILSplit.con
   where type term = ILSplit.term
   where type kindresult = Pass.kindresult
   where type conresult = Pass.conresult
   where type termresult = Pass.termresult
   =
   struct

      open Pass
      open ILSplit

      fun traverseKind k =
          let val self = { 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 = { 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 = { 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)
   :>
   PASS_SPLIT
   where type kind = Src.kind
   where type con = Src.con
   where type term = Src.term
   where type kindresult = arg -> Dst.kind
   where type conresult = arg -> Dst.con
   where type termresult = arg -> Dst.term
   =
   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

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

      fun caseKbind f ({kself, ...}:self) (v, k1, k2) arg =
          f (v, kself k1 arg, kself k2 arg)

      fun caseKtype _ () _ = 
          Dst.Ktype

      fun caseKsing ({cself, ...}:self) c arg = 
          Dst.Ksing (cself c arg)

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

      fun caseCbind f ({kself, cself, ...}:self) (v, k, c) arg =
          f (v, kself k arg, cself c arg)
             
      fun caseC1 f ({cself, ...}:self) c arg =
          f (cself c arg)

      fun caseC2 f ({cself, ...}:self) (c1, c2) arg =
          f (cself c1 arg, cself 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 ({cself, ...}:self) (c1, c2) arg =
          Dst.Carrow (cself c1 arg, cself c2 arg)

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

      fun caseTvar _ v _ = 
          Dst.Tvar v

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

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

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

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

   end


functor SubstPassSplit 
   (structure Ops : OPS_SPLIT)
   :>
   PASS_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
   =
   struct

      open Ops

      structure Super =
         IdPassSplit (type arg = Ops.con Variable.map
                      structure Src = Ops
                      structure Dst = Ops)

      open Super  (* Inherit cases. *)

      fun caseKbind f ({kself, ...}:self) (v, k1, k2) s =
          let val v' = Variable.newvar ()
          in
             f (v', kself k1 s, kself 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 ({kself, cself, ...}:self) (v, k, c) s =
          let val v' = Variable.newvar ()
          in
             f (v', kself k s, cself c (Variable.extend s v (Cvar v')))
          end 

      val caseClam = caseCbind Clam
      val caseCforall = caseCbind Cforall

      fun caseTplam ({kself, tself, ...}:self) (v, k, t) s =
          let val v' = Variable.newvar ()
          in
             Tplam (v', kself k s, tself 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
   where type kind = Ops.kind
   where type con = Ops.con
   where type term = Ops.term
   =
   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 Pass = SubstPassSplit (structure Ops = OpsSplit)
   structure Traverse = TraverseSplit (structure Pass = Pass)
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
   where type kind = ILDirect.kind
   where type con = ILDirect.con
   where type term = ILDirect.term
   =
   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
   where type kind = Ops.kind
   where type con = Ops.con
   where type term = Ops.term
   =
   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 = { kself : kind -> kindresult,
                    cself : con -> conresult,
                    tself : term -> termresult }

      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 TraverseDirect
   (structure Pass : PASS_DIRECT
                     where type kind = ILDirect.kind
                     where type con = ILDirect.con
                     where type term = ILDirect.term)
   :>
   TRAVERSE_DIRECT
   where type kind = ILDirect.kind
   where type con = ILDirect.con
   where type term = ILDirect.term
   where type kindresult = Pass.kindresult
   where type conresult = Pass.conresult
   where type termresult = Pass.termresult
   =
   struct

      open Pass
      open ILDirect

      fun traverseKind k =
          let val self = { 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 = { 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 = { 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)
   :>
   PASS_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
   =
   struct

      open Ops

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

      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 ({cself, ...}:self) (v, k, c) s =
          let val v' = Variable.newvar ()
          in
             Clam (v', k, cself c (Variable.extend s v (Cvar v')))
          end 

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

      fun caseTplam ({tself, ...}:self) (v, k, t) s =
          let val v' = Variable.newvar ()
          in
             Tplam (v', k, tself 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
   structure Pass = SubstPassDirect (structure Ops = OpsDirect)
   structure Traverse = TraverseDirect (structure Pass = Pass)
in
   structure SubstDirect = SubstDirectFun (structure Ops = OpsDirect
                                           structure Traverse = Traverse)
end