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 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


structure SubstSplit :> SUBST_SPLIT =
   struct

      open Variable
      open ILSplit

      fun ksubst s k =
          (case k of
              Ktype => 
                 Ktype
            | Ksing c => 
                 Ksing (csubst s c)
            | Kpi (v, k1, k2) =>
                 let val v' = newvar ()
                 in
                    Kpi (v', ksubst s k1, ksubst (extend s v (Cvar v')) k2)
                 end
            | Ksigma (v, k1, k2) =>
                 let val v' = newvar ()
                 in
                    Ksigma (v', ksubst s k1, ksubst (extend s v (Cvar v')) k2)
                 end)

      and csubst s c =
          (case c of
              Cvar v =>
                 (case find s v of
                     NONE => c
                   | SOME c' => c')
            | Clam (v, k, c) =>
                 let val v' = newvar ()
                 in
                    Clam (v', ksubst s k, csubst (extend s v (Cvar v')) c)
                 end
            | Capp (c1, c2) =>
                 Capp (csubst s c1, csubst s c2)
            | Cpair (c1, c2) =>
                 Cpair (csubst s c1, csubst s c2)
            | Cpi1 c =>
                 Cpi1 (csubst s c)
            | Cpi2 c =>
                 Cpi2 (csubst s c)
            | Carrow (c1, c2) =>
                 Carrow (csubst s c1, csubst s c2)
            | Cforall (v, k, c) =>
                 let val v' = newvar ()
                 in
                    Cforall (v', ksubst s k, csubst (extend s v (Cvar v')) c)
                 end)

      fun tsubst s t =
          (case t of
              Tvar _ =>
                 t
            | Tlam (v, c, t) =>
                 Tlam (v, csubst s c, tsubst s t)
            | Tapp (t1, t2) =>
                 Tapp (tsubst s t1, tsubst s t2)
            | Tplam (v, k, t) =>
                 let val v' = newvar ()
                 in
                    Tplam (v', ksubst s k, tsubst (extend s v (Cvar v')) t)
                 end
            | Tpapp (t, c) =>
                 Tpapp (tsubst s t, csubst s c))

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

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

   end