dk_machine_int.dk

#NAME dk_machine_int.
def Bool : Type := dk_bool.Bool.

def UNat : Type := dk_nat.Nat.
def UO : UNat := dk_nat.O.
def US : UNat -> UNat := dk_nat.S.

Mint : UNat -> cc.uT.
MInt : UNat -> Type.
[N] cc.eT (Mint N) --> MInt N.

O : MInt UO.
S0 : N : UNat -> MInt N -> MInt (US N).
S1 : N : UNat -> MInt N -> MInt (US N).

def zero : N : UNat -> MInt N.
[] zero dk_nat.O --> O
[N] zero (dk_nat.S N) --> S0 N (zero N).

def bound : N : UNat -> MInt N.
[] bound dk_nat.O --> O
[N] bound (dk_nat.S N) --> S1 N (bound N).

(; cast ;)
def downcast : N : UNat -> MInt (US N) -> MInt N.
[]    downcast dk_nat.O _ --> O
[N,n] downcast (dk_nat.S _) (S0 (dk_nat.S N) n) --> S0 N (downcast N n)
[N,n] downcast (dk_nat.S _) (S1 (dk_nat.S N) n) --> S1 N (downcast N n).

def double (N : UNat) (n : MInt N) : MInt N := downcast N (S0 N n).

def succ : N : UNat -> MInt N -> MInt N.
[] succ dk_nat.O O --> O
[N,n] succ (dk_nat.S _) (S0 N n) --> S1 N n
[N,n] succ (dk_nat.S _) (S1 N n) --> S0 N (succ N n).

def pred : N : UNat -> MInt N -> MInt N.
[] pred dk_nat.O O --> O
[N,n] pred (dk_nat.S _) (S1 N n) --> S0 N n
[N,n] pred (dk_nat.S _) (S0 N n) --> S1 N (pred N n).

def plus : N : UNat -> MInt N -> MInt N -> MInt N.
[]  plus dk_nat.O O O --> O
[N,n,m]
    plus (dk_nat.S N) (S0 _ n) (S0 _ m) --> S0 N (plus N n m)
[N,n,m]
    plus (dk_nat.S N) (S0 _ n) (S1 _ m) --> S1 N (plus N n m)
[N,n,m]
    plus (dk_nat.S N) (S1 _ n) (S0 _ m) --> S1 N (plus N n m)
[N,n,m]
    plus (dk_nat.S N) (S1 _ n) (S1 _ m) --> S0 N (succ N (plus N n m)).

def complement : N : UNat -> MInt N -> MInt N.
[] complement dk_nat.O O --> O
[N,n] complement (dk_nat.S N) (S0 _ n) --> S1 N (complement N n)
[N,n] complement (dk_nat.S N) (S1 _ n) --> S0 N (complement N n).

def opp : N : UNat -> MInt N -> MInt N.
[N,n] opp N n --> succ N (complement N n).

def sub : N : UNat -> MInt N -> MInt N -> MInt N.
[N,n,m] sub N n m --> plus N n (opp N m).

(; Product ;)
def mult : N : UNat -> MInt N -> MInt N -> MInt N.
[ ] mult dk_nat.O O O --> O
[N,n,m]
    mult (dk_nat.S N) (S0 _ n) (S0 _ m)
      -->
    double (US N) (S0 N (mult N n m))
[N,n,m]
    mult (dk_nat.S N) (S0 _ n) (S1 _ m)
      -->
    S0 N (plus N m (double N (mult N n m)))
[N,n,m]
    mult (dk_nat.S N) (S1 _ n) (S0 _ m)
      -->
    S0 N (plus N n (double N (mult N n m)))
[N,n,m]
    mult (dk_nat.S N) (S1 _ n) (S1 _ m)
      -->
    S1 N (plus N (double N (mult N m n)) (plus N n m)).

(; equality ;)
def equal : N : UNat -> MInt N -> MInt N -> Bool.
(; [n] equal _ n n --> dk_bool.true ;)
[] equal _ O O --> dk_bool.true
[N,n,m]
    equal (dk_nat.S N) (S0 _ n) (S0 _ m) --> equal N n m
[N,n,m]
    equal (dk_nat.S N) (S1 _ n) (S1 _ m) --> equal N n m
[]
    equal (dk_nat.S _) (S0 _ _) (S1 _ _) --> dk_bool.false
[]
    equal (dk_nat.S _) (S1 _ _) (S0 _ _) --> dk_bool.false.

(; unsigned comparison ;)
def unsigned_lt : N : UNat -> MInt N -> MInt N -> Bool.
def unsigned_leq : N : UNat -> MInt N -> MInt N -> Bool.

[] unsigned_lt dk_nat.O O O --> dk_bool.false
[N,n,m]
    unsigned_lt (dk_nat.S N) (S0 _ n) (S0 _ m)
      -->
    unsigned_lt N n m
[N,n,m]
    unsigned_lt (dk_nat.S N) (S1 _ n) (S1 _ m)
      -->
    unsigned_lt N n m
[N,n,m]
    unsigned_lt (dk_nat.S N) (S0 _ n) (S1 _ m)
      -->
    unsigned_leq N n m
[N,n,m]
    unsigned_lt (dk_nat.S N) (S1 _ n) (S0 _ m)
      -->
    unsigned_lt N n m.

[] unsigned_leq dk_nat.O O O --> dk_bool.true
[N,n,m]
    unsigned_leq (dk_nat.S N) (S0 _ n) (S0 _ m)
      -->
    unsigned_leq N n m
[N,n,m]
    unsigned_leq (dk_nat.S N) (S1 _ n) (S1 _ m)
      -->
    unsigned_leq N n m
[N,n,m]
    unsigned_leq (dk_nat.S N) (S0 _ n) (S1 _ m)
      -->
    unsigned_leq N n m
[N,n,m]
    unsigned_leq (dk_nat.S N) (S1 _ n) (S0 _ m)
      -->
    unsigned_lt N n m.

def unsigned_gt : N : UNat -> MInt N -> MInt N -> Bool
                := N : UNat => n : MInt N => m : MInt N => unsigned_lt N m n.

def unsigned_geq : N : UNat -> MInt N -> MInt N -> Bool
                 := N : UNat => n : MInt N => m : MInt N => unsigned_leq N m n.

(; signed comparison ;)
def positive : N : UNat -> MInt N -> Bool.
[] positive dk_nat.O O --> dk_bool.true
[] positive (dk_nat.S dk_nat.O) (S0 dk_nat.O O) --> dk_bool.true
[] positive (dk_nat.S dk_nat.O) (S1 dk_nat.O O) --> dk_bool.false
[N,n] positive (dk_nat.S N) (S0 _ n) --> positive N n
[N,n] positive (dk_nat.S N) (S1 _ n) --> positive N n.

def signed_leq : N : UNat ->
                 n : MInt N ->
                 m : MInt N ->
                 Bool
               :=
                 N : UNat =>
                 n : MInt N =>
                 m : MInt N =>
                 dk_bool.iteb (dk_bool.and
                                (positive N m)
                                (dk_bool.not (positive N n)))
                              dk_bool.true
                                (dk_bool.iteb (dk_bool.and
                                                (positive N n)
                                                (dk_bool.not (positive N m)))
                                              dk_bool.false
                                                (positive N (sub N m n))).

def signed_geq : N : UNat ->
                 n : MInt N ->
                 m : MInt N ->
                 Bool
               :=
                 N : UNat =>
                 n : MInt N =>
                 m : MInt N =>
                 signed_leq N m n.

def signed_lt : N : UNat ->
                n : MInt N ->
                m : MInt N ->
                Bool
              :=
                N : UNat =>
                n : MInt N =>
                m : MInt N =>
                dk_bool.not (signed_geq N m n).

def signed_gt : N : UNat ->
                n : MInt N ->
                m : MInt N ->
                Bool
              :=
                N : UNat =>
                n : MInt N =>
                m : MInt N =>
                dk_bool.not (signed_leq N m n).

(; Casting Peano natural numbers ;)
def cast_peano : N : UNat -> n : UNat -> MInt N.
[N] cast_peano N dk_nat.O --> zero N
[N,n] cast_peano N (dk_nat.S n) --> succ N (cast_peano N n).

(; Casting binary natural numbers ;)

def cast_bnat : N : UNat -> bn : dk_binary_nat.BNat -> MInt N.
[N] cast_bnat N dk_binary_nat.O --> zero N
[ ] cast_bnat dk_nat.O _ --> O.
[N,bn]
    cast_bnat (dk_nat.S N) (dk_binary_nat.S0 bn)
      -->
    S0 N (cast_bnat N bn)
[N,bn]
    cast_bnat (dk_nat.S N) (dk_binary_nat.S1 bn)
      -->
    S1 N (cast_bnat N bn).