external forall alpha
external ty.i.j ty.i.0 ty.i.n C.i e.i p.i j C.i.unp emptyenvl identc..unp ty.i.l ty.i.r ty ty..a l r f ty..f ty..g ty..b sym trans left right identx coe..1 coe..2 compose ty..a ty.b alpha.i beta.i dot subst tya p' e'.s f' identc identv.i identv..._ _ ty.i.p v v.i ty.i congrsubst ty..a._ ty..b._ spine coe..._ ty' coeOut..l coeOut..r coe.i coeIn coeIn..._ e' ty'.i ty..r coe.i.._ ty''..b e'..s

external trans sc sc1 sc2 sc3 coe' x y congruence Uni coe

viewhierarchy = F < FE < G < T, C


data Prog [prog]
  view F
    | Prog [prog]
        decls :: Decls
        body  :: Expr

data Decl [decl]
  view F
    | Data [adt]
        ident   :: Name
        params  :: Names
        constrs :: Constrs

data Constr [constr]
  view F
    | Constr [constr]
        ident  :: Name
        fields :: Types
  view FE
    | Constr [constr]
        vars   :: Names
  view G
    | Constr [constr]
        eqs    :: Equations

data Expr [expr]
  view F
    | Var [e.var]
        ident :: Name
    | Con [e.con]
        ident :: Name
    | AppE [e.app.expr]
        f :: Expr
        a :: Expr
    | AppT [e.app.univ]
        f :: Expr
        a :: Type
    | LamE [e.lam.abs]
        pat   :: Pat
        body  :: Expr
    | LamT [e.univ.abs]
        ident :: Name
        body  :: Expr
    | Let [e.let]
        defs  :: Bindings
        body  :: Expr
    | Case [e.case]
        scrutinee :: Expr
        alts      :: Alts
  view G
    | AppC [e.app.eqs]
        f :: Expr
    | Coerce [e.coerce]
        e :: Expr

data Binding [binding]
  view F
    | Def [binding]
        pat  :: Pat
        body :: Expr

data Alt [alt]
  view F
    | Alt [alt]
        pat  :: Pat
        body :: Expr
        tp   :: Type

data Pat [pat]
  view F
    | Con [p.con]
        ident :: Name
    | Var [p.var]
        ident :: Name
        tp    :: Type
    | AppP [p.app.pat]
        f :: Pat
        a :: Pat
    | AppT [p.app.univ]
        f :: Pat
        a :: Type
  view FE
    | AppV [p.app.exist]
        f :: Pat
        a :: Name
  view G
    | AppC [p.app.eqs]
        f :: Pat

data Type [type]
  view F
    | Con [t.con]
        ident :: Name
    | Var [t.var]
        ident :: Name
    | App [t.app]
        f :: Type
        a :: Type
    | Forall [t.forall]
        ident :: Name
        ty    :: Type
  view FE
    | Exists [t.exists]
        ident :: Name
        ty    :: Type
  view G
    | Eqs [t.eqs]
        eqs :: Equations
        ty  :: Type


scheme expr "Expr" =
  view F =
    holes [ node e : Expr, env : Env | | ty : Type ]
    judgespec env :- e : ty
    judgeuse tex env :-."e" e : ty
  view T =
    holes [ node e : Expr, env : Env | | ty : Type, e' : Expr' ]
    judgespec env :- e : ty ~> e'
    judgeuse tex env :-."e" e : ty ~> e'

ruleset expr.base scheme expr "Expression type rules" =
  rule e.coerce "Coerce" =
    view G =
      judge B : expr = env :- e : ((subst ty v)..._ ty')
      judge E : entails = env ::- ty.i =*= v.i
      ---
      judge R : expr = env :- e : ty'
    view T =
      judge E : entails = env ::- ty.i =*= v.i ~> coe.i
      judge T : equalty = ty' `=` (subst ty v)..._ ty
--    judge S : spine = (_ ^^^) ; coe..._ ; env :- ty ~~ ty' ~> coe ; _
      judge S : lift = coe..._ ~> coe
      ---
      judge R : expr = env :- e : ty' ~> (e' :> coe)

  rule e.app.eqs "AppC" =
    view G =
      judge F : expr = env :- e : ( ((ty..l =*= ty..r)..._) => ty)
      judge* P : entails = env ::- ty.i.l =*= ty.i.r
      ---
      judge R : expr = env :- e : ty
      group P F
    view T =
      ---
      judge R : expr = env :- e : ty ~> (e' coe)

  rule e.con "Con" =
    view F =
      judge L : lookup = env(identc) `=` ty
      ---
      judge R : expr = env :- identc : ty
    view T =
      ---
      judge R : expr = env :- identc : ty ~> identc

  rule e.var "Var" =
    view F =
      judge L : lookup = env(identx) `=` ty
      ---
      judge R : expr = env :- identx : ty
    view T =
      ---
      judge R : expr = env :- identx : ty ~> identx
  
  rule e.app.expr "AppE" =
    view F =
      judge F : expr = env :- f : (ty..a -> ty)
      judge A : expr = env :- a : ty..a
      ---
      judge R : expr = env :- f a : ty
    view T =
      judge F : expr = env :- f : (ty..a -> ty) ~> f'
      judge A : expr = env :- a : ty..a ~> a'
      ---
      judge R : expr = env :- f a : ty ~> (f' a')
  
  rule e.app.univ "AppT" =
    view F = 
--      judge A : kind = env :- ty..a
      judge F : expr = env :- f : (forall^alpha^dot ty)
      ---
      judge R : expr = env :- f ty..a : ((subst tya alpha) ty)
    view T =
      judge F : expr = env :- f : (forall^alpha^dot ty) ~> f'
      ---
      judge R : expr = env :- f ty..a : ((subst tya alpha) ty) ~> (f' ty..a)

  rule e.lam.abs "LamE" =
    view F =
--      judge A : kind = env :- ty..a
      judge P : pat  = env ; envl :- p : ty..a
      judge B : expr = (envl env) :- e : ty
      ---
      judge R : expr = env :- (\p dot e) : (ty..a -> ty)
    view FE =
      judge E : emptyintersection = ty >< envl <== env
      ---
    view T =
      ---
      judge R : expr = env :- (\p dot e) : (ty..a -> ty) ~> (\p' dot e')

  rule e.univ.abs "LamT" =
    view F =
      judge B : expr = (v, env) :- e : ty
      ---
      judge R : expr = env :- (BigLam v dot e) : (forall^v^dot ty)
    view FE =
      judge E : notelemftv = !env(v)
      ---
    view T =
      ---
      judge R : expr = env :- (BigLam v dot e) : (forall^v^dot ty) ~> (BigLam v dot e')

  rule e.let "Let" =
    view F =
      judge P  : pat  = env ; envl :- p.i : ty.i
      judge E1 : expr = (envl env) :- e.i : ty.i
      judge B  : expr = (envl env) :- e : ty
      ---
      judge R : expr = env :- (let ^^^ (p `=` e)..._ ^^^ in e) : ty
    view FE =
      judge E2 : emptyintersection = ty >< envl <== env
      ---
    view T =
      judge P  : pat  = env ; envl :- p.i : ty.i ~> p'.i
      judge E1 : expr = (envl env) :- e.i : ty.i ~> e'.i
      ---
      judge R : expr = env :- (let ^^^ (p `=` e)..._ ^^^ in e) : ty ~> (let ^^^ (p' `=` e')..._ ^^^ in e')

  rule e.case "Case" =
    view F =
      judge P : pat = env ; envl.i :- p.i : ty..p
      judge B : expr = (envl.i env) :- e.i : ty
      judge S : expr = env :- e..s : ty..p
      ---
      judge R : expr = env :- ((case e..s ^^^ of ^^^ (p -> e)..._) :: ty) : ty
    view FE =
      judge E : emptyintersection = ty..p >< envl.i <== env
      ---
    view T =
      judge P : pat = env ; envl.i :- p.i : ty.i.p ~> p'.i
      judge B : expr = (envl.i env) :- e.i : ty ~> e'.i
      ---
      judge R : expr = env :- ((case e..s ^^^ of ^^^ (p -> e)..._) :: ty) : ty ~> (case e'..s ^^^ of ^^^ (p' -> e')..._)


ruleset expr.trans scheme expr "Expression type rules" =
  rule e.app.eqs "AppC" =
    view G =
      judge F : expr = env :- e : ( ((ty..l =*= ty..r)..._) => ty)
      judge P : entails = env ::- ty.i.l =*= ty.i.r
      ---
      judge R : expr = env :- e : ty
    view T =
      ---
      judge R : expr = env :- e : ty ~> (e' coe)
    group P F

  rule e.coerce "Coerce" =
    view G =
      judge B : expr = env :- e : ((subst ty v)..._ ty')
      judge E : entails = env ::- ty.i =*= v.i
      ---
      judge R : expr = env :- e : ty'
    view T =
      judge E : entails = env ::- ty.i =*= v.i ~> coe.i
--    judge T : equalty = ty' `=` (subst ty v)..._ ty
--    judge S : spine = (_ ^^^) ; coe..._ ; env :- ty ~~ ty' ~> coe ; _
      judge S : lift = coe..._ ~> coe
      ---
      judge R : expr = env :- e : ty' ~> (e' :> coe)

ruleset expr.syndir scheme expr "Expression type rules (syn. dir.)" =
  rule e.con "Con" =
    view T =
      judge L : lookup = env(identc) `=` ( ((ty..l =*= ty..r)..._) => ty)
      judge P : entails = env ::- ty.i.l =*= ty.i.r ~> coe.i
      ---
      judge R : expr = env :- e : ty ~> (identc coe..._)

  rule e.case "Case" =
    view F =
      judge P : pat = env ; env.i :- p.i : ty.i.p
      judge B : expr = (env.i env) :- e.i : ty
      judge S : expr = env :- e.s : ty.i.p
      ---
      judge R : expr = env :- ((case e.s ^^^ of ^^^ (p -> e)..._) :: ty) : ty
    view FE =
      judge E : emptyintersection = ty.i.p >< env.i <== env
      ---
    view T =
      judge P : pat = env ; env.i :- p.i : ty.i.p ~> p'.i
      judge B : expr = (env.i env) :- e.i : ty.i ~> e'.i
      
      judge E : entails = (env.i env) ::- ty.i.r =*= v.i ~> coe.i
      judge T : equalty = ty' `=` (subst ty..r v)..._ ty
--    judge S : spine = (_ ^^^) ; coe.i.._ ; (env.i env) :- ty'.i ~~ ty.i ~> coe.i ; _
      judge S : decompose = coe.i.._ ~> coe.i
      ---
      judge R : expr = env :- ((case e.s ^^^ of ^^^ (p -> e)..._) :: ty) : ty ~> (case e'.s ^^^ of ^^^ (p' -> e' :> coe)..._)


scheme kind "Kind" =
  view F =
    holes [ node t : Type, env : Gam | | ]
    judgespec env :- t
    judgeuse tex env :-."k" t

ruleset kind.base scheme kind "Well-formedness rules" =
  rule t.con "Con" =
    view F =
      judge L : elem = env(identc)
      ---
      judge R : kind = env :- identc

  rule t.var "Var" =
    view F =
      judge L : elem = env(identx)
      ---
      judge R : kind = env :- identx
  
  rule t.app "App" =
    view F =
      judge F : kind = env :- f
      judge A : kind = env :- a
      ---
      judge R : kind = env :- f a

  rule t.forall "Forall" =
    view F =
      judge B : kind = (alpha,env) :- ty
      ---
      judge R : kind = env :- (forall^alpha^dot ty)
  
  rule t.exists "Exists" =
    view FE =
      judge B : kind = (alpha,env) :- ty
      ---
      judge R : kind = env :- (exists alpha dot ty)
  rule t.eqs "Eqs" =
    view G =
      judge L  : elem = env (ty.i.l =*= ty.i.r)
      judge BL : kind = env :- ty.i.l
      judge BR : kind = env :- ty.i.r
      judge B  : kind = env :- ty
      ---
      judge R : kind = env :- (((ty..l =*= ty..r)..._) => ty)


scheme pat "Pat" =
  view F =
    holes [ node p : Pat, env : Gam | | ty : Type, envl : Gam ]
    judgespec env ; envl :- p : ty
    judgeuse tex env ; envl :-."p" p : ty
  view T =
    holes [ node p : Pat, env : Gam | | ty : Type, envl : Gam, p' : Pat' ]
    judgespec env ; envl :- p : ty ~> p'
    judgeuse tex env ; envl :-."p" p : ty ~> p'

ruleset pat.base scheme pat "Pattern type rules" =
  rule p.con "Con" =
    view F =
      judge L : lookup = env(identc..unp) `=` ty
      ---
      judge R : pat = env ; emptyenvl :- identc : ty
    view T =
      ---
      judge R : pat = env ; emptyenvl :- identc : ty ~> identc

  rule p.var "Var" =
    view F =
      judge L : insert = envl(identx) `=` ty
      ---
      judge R : pat = env ; envl :- (identx :: ty) : ty
    view T =
      ---
      judge R : pat = env ; envl :- (identx :: ty) : ty ~> (identx :: ty)
  
  rule p.app.pat "AppP" =
    view F =
      judge F : pat = env ; envl :- f : (ty..a -> ty)
      judge A : pat = env ; envl :- a : ty..a
      ---
      judge R : pat = env ; envl :- f a : ty
    view T =
      judge F : pat = env ; envl :- f : (ty..a -> ty) ~> f'
      judge A : pat = env ; envl :- a : ty..a ~> a'
      ---
      judge R : pat = env ; envl :- f a : ty ~> (f' a')

  rule p.app.univ "AppT" =
    view F =
--      judge A : kind = env :- ty..a
      judge F : pat  = env ; envl :- f : (forall^alpha^dot ty)
      ---
      judge R : pat = env ; envl :- f ty..a : ((subst tya alpha) ty)
    view T =
      judge F : pat  = env ; envl :- f : (forall^alpha^dot ty) ~> f'
      ---
      judge R : pat = env ; envl :- f ty..a : ((subst tya alpha) ty) ~> (f' ty..a)

  rule p.app.exist "AppV" =
    view FE =
      judge F : pat = env ; envl :- f : (exists alpha dot ty)
      judge* D2 : elem = envl identv
      judge E1 : notelemftv = ! env identv
      ---
      judge R : pat = env ; envl :- f identv : ((subst identv alpha) ty)
      group D2 E1
    view T =
      judge F : pat = env ; envl :- f : (exists alpha dot ty) ~> f'
      ---
      judge R : pat = env ; envl :- f identv : ((subst identv alpha) ty) ~> (f' identv)
  
  rule p.app.eqs "AppC" =
    view G =
      judge* F : pat = env ; envl :- f : (((ty..l =*= ty..r)..._) => ty)
      judge C : elem = envl (ty.i.l =*= ty.i.r)
      ---
      judge R : pat = env ; envl :- f : ty
      group F C
    view T =
      judge C : lookup = envl(identv.i) `=` ((ty.i.l =*= ty.i.r))
      ---
      judge R : pat = env ; envl :- f : ty ~> f' identv..._


scheme decl "Decl" =
  view F =
    holes [ node d : Decl, env : Gam | | ]
    judgespec env :- d
    judgeuse tex env :-."d" d

ruleset decl.base scheme decl "Data definition type rules" =
  rule adt "Data" =
    view F =
      judge L1 : elem = env(D)
      judge L2 : lookup = env(C.i) `=` (forall^alpha..._ dot (ty).(i,0) -> dots -> (ty).(i,n.i) -> D ^^^ (alpha..._).i)
--      judge K : kind = (alpha..._, env) :-."k" (ty).(i,j)
      ---
      judge R : decl = env :- (dta D ^^^ alpha..._ `=` (C ^^^ ty..._)..._)
    view FE =
      judge L2 : lookup = env(C.i) `=` (forall^alpha..._ forall^(beta..._).i ^^^ dot (ty).(i,0) -> dots -> (ty).(i,n.i) -> D ^^^ (alpha..._).i)
      judge L3 : lookup = env(C.i.unp) `=` (forall^alpha..._ ^^^ exists (beta..._).i ^^^ dot (ty).(i,0) -> dots -> (ty).(i,n.i) -> D ^^^ (alpha..._).i)
--      judge K : kind = (alpha..._ beta..._, env) :-."k" (ty).(i,j)
      ---
      judge R : decl = env :- (dta D ^^^ alpha..._ `=` (exists beta..._ dot C ^^^ ty..._)..._)
    view G =
      judge L2 : lookup = env(C.i) `=` (forall^alpha..._ forall^(beta..._).i ^^^ dot ((x..l =*= ty..r)..._) => (ty).(i,0) -> dots -> (ty).(i,n.i) -> D ^^^ (alpha..._).i)
      judge L3 : lookup = env(C.i.unp) `=` (forall^alpha..._ ^^^ exists (beta..._).i ^^^ dot ((x..l =*= ty..r)..._) => (ty).(i,0) -> dots -> (ty).(i,n.i) -> D ^^^ (alpha..._).i)
--      judge K : kind = (alpha..._, (beta..._).i, env) :-."k" (ty).(i,j)
--      judge K2 : kind = (alpha..._, (beta..._).i, env) :-."k" (x).(i,j).l
--      judge K3 : kind = (alpha..._, (beta..._).i, env) :-."k" (ty).(i,j).r
      ---
      judge R : decl = env :- (dta D ^^^ alpha..._ `=` (`|` exists^beta..._ dot ((x..l =*= ty..r)..._) => C ^^^ ty..._)..._)


relation entails "Entailment" =
  view G =
    holes [ ty..l: Type, ty..r: Type, env: Gam | | ]
    judgespec env ::- ty..l =*= ty..r
  view T =
    holes [ ty..l: Type, ty..r: Type, env: Gam | | coe: Coercion]
    judgespec env ::- ty..l =*= ty..r ~> coe

ruleset entails.base scheme entails "Entailment rules" =
  rule e.sym "Symmetry" =
    view G =
      judge B : entails = env ::- ty..r =*= ty..l
      ---
      judge R : entails = env ::- ty..l =*= ty..r
    view T =
      judge B : entails = env ::- ty..r =*= ty..l ~> coe
      ---
      judge R : entails = env ::- ty..l =*= ty..r ~> sym coe

  rule e.trans "Transitivity" =
    view G =
      judge B1 : entails = env ::- ty..l =*= ty..a
      judge B2 : entails = env ::- ty..a =*= ty..r
      ---
      judge R : entails = env ::- ty..l =*= ty..r
    view T =
      judge B1 : entails = env ::- ty..l =*= ty..a ~> coe..1
      judge B2 : entails = env ::- ty..a =*= ty..r ~> coe..2
      ---
      judge R : entails = env ::- ty..l =*= ty..r ~> (coe..2 compose coe..1)

  rule e.assume "Assume" =
    view G =
      judge L : elem = env (ty..l =*= ty..r)
      ---
      judge R : entails = env ::- ty..l =*= ty..r
    view T =
      judge L : lookup = env (identx) `=` ((ty..l =*= ty..r))
      ---
      judge R : entails = env ::- ty..l =*= ty..r ~> identx

  rule e.congr "Congr" =
    view G =
      judge B : entails = env ::- v.i =*= ty.i
      judge T : entails = env ::- (congrsubst ty..a) =*= ty..b
      ---
      judge R : entails = env ::- ty..a =*= ty..b
    view T =
--    judge S : spine = (_ ^^^) ; coe..._ ; env :- ty..a ~~ (congrsubst ty..a) ~> coe ; _
      judge S : lift = coe..._ ~> coe
      judge B : entails = env ::- v.i =*= ty.i ~> coe.i
      judge T : entails = env ::- (congrsubst ty..a) =*= ty..b ~> coe..tl
      ---
      judge R : entails = env ::- ty..a =*= ty..b ~> coe..tl compose coe
  
  rule e.subsume "Subsume" =
    view G =
      judge B : entails = env ::- (ty [ty..a._]) =*= (ty [ty..b._])
      ---
      judge R : entails = env ::- ty.i.a =*= ty.i.b
    view T =
      judge B : entails = env ::- (ty [ty..a._]) =*= (ty [ty..b._]) ~> coe
--    judge S : spine = coe ; (_ ^^^) ; env :- (ty [ty..a._]) ~~ (ty [ty..b._]) ~> (_ ^^^) ; coe..._
      judge S : decompose = coe ~> coe..._
      ---
      judge R : entails = env ::- ty.i.a =*= ty.i.b ~> coe.i


ruleset entails.alt scheme entails "Entailment rules (alt.)" =
  rule e.refl "Refl" =
    view G =
      ---
      judge R : entails = env ::- ty =*= ty
    view T =
      ---
      judge R : entails = env ::- ty =*= ty ~> ty

  rule e.sym "Symmetry" =
    view G =
      judge B : entails = env ::- ty..r =*= ty..l
      ---
      judge R : entails = env ::- ty..l =*= ty..r
    view T =
      judge B : entails = env ::- ty..r =*= ty..l ~> coe
      ---
      judge R : entails = env ::- ty..l =*= ty..r ~> sym coe

  rule e.trans "Transitivity" =
    view G =
      judge B1 : entails = env ::- ty..l =*= ty..a
      judge B2 : entails = env ::- ty..a =*= ty..r
      ---
      judge R : entails = env ::- ty..l =*= ty..r
    view T =
      judge B1 : entails = env ::- ty..l =*= ty..a ~> coe..1
      judge B2 : entails = env ::- ty..a =*= ty..r ~> coe..2
      ---
      judge R : entails = env ::- ty..l =*= ty..r ~> (coe..2 compose coe..1)

  rule e.assume "Assume" =
    view G =
      judge L : elem = env (ty..l =*= ty..r)
      ---
      judge R : entails = env ::- ty..l =*= ty..r
    view T =
      judge L : lookup = env (identx) `=` ((ty..l =*= ty..r))
      ---
      judge R : entails = env ::- ty..l =*= ty..r ~> identx

  rule e.subsume.left "SubsumeLeft" =
    view G =
      judge B : entails = env ::- (ty..f ty..a) =*= (ty..g ty..b)
      ---
      judge R : entails = env ::- ty..f =*= ty..g
    view T =
      judge B : entails = env ::- (ty..f ty..a) =*= (ty..g ty..b) ~> coe
      ---
      judge R : entails = env ::- ty..f =*= ty..g ~> (left coe)
  
  rule e.subsume.right "SubsumeRight" =
    view G =
      judge B : entails = env ::- (ty..f ty..a) =*= (ty..g ty..b)
      ---
      judge R : entails = env ::- ty..a =*= ty..b
    view T =
      judge B : entails = env ::- (ty..f ty..a) =*= (ty..g ty..b) ~> coe
      ---
      judge R : entails = env ::- ty..a =*= ty..b ~> (right coe)
  
  rule e.congr "Congruence" =
    view G =
      judge F : entails = env ::- ty..f =*= ty..g
      judge A : entails = env ::- ty..a =*= ty..b
      ---
      judge R : entails = env ::- (ty..f ty..a) =*= (ty..g ty..b)
    view T =
      judge F : entails = env ::- ty..f =*= ty..g ~> coe..f
      judge A : entails = env ::- ty..a =*= ty..b ~> coe..a
      ---
      judge R : entails = env ::- (ty..f ty..a) =*= (ty..g ty..b) ~> (coe..f coe..a)
  
  rule e.univ "Univ" =
    view G =
      judge B : entails = env ::- ty..l =*= ty..r
      judge U1 : notelemftv = !env(alpha.i)
      ---
      judge R : entails = env ::- (forall alpha..._ dot ty..l) =*= (forall alpha..._ dot ty..r)
    view T =
      ---
      judge R : entails = env ::- (forall alpha..._ dot ty..l) =*= (forall alpha..._ dot ty..r) ~> (forall alpha..._ dot coe)
  
  rule e.inst "Inst" =
    view G =
      judge B : entails = env ::- (forall^alpha^dot ty..l) =*= (forall^beta^dot ty..r)
--      judge K1 : kind = env :- ty
      ---
      judge R : entails = env ::- ((subst ty alpha) ty..l) =*= ((subst ty beta) ty..r)
    view T =
      ---
      judge R : entails = env ::- ((subst ty alpha) ty..l) =*= ((subst ty beta) ty..r) ~> (coe @ ty)


relation lookup =
  view F =
    holes [ nm: Name, env: Gam | | ty: Type ]
    judgespec env(nm) `=` ty

relation insert =
  view F =
    holes [ nm: Name, ty: Type | | env: Gam ]
    judgespec env(nm) `=` ty

relation elem =
  view F =
    holes [ nm: Name, env: Gam | | ]
    judgespec env(nm)
    judgeuse tex nm `elem` env

relation notelemftv =
  view FE =
    holes [ nm: Name, env: Gam | | ]
    judgespec !env(nm)
    judgeuse tex nm notelem ftv(env)

relation emptyintersection =
  view FE =
    holes [ ty: Type , env: Gam, env.g: Gam | | ]
    judgespec ty >< env <== env.g
    judgeuse tex ftv(ty) >< ftv(env) <== ftv(env.g)

relation equalty =
  view G =
    holes [ tya: Type, tyb : Type | | ]
    judgespec tya `=` tyb

relation unify =
  view G =
    holes [ tya : Type, tyb : Type | | theta : Substitution ]
    judgespec theta `=` tya == tyb
    judgeuse tex theta `=` Uni (tya, tyb)


relation ass "Assumption" =
  view C =
    holes [ nm: Name, pred : Pred | | sc : Scope ]
    judgespec nm : pred sc
    judgeuse tex (sub(Ass)(nm)) ^^^ ^^^ pred (brack (sc))

relation prv "Prove" =
  view C =
    holes [ nm: Name, pred : Pred | | sc : Scope ]
    judgespec nm : pred sc
    judgeuse tex (sub(Prv)(nm)) ^^^ ^^^ pred (brack (sc))

relation grd "Guard" =
  view C =
    holes [ expr : Guard | | ]
    judgespec expr
    judgeuse tex expr

relation chr "CHRs" =
  view C =
    holes [ x : Pred, y : Pred, coe' : Coercion' | | ]
    judgespec x y coe'
    judgeuse tex Red ^^^ ^^^ x (sub (~>) (coe')) y

ruleset chr.base scheme chr "Entailment expressed with CHRs" =
  rule a.sym "AssSym" =
    view C =
      judge A1 : ass = x : (ty..a =*= ty..b) sc
      ---
      judge A2 : ass = y : (ty..b =*= ty..a) sc
      judge R1 : chr = x y ((\coe dot sym coe))

  rule a.trans "AssTrans" =
    view C =
      judge A1 : ass = x : (ty..a =*= ty..b) sc1
      judge A2 : ass = y : (ty..b =*= ty..c) sc2
      judge G1 : grd = ((sc1 sc2) `visible` sc3)
      ---
      judge A3 : ass = z : (ty..a =*= ty..c) sc3
      judge R1 : chr = (x, y) z transcoe
  
  rule a.congr "AssCongr" =
    view C =
      judge A1 : ass = x : (ty..a =*= ty..b) sc
      judge G1 : grd = ((substitution, (overline p), _, coe') `=` Uni ty..a ty..b)
      ---
      judge A2 : ass = y : ((substitution (overline p))) sc
      judge R1 : chr = x y coe'
  

  rule p.sym "PrvSym" =
    view C =
      judge A1 : prv = x : (ty..a =*= ty..b) sc
      ---
      judge A2 : prv = y : (ty..b =*= ty..a) sc
      judge R1 : chr = x y ((\coe dot sym coe))

  rule p.trans "PrvTrans" =
    view C =
      judge P1 : prv = x : (ty..a =*= ty..b) sc1
      judge A1 : ass = y : (ty..b =*= ty..c) sc2
      judge G1 : grd = (sc2 `visible` sc1)
      ---
      judge P2 : prv = z : (ty..a =*= ty..c) sc1
      judge R1 : chr = (x, y) z transcoe
  
  rule p.congr "PrvCongr" =
    view C =
      judge P1 : prv = x : (ty..a =*= ty..b) sc
      judge G1 : grd = ((substitution, (overline p), (overline coe'), _) `=` Uni ty..a ty..b)
      ---
      judge P2 : prv = y : ((substitution (overline p))) sc
      judge R1 : chr = x y (overline coe')

  rule p.assume "PrvAss" =
    view C =
      judge P1 : prv = x : (ty..a =*= ty.b) sc1
      judge A1 : ass = y : (ty..a =*= ty.b) sc2
      judge G1 : grd = (sc2 `visible` sc1)
      ---
      judge R1 : chr = x y ((lookup x))
  
{-
  rule p.nil "PrvNil" =
    view C =
      judge P1 : prv = x : (()) sc
      ---
      judge R1 : chr = x (()) nil

  rule p.unpack "PrvUnpack" =
    view C =
      judge P1 : prv = x : ((p (overline ps))) sc
      ---
      judge P2 : prv = y : p sc
      judge P3 : prv = z : (overline(ps)) sc
      judge R1 : chr = x (y z) unpack
-}


relation spine "Spine" =
  view T =
    holes [ ty..a : Ty, ty..b : Ty, coeIn..._ : Coercion, coeIn : Coercion, env : Gam | | coe : Coercion, coeOut..._ : Coercion ]
    judgespec coeIn ; coeIn..._ ; env :- ty..a ~~ ty..b ~> coe ; coeOut..._
    judgeuse tex coeIn ; coeIn..._ ; env :-."s" ty..a ~~ ty..b ~> coe ; coeOut..._

ruleset spine.base scheme spine "Coercion construction and deconstruction by spine" =
  rule s.app "App" =
    view T =
      judge F : spine = coeIn..i ; coeIn..il._ ; env :- ty..f ~~ ty..g ~> coe..l ; coeOut..l._
      judge A : spine = coeIn..i ; coeIn..ir._ ; env :- ty..b ~~ ty..a ~> coe..r ; coeOut..r._
      ---
      judge R : spine = coeIn..i ; (coeIn..il._ coeIn..ir._) ; env :- (ty..f ty..a) ~~ (ty..g ty..b) ~> (coe..l coe..r) ; ((left coeOut..l)..._ ^^^ (right coeOut..r)..._)

  rule s.univ "Univ" =
    view T =
      judge B : spine = coeIn..i ; coeIn..i._ ; env :- ty..a ~~ ty..b ~> coe..._ ; coe
      judge E : notelemftv = !env(v)
      ---
      judge R : spine = coeIn..i ; coeIn..i._ ; env :- (forall^alpha^dot ty..a) ~~ (forall^alpha^dot ty..b) ~> (coe @ alpha)..._ ; (forall^alpha^dot coe)

  rule s.refl "Refl" =
    view T =
      ---
      judge R : spine = (_ ^^^) ; emptyset ; env :- ty ~~ ty ~> emptyset ; ty
  
  rule s.uneq "Unequal" =
    view T =
      ---
      judge R : spine = coeIn..i ; coe ; env :- ty..a ~~ ty..b ~> coeIn..i ; coe


scheme coercion "Coercion" =
  view T =
    holes [ node coe : Coercion, env : Environment | | ty..a : Type, ty..b : Type ]
    judgespec env :- coe : ty..a ~ ty..b
    judgeuse tex env :-."c" coe : ty..a ~ ty..b

ruleset coercion.base scheme coercion "Coercion type rules" =
  rule c.var "Var" =
    view T =
      judge L : lookup = env(identx) `=` (ty..a ~ ty..b)
      ---
      judge R : coercion = env :- identx : ty..a ~ ty..b
  
  rule c.app "App" =
    view T =
      judge F : coercion = env :- coe..f : ty..f ~ ty..g
      judge A : coercion = env :- coe..a : ty..a ~ ty..b
      ---
      judge R : coercion = env :- coe..f coe..a : (ty..f ty..a) ~ (ty..g ty..b)

  rule c.refl "Refl" =
    view T =
      ---
      judge R : coercion = env :- ty : ty ~ ty

  rule c.sym "Sym" =
    view T =
      judge B : coercion = env :- coe : ty..b ~ ty..a
      ---
      judge R : coercion = env :- sym coe : ty..a ~ ty..b

  rule c.trans "Trans" =
    view T =
      judge Q : coercion = env :- coe..q : ty..a ~ ty..b
      judge P : coercion = env :- coe..p : ty..b ~ ty..c
      ---
      judge R : coercion = env :- coe..p compose coe..q : ty..a ~ ty..c

  rule c.left "Left" =
    view T =
      judge B : coercion = env :- coe : (ty..f ty..a) ~ (ty..g ty..b)
      ---
      judge R : coercion = env :- left coe : ty..f ~ ty..g

  rule c.right "Right" =
    view T =
      judge B : coercion = env :- coe : (ty..f ty..a) ~ (ty..g ty..b)
      ---
      judge R : coercion = env :- right coe : ty..a ~ ty..b

  rule c.univ "Univ" =
    view T =
      judge B : coercion = env :- coe : ty..a ~ ty..b
      judge E : notelemftv = !env(alpha)
      ---
      judge R : coercion = env :- (forall^alpha dot coe) : (forall^alpha dot ty..a) ~ (forall^alpha dot ty..b)

  rule c.inst "Inst" =
     view T =
       judge B : coercion = env :- coe : (forall^alpha dot ty..a) ~ (forall^beta dot ty..b)
       ---
       judge R : coercion = env :- (coe @ ty) : ((subst ty alpha) ty..a) ~ ((subst ty beta) ty..b)


scheme expr' "Expr'" =
  view T =
    holes [ node e : Expr', env : Env | | ty' : Type ]
    judgespec env :- e' : ty'
    judgeuse tex env :-."e'" e' : ty'

ruleset expr'.base scheme expr' "Expression type rules" =
  rule e.cast "Cast" =
    view T =
      judge B : expr' = env :- e' : ty''..a
      judge C : coercion = env :- coe : ty''..a ~ ty''..b
      ---
      judge R : expr' = env :- (e' ^^^ :> ^^^ coe) : ty''..b

  rule e.app.coe "AppCoe" =
    view T =
      judge B : expr' = env :- e' : (coe -> ty'')
      ---
      judge R : expr' = env :- (e' coe) : ty''


relation lift "Lift" =
  view T =
    holes [ coes : Coes | | coe : Coe ]
    judgespec coes ~> coe
    judgeuse tex coe `=` lift ^^^ coes

relation decompose "Decompose" =
  view T =
    holes [ coe : Coe | | coes : Coes ]
    judgespec coe ~> coes
    judgeuse tex coes `=` decompose ^^^ coe