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 PASS_SPLIT =
   sig

      type variable = Variable.variable
      type kind = ILSplit.kind
      type con = ILSplit.con
      type term = ILSplit.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


structure SubstPassSplit 
   :>
   PASS_SPLIT
   where type kindresult = ILSplit.con Variable.map -> ILSplit.kind
   where type conresult = ILSplit.con Variable.map -> ILSplit.con
   where type termresult = ILSplit.con Variable.map -> ILSplit.term
   =
   struct

      open Variable
      open ILSplit

      type kindresult = con map -> kind
      type conresult = con map -> con
      type termresult = con map -> term

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

      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 

      fun caseKtype _ () s = Ktype

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

      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 

      fun caseC2 f ({cself, ...}:self) (c1, c2) s =
          f (cself c1 s, cself c2 s)

      fun caseC1 f ({cself, ...}:self) c s =
          f (cself c s)

      val caseClam = caseCbind Clam
      val caseCapp = caseC2 Capp
      val caseCpair = caseC2 Cpair
      val caseCpi1 = caseC1 Cpi1
      val caseCpi2 = caseC1 Cpi2
      val caseCarrow = caseC2 Carrow
      val caseCforall = caseCbind Cforall

      fun caseTvar _ v s =
          Tvar v

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

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

      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

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

   end


signature TRAVERSE_SPLIT =
   sig

      type kind = ILSplit.kind
      type con = ILSplit.con
      type term = ILSplit.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)
   :>
   TRAVERSE_SPLIT
   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


signature SUBST_SPLIT =
   sig

      type kind = ILSplit.kind
      type con = ILSplit.con
      type term = ILSplit.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 Traverse : TRAVERSE_SPLIT
                         where type kindresult = ILSplit.con Variable.map -> ILSplit.kind
                         where type conresult = ILSplit.con Variable.map -> ILSplit.con
                         where type termresult = ILSplit.con Variable.map -> ILSplit.term)
   :>
   SUBST_SPLIT
   =
   struct

      type kind = ILSplit.kind
      type con = ILSplit.con
      type term = ILSplit.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 (ILSplit.Cvar v') v k
      fun crename v' v c = csubst1 (ILSplit.Cvar v') v c
      fun trename v' v t = tsubst1 (ILSplit.Cvar v') v t

   end


local
   structure Traverse = TraverseSplit (structure Pass = SubstPassSplit)
in
   structure SubstSplit = SubstSplitFun (structure Traverse = Traverse)
end