--------------------------------------------------------------------------------------- ( n : Nat ! data (---------! where (------------! ; !-------------! ! Nat : * ) ! zero : Nat ) ! suc n : Nat ) --------------------------------------------------------------------------------------- let (-----------! ! one : Nat ) one => suc zero --------------------------------------------------------------------------------------- let (-----------! ! two : Nat ) two => suc one --------------------------------------------------------------------------------------- let (-------------! ! three : Nat ) three => suc two --------------------------------------------------------------------------------------- ( x, y : Nat ! let !---------------! ! add x y : Nat ) add x y <= rec x { add x y <= case x { add zero y => y add (suc n) y => suc (add n y) } } --------------------------------------------------------------------------------------- data (----------! where (-------------! ; (--------------! ! Bool : * ) ! true : Bool ) ! false : Bool ) --------------------------------------------------------------------------------------- ( b : Bool ; t, e : A ! let !----------------------! ! if b t e : A ) if b t e <= case b { if true t e => t if false t e => e } --------------------------------------------------------------------------------------- ( A : * ! ( a : A ! data !-------------! where !----------------! ; (-----------------! ! Error A : * ) ! ok a : Error A ) ! error : Error A ) --------------------------------------------------------------------------------------- ( b : Bool ! ( n : Nat ! ( c, t, e : Tm ! ( t, u : Tm ! data (------! where !----------! ; !----------! ; !--------------! ; !-----------! ! Tm ! ! bconst b ! ! nconst n ! ! ifElse c t e ! ! plus t u ! ! : * ) ! : Tm ) ! : Tm ) ! : Tm ) ! : Tm ) --------------------------------------------------------------------------------------- ( b : Bool ! let !-----------! ! p1 b : Tm ) p1 b => ifElse (bconst b) (plus (nconst one) (nconst one)) (nconst zero) --------------------------------------------------------------------------------------- let (---------! ! p2 : Tm ) p2 => ifElse (plus (nconst one) (nconst one)) (bconst true) (nconst zero) --------------------------------------------------------------------------------------- ( b : Bool ! ( n : Nat ! data (---------! where !--------------! ; !--------------! ! Val : * ) ! bval b : Val ) ! nval n : Val ) --------------------------------------------------------------------------------------- ( cv, tv, ev : Error Val ! let !-----------------------------! ! evalIf cv tv ev : Error Val ) evalIf cv tv ev <= case cv { evalIf (ok a) tv ev <= case a { evalIf (ok (bval b)) tv ev <= case b { evalIf (ok (bval true)) tv ev => tv evalIf (ok (bval false)) tv ev => ev } evalIf (ok (nval n)) tv ev => error } evalIf error tv ev => error } --------------------------------------------------------------------------------------- ( tv, uv : Error Val ! let !----------------------------! ! evalPlus tv uv : Error Val ) evalPlus tv uv <= case tv { evalPlus (ok a) uv <= case uv { evalPlus (ok a') (ok a) <= case a' { evalPlus (ok (bval b)) (ok a) => error evalPlus (ok (nval n)) (ok a) <= case a { evalPlus (ok (nval n)) (ok (bval b)) => error evalPlus (ok (nval n')) (ok (nval n)) => ok (nval (add n' n)) } } evalPlus (ok a) error => error } evalPlus error uv => error } --------------------------------------------------------------------------------------- ( t : Tm ! let !--------------------! ! eval t : Error Val ) eval t <= rec t { eval t <= case t { eval (bconst b) => ok (bval b) eval (nconst n) => ok (nval n) eval (ifElse c t e) => evalIf (eval c) (eval t) (eval e) eval (plus t u) => evalPlus (eval t) (eval u) } } --------------------------------------------------------------------------------------- inspect eval (p1 true) => ok (nval (suc (suc zero))) : Error Val --------------------------------------------------------------------------------------- inspect eval p2 => error : Error Val --------------------------------------------------------------------------------------- data (--------! where (-----------! ; (----------! ! Ty : * ) ! bool : Ty ) ! nat : Ty ) --------------------------------------------------------------------------------------- ( c : TM bool ! ( a : ! ! ! ( t, u : ! ! Ty ! ( b : Bool ! ( n : Nat ! ! t, e : TM a ! ! TM nat ! data !------! where !-----------! ; !----------! ; !--------------! ; !-----------! ! TM a ! ! Bconst b ! ! Nconst n ! ! IfElse c t e ! ! Plus t u ! ! : * ) ! : TM ! ! : TM ! ! : TM a ) ! : TM nat ) ! % bool ) ! % nat ) --------------------------------------------------------------------------------------- ( a : Ty ! ( b : Bool ! ( n : Nat ! data !-----------! where !-------------------! ; !------------------! ! VAL a : * ) ! Bval b : VAL bool ) ! Nval n : VAL nat ) --------------------------------------------------------------------------------------- ( cv : VAL bool ; tv, ev : VAL a ! let !---------------------------------! ! EvalIf cv tv ev : VAL a ) EvalIf cv tv ev <= case cv { EvalIf (Bval b) tv ev <= case b { EvalIf (Bval true) tv ev => tv EvalIf (Bval false) tv ev => ev } } --------------------------------------------------------------------------------------- ( tv, uv : VAL nat ! let !--------------------------! ! EvalPlus tv uv : VAL nat ) EvalPlus tv uv <= case tv { EvalPlus (Nval n) uv <= case uv { EvalPlus (Nval n') (Nval n) => Nval (add n' n) } } --------------------------------------------------------------------------------------- ( t : TM a ! let !----------------! ! Eval t : VAL a ) Eval t <= rec t { Eval t <= case t { Eval (Bconst b) => Bval b Eval (Nconst n) => Nval n Eval (IfElse c t e) => EvalIf (Eval c) (Eval t) (Eval e) Eval (Plus t u) => EvalPlus (Eval t) (Eval u) } } --------------------------------------------------------------------------------------- ( t : TM a ! let !------------! ! fog t : Tm ) fog t <= rec t { fog t <= case t { fog (Bconst b) => bconst b fog (Nconst n) => nconst n fog (IfElse c t e) => ifElse (fog c) (fog t) (fog e) fog (Plus t u) => plus (fog t) (fog u) } } --------------------------------------------------------------------------------------- ( t : Tm ! ( a : Ty ; t : TM a ! data !--------------! where !-------------------------! ; (-------------------! ! TCheck t : * ) ! tc a t : TCheck (fog t) ) ! terror : TCheck t ) --------------------------------------------------------------------------------------- ( cc : TCheck c ; ct : TCheck t ; ce : TCheck e ! let !-------------------------------------------------! ! checkIf cc ct ce : TCheck (ifElse c t e) ) checkIf cc ct ce <= case cc { checkIf (tc a c) ct ce <= case a { checkIf (tc bool c) ct ce <= case ct { checkIf (tc bool c) (tc a t) ce <= case ce { checkIf (tc bool c) (tc a' t) (tc a e) <= case a' { checkIf (tc bool c) (tc bool t) (tc a e) <= case a { checkIf (tc bool c) (tc bool t) (tc bool e) => tc bool (IfElse c t e) checkIf (tc bool c) (tc bool t) (tc nat e) => terror } checkIf (tc bool c) (tc nat t) (tc a e) <= case a { checkIf (tc bool c) (tc nat t) (tc bool e) => terror checkIf (tc bool c) (tc nat t) (tc nat e) => tc nat (IfElse c t e) } } checkIf (tc bool c) (tc a t) terror => terror } checkIf (tc bool c) terror ce => terror } checkIf (tc nat c) ct ce => terror } checkIf terror ct ce => terror } --------------------------------------------------------------------------------------- ( ct : TCheck t ; cu : TCheck u ! let !---------------------------------! ! checkPlus ct cu : TCheck (plus t u) ) checkPlus ct cu <= case ct { checkPlus (tc a t) cu <= case cu { checkPlus (tc a' t) (tc a u) <= case a' { checkPlus (tc bool t) (tc a u) => terror checkPlus (tc nat t) (tc a u) <= case a { checkPlus (tc nat t) (tc bool u) => terror checkPlus (tc nat t) (tc nat u) => tc nat (Plus t u) } } checkPlus (tc a t) terror => terror } checkPlus terror cu => terror } --------------------------------------------------------------------------------------- ( t : Tm ! let !---------------------! ! tcheck t : TCheck t ) tcheck t <= rec t { tcheck t <= case t { tcheck (bconst b) => tc bool (Bconst b) tcheck (nconst n) => tc nat (Nconst n) tcheck (ifElse c t e) => checkIf (tcheck c) (tcheck t) (tcheck e) tcheck (plus t u) => checkPlus (tcheck t) (tcheck u) } } ---------------------------------------------------------------------------------------