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

      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


signature EQUIV_SPLIT =
   sig

      type kind
      type con

      exception TypeError

      type kcontext = kind Variable.map

      val whnf : kcontext -> con -> con
      val equiv : kcontext -> con -> con -> kind -> unit
      val subkind : kcontext -> kind -> kind -> unit
      val samekind : kcontext -> kind -> kind -> unit
      val selfify : con -> kind -> kind

   end


structure EquivSplit
   :>
   EQUIV_SPLIT
   where type kind = ILSplit.kind
   where type con = ILSplit.con
   =
   struct

      open ILSplit
      exception TypeError
      type kcontext = kind Variable.map

      exception ThisIsProjectTwo

      fun naturalKind ctx c = raise ThisIsProjectTwo
      fun whreduce c = raise ThisIsProjectTwo
      fun whnf ctx c = raise ThisIsProjectTwo
      fun equiv ctx c1 c2 k = raise ThisIsProjectTwo
      fun equivPath ctx c1 c2 = raise ThisIsProjectTwo
      fun samekind ctx k1 k2 = raise ThisIsProjectTwo
      fun subkind ctx k1 k2 = raise ThisIsProjectTwo

      fun selfify c k =
          (case k of
              Ktype =>
                 Ksing c
            | Ksing _ =>
                 k
            | Kpi (v, k1, k2) =>
                 let val v' = Variable.newvar ()
                 in
                    Kpi (v', k1, selfify (Capp (c, Cvar v')) (SubstSplit.krename v' v k2))
                 end
            | Ksigma (v, k1, k2) =>
                 Ksigma (Variable.newvar (),
                         selfify (Cpi1 c) k1,
                         selfify (Cpi2 c) (SubstSplit.ksubst1 (Cpi1 c) v k2)))

   end


functor TidPassSplit
   (structure Src : OPS_SPLIT
    structure Dst : OPS_SPLIT
    type arg
    type karg
    val karg : Src.kind Variable.map * Src.con Variable.map * arg -> karg
    structure Subst : SUBST_SPLIT
                      where type kind = Src.kind
                      where type con = Src.con
                      where type term = Src.term
    structure Equiv : EQUIV_SPLIT
                      where type kind = Src.kind
                      where type con = Src.con
    structure Self :
       sig
          type self
          val kself : self -> Src.kind -> karg -> Dst.kind
          val cself : self -> Src.con -> karg -> Dst.con
          val tself : self -> Src.term -> Src.kind Variable.map * Src.con Variable.map * arg -> Src.con * Dst.term
       end)
   : 
   PASS_SPLIT
   =
   struct
      
      type variable = Variable.variable
      type kind = Src.kind
      type con = Src.con
      type term = Src.term

      type kindresult = karg -> Dst.kind
      type conresult = karg -> Dst.con
      type termresult = Src.kind Variable.map * Src.con Variable.map * arg -> Src.con * Dst.term  

      open Self
      open Variable
      open Subst

      exception TypeError = Equiv.TypeError

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

      fun caseK0 x (_:self) () (_:karg) = x

      val caseKtype = caseK0 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 caseC0 x (_:self) () (_:karg) = x
          
      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)

      val caseCforall = caseCbind Dst.Cforall


      fun caseTvar self v (_, cctx, _) =
          (case find cctx v of
              SOME c =>
                 (c, Dst.Tvar v)
            | NONE =>
                 raise TypeError)

      fun caseTlam self (v, c1, t) (arg as (kctx, cctx, subarg)) =
          let val c1' = cself self c1 (karg arg)
              val cctx' = extend cctx v c1
              val (c2, t') = tself self t (kctx, cctx', subarg)
          in
             (Src.Carrow (c1, c2),
              Dst.Tlam (v, c1', t'))
          end

      fun caseTapp self (t1, t2) (arg as (kctx, _, _)) =
          let val (c1, t1') = tself self t1 arg
              val (c2, t2') = tself self t2 arg
          in
             (case Src.destCarrow (Equiv.whnf kctx c1) of
                 SOME (dom, cod) =>
                    (cod, Dst.Tapp (t1', t2'))
               | NONE =>
                    raise TypeError)
          end

      fun caseTplam self (v, k, t) (arg as (kctx, cctx, subarg)) =
          let val k' = kself self k (karg arg)
              val v' = newvar ()
              val kctx' = extend kctx v' k
              val (c, t') = tself self (trename v' v t) (kctx', cctx, subarg)
          in
             (Src.Cforall (v', k, c),
              Dst.Tplam (v', k', t'))
          end

      fun caseTpapp self (t, c) (arg as (kctx, _, _)) =
          let val (c1, t') = tself self t arg
              val c' = cself self c (karg arg)
          in
             (case Src.destCforall (Equiv.whnf kctx c1) of
                 SOME (v, k1, c2) =>
                    (csubst1 c v c2,
                     Dst.Tpapp (t', c'))
               | NONE =>
                    raise TypeError)
          end

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

      val translateTerm : ILSplit.term -> ILDirect.term

   end


structure SingelimPass : PASS_SPLIT
   =
   struct

      type arg = ILSplit.kind Variable.map * ILSplit.con Variable.map * unit

      structure Self = SelfSplit (structure Ops = OpsSplit
                                  type kindresult = unit -> ILDirect.kind
                                  type conresult = unit -> ILDirect.con
                                  type termresult = arg -> ILSplit.con * ILDirect.term)

      structure Super =
         TidPassSplit (type arg = unit
                       type karg = unit
                       fun karg _ = ()
                       structure Src = OpsSplit
                       structure Dst = CoerceOpsDirectToSplit (structure Ops = OpsDirect)
                       structure Subst = SubstSplit
                       structure Equiv = EquivSplit
                       structure Self = Self)


      open Variable
      open ILDirect
      open Self

      open Super  (* Inherit cases. *)

      
      (* PUT CASES HERE *)

   end




structure Singelim :> SINGELIM =
   struct

      structure Traverse = TraverseSplit (structure Pass = SingelimPass
                                          fun mkself x = x)

      fun translate c t =
          (Traverse.traverseCon c (),
           #2 (Traverse.traverseTerm t (Variable.null, Variable.null, ())))

   end