------------------------------------------------------------------------------ ( n : Nat ! data (---------! where (------------! ; !-------------! ! Nat : * ) ! zero : Nat ) ! suc n : Nat ) ------------------------------------------------------------------------------ ( n : Nat ! ( i : Fin n ! data !-----------! where (------------------! ; !--------------------! ! Fin n : * ) ! fz : Fin (suc n) ) ! fs i : Fin (suc n) ) ------------------------------------------------------------------------------ ( S, T : Ty ! data (--------! where (----------! ; !--------------! ! Ty : * ) ! nat : Ty ) ! arr S T : Ty ) ------------------------------------------------------------------------------ ( n : Nat ! data !-----------! ! Raw n : * ) ( i : Fin n ! where !----------------! ! varR i : Raw n ) ( f, s : Raw n ! !------------------! ! appR f s : Raw n ) ( S : Ty ; b : Raw (suc n) ! ( T : Ty ! !---------------------------! ; (-------! ; (-------! ; !---------! ! ldaR S b : Raw n ) ! zeR : ! ! suR : ! ! precR T ! ! Raw ! ! Raw ! ! : Raw ! ! % n ) ! % n ) ! % n ) ------------------------------------------------------------------------------ let (----------------! ! add : Raw zero ) add => ldaR nat (ldaR nat (appR (appR (appR (precR nat) (varR fz))!!! ! ! !% (ldaR nat suR) )!! ! !% (varR (fs fz)) )) ------------------------------------------------------------------------------ ( n : Nat ! ( Gam : Ctx n ; T : Ty ! data !-----------! where (-----------------! ; !--------------------------! ! Ctx n : * ) ! empC : Ctx zero ) ! extC Gam T : Ctx (suc n) ) ------------------------------------------------------------------------------ ( G : Ctx n ! ! ! ! T : Ty ! ( i : Var G T ! data !-----------! where (--------------------! ; !--------------------! ! Var G T ! ! vz : ! ! vs i : ! ! : * ) ! Var (extC G T) T ) ! Var (extC G S) T ) ------------------------------------------------------------------------------ ( G : Ctx n ; T : Ty ! data !---------------------! ! Tm G T : * ) ( i : Var G T ! where !----------------! ! var i : Tm G T ) ( f : Tm G (arr S T) ; s : Tm G S ! !----------------------------------! ! app f s : Tm G T ) ( b : Tm (extC G S) T ! !------------------------! ! lda b : Tm G (arr S T) ) (---------------! ! ze : Tm G nat ) (------------------! ; (------------------------------------------! ! su : ! ! prec T : ! ! Tm G (arr nat! ! ! Tm G (arr T (arr (arr nat (arr T T))!! ! ! !% nat ) ) ! ! !% (arr nat T) )) ) ------------------------------------------------------------------------------ ( G : Ctx n ; i : Var G T ! let !--------------------------! ! fVar G T i : Fin n ) fVar G T i <= rec i { fVar G T x <= case x { fVar (extC G T) T vz => fz fVar (extC G S) T (vs i) => fs (fVar ? ? i) } } ------------------------------------------------------------------------------ ( G : Ctx n ; i : Fin n ! ( i : Var G t ! data !------------------------! where !-------------------------------! ! VarV G i : * ) ! found i : VarV G (fVar G t i) ) ------------------------------------------------------------------------------ let (---------------------! ! varV G i : VarV G i ) varV G i <= rec G { varV x i <= case x { varV empC i <= case i varV (extC Gam T) i <= case i { varV (extC Gam T) fz => found vz varV (extC Gam T) (fs i) <= view varV Gam i { varV (extC G T) (fs (fVar G t i)) => found (vs i) } } } } ------------------------------------------------------------------------------ ( S : Ty ! data !-------------! ! TyNeq S : * ) ( S, T : Ty ! where !-----------------------! ! tNarr S T : TyNeq nat ) (-------------------------! ! tNnat : TyNeq (arr S T) ) ( S' : TyNeq S ; T, T' : Ty ! ( S : Ty ; T' : TyNeq T ! !-------------------------------! ; !------------------------------! ! tNdom S' T' : TyNeq (arr S T) ) ! tNran S T' : TyNeq (arr S T) ) ------------------------------------------------------------------------------ ( T' : TyNeq S ! let !----------------! ! fNeq S T' : Ty ) fNeq S T' <= rec S { fNeq x T' <= case T' { fNeq nat (tNarr S T) => arr S T fNeq (arr S T) tNnat => nat fNeq (arr S T) (tNdom S' T') => arr (fNeq S S') T' fNeq (arr S T) (tNran S T') => arr S (fNeq T T') } } ------------------------------------------------------------------------------ ( S, T : Ty ! ( T' : TyNeq S ! data !-----------! where (-------------! ; !-----------------------! ! TyEqV S T ! ! tySame : ! ! tyDiff T' : ! ! : * ) ! TyEqV S S ) ! TyEqV S (fNeq S T') ) ------------------------------------------------------------------------------ let (-----------------------! ! tyEqV S T : TyEqV S T ) tyEqV S T <= rec S { tyEqV x T <= case x { tyEqV nat T <= case T { tyEqV nat nat => tySame tyEqV nat (arr S T) => tyDiff (tNarr S T) } tyEqV (arr S T) T' <= case T' { tyEqV (arr S T) nat => tyDiff (tNnat) tyEqV (arr S' T') (arr S T) <= view tyEqV S' S { tyEqV (arr S T') (arr S T) <= view tyEqV T' T { tyEqV (arr S' S) (arr S' S) => tySame tyEqV (arr S' S) (arr S' (fNeq S T')) => tyDiff (tNran S' T') } tyEqV (arr S T'') (arr (fNeq S T') T) => tyDiff (tNdom T' T) } } } } ------------------------------------------------------------------------------ inspect tyEqV (arr nat nat) (arr nat nat) => tySame : TyEqV (arr nat nat) (arr nat nat) ------------------------------------------------------------------------------ inspect tyEqV (arr nat nat) (arr nat (arr nat nat)) => tyDiff (tNran nat (tNarr nat nat)) : TyEqV (arr nat nat) (arr nat (arr nat nat)) ------------------------------------------------------------------------------ ( G : Ctx n ; t : Tm G T ! let !-------------------------! ! fTm T t : Raw n ) fTm T t <= rec t { fTm T x <= case x { fTm T (var i) => varR (fVar ? ? i) fTm T (app f s) => appR (fTm ? f) (fTm ? s) fTm (arr S T) (lda b) => ldaR S (fTm ? b) fTm nat ze => zeR fTm (arr nat nat) su => suR fTm (arr T (arr (arr nat (arr T T)) (arr nat T))) (prec T) => precR T } } ------------------------------------------------------------------------------ ( G : Ctx n ! data !--------------! ! Terror G : * ) ( f : Tm G nat ; s : Tm G S ! where !----------------------------! ! noFun f s : Terror G ) ( f : Tm G (arr S T) ; s : Tm G (fNeq S S') ! !--------------------------------------------! ! mismatch f s : Terror G ) ( b : ! ( G : Ctx n ! ( f : Tm G T ! ! Terror ! ! ! ! ! ! % (extC G S) ! ! f : Terror G ; s : Raw n ! ! s : Terror G ! !----------------! ; !---------------------------! ; !--------------! ! ldaE S b : ! ! appFE f s : Terror G ) ! appSE f s ! ! Terror G ) ! : Terror G ) ------------------------------------------------------------------------------ ( G : Ctx n ; t : Terror G ! let !---------------------------! ! fTerror t : Raw n ) fTerror t <= rec t { fTerror x <= case x { fTerror (noFun f s) => appR (fTm ? f) (fTm ? s) fTerror (mismatch f s) => appR (fTm ? f) (fTm ? s) fTerror (ldaE S b) => ldaR S (fTerror b) fTerror (appFE f s) => appR (fTerror f) s fTerror (appSE f s) => appR (fTm ? f) (fTerror s) } } ------------------------------------------------------------------------------ ( G : Ctx n ! ! ! ! t : Raw n ! ( t : Tm G T ! ( e : Terror G ! data !-----------! where !------------------! ; !--------------------! ! TC G t ! ! good T t : ! ! bad e : ! ! : * ) ! TC G (fTm T t) ) ! TC G (fTerror e) ) ------------------------------------------------------------------------------ let (-----------------! ! tc G t : TC G t ) tc G t <= rec t { tc G x <= case x { tc G (varR i) <= view varV G i { tc G (varR (fVar G t i)) => good ? (var i) } tc G (appR f s) <= view tc G f { tc G (appR (fTm T t) s) <= view tc G s { tc G (appR (fTm T' t') (fTm T t)) <= case T' { tc G (appR (fTm nat t') (fTm T t)) => bad (noFun t' t) tc G (appR (fTm (arr S T) t') (fTm T' t)) <= view tyEqV S T' { tc G (appR (fTm (arr S T) t') (fTm S t)) => good ? (app t' t) tc G (appR (fTm (arr S T) t') (fTm (fNeq S T') t)) => bad (mismatch t' _ T' t) } } tc G (appR (fTm T t) (fTerror e)) => bad (appSE t e) } tc G (appR (fTerror e) s) => bad (appFE e s) } tc G (ldaR S b) <= view tc (extC G S) b { tc G (ldaR S (fTm T t)) => good ? (lda t) tc G (ldaR S (fTerror e)) => bad (ldaE S e) } tc G zeR => good ? ze tc G suR => good ? su tc G (precR T) => good ? (prec T) } } ------------------------------------------------------------------------------ inspect tc empC add => good (arr nat (arr nat nat)) % (lda (lda (app (app (app (prec nat) (var vz)) (lda su))!!! ! ! !% (var (vs vz)) ))) : TC empC (ldaR nat (ldaR nat (appR (appR (appR (precR nat)!!!!! ! ! ! ! !% (varR fz) )!!!! ! ! ! !% (ldaR nat suR) )!!! ! ! !% (varR (fs fz)) ))) ------------------------------------------------------------------------------