vec.hs

import examples/fin;

-- generate a vector of given length from a specified element (replicate)
replicate : forall (n : Nat) . forall (a : Set) (_ : a) . Vec a n;
replicate =
    \ (n : Nat) ->
        elim Nat
            (\ (n : Nat) -> forall (a : Set) (_ : a) . Vec a n )
            (\ (a : Set) (_ : a) -> VNil a )
            (\ (n : Nat) (rec : forall (a : Set) (_ : a) . Vec a n) (a : Set) (x : a) -> VCons a n x (rec a x) )
             n;

-- generate a vector of given length n, containing the natural numbers smaller than n
fromto =
    \ (n : Nat) ->
        elim Nat
            ( \ (n : Nat) -> Vec Nat n )
            ( VNil Nat )
            ( \ (n : Nat) (rec : Vec Nat n) -> VCons Nat n n rec )
            n;

bool_to_prop = \ (x : Bool) -> elim Bool (\ (_ : Bool) -> Set) Falsity Truth x;

-- Zero > _x = False
-- Succ x > Zero = True
-- Succ x > Succ y = x > y
gt = \ (x : Nat) ->
    elim Nat
        (\ (_ : Nat) -> forall (_ : Nat) . Bool)
        (\ (_ : Nat) -> False)
        (\ (x1 : Nat) (rec : forall (_ : Nat) . Bool) (y : Nat) ->
             elim Nat (\ (_ : Nat) -> Bool) True (\ (y1 : Nat) (_ : Bool) -> rec y1) y)
        x;

test1 : Id Bool (gt Zero Zero) False;
test1 = Refl Bool False;

test2 : Id Bool (gt (Succ Zero) Zero) True;
test2 = Refl Bool True;

test3 : Id Bool (gt (Succ (Succ Zero)) (Succ Zero)) True;
test3 = Refl Bool True;

gt_prop = \ (x : Nat) (y : Nat) -> bool_to_prop (gt x y);

--at : forall (A : Set) (i : Nat) (v : )

isEmpty : forall (A : Set) (n : Nat) (v : Vec A n) -> Bool;
isEmpty = \ (A : Set) (n : Nat) (v : Vec A n) ->
    vecElim A (\ (n : Nat) (v : Vec A n) -> Bool)
        True
        (\ (n : Nat) (v : A) (vs : Vec A n) (rec : Bool) -> False )
        n
        v;

$A : Set;
A = $A;

$a : A;

head_aux : forall (n : Nat) (v : Vec A n) (contr: gt_prop n Zero) . A;
head_aux = \ (n : Nat) (v : Vec A n) ->
    vecElim A
        (\ (n : Nat) (_ : Vec A n) -> forall (contr: gt_prop n Zero) . A)
        ( \ (contr : gt_prop Zero Zero) -> abort A contr)
        (\ (n : Nat)
           (v : A)
           (vs : Vec A n)
           (r : forall (contr: gt_prop n Zero) . A)
           (_ : gt_prop (Succ n) Zero) ->
                v)
        n
        v;


head : forall (n : Nat) (v : Vec A (Succ n)) . A;
head = \ (n : Nat) (v : Vec A (Succ n)) -> head_aux (Succ n) v Triv;

at_i : forall (n : Nat) (v : Vec A n) (i : Nat) (contr: gt_prop n i) . A;
at_i = \ (n : Nat) (v : Vec A n) ->
    vecElim A
        (\ (n : Nat) (_ : Vec A n) -> forall (i : Nat) (contr: gt_prop n i) . A)
        (\ (i : Nat) (contr : gt_prop Zero i) -> abort A contr)
        (\ (n : Nat)
           (v : A)
           (vs : Vec A n)
           (rvec : forall (i : Nat) (contr: gt_prop n i) . A)
           (i : Nat) ->
                elim Nat
                    (\ (i : Nat) -> forall (contr : gt_prop (Succ n) i) . A)
                    (\ (_ : gt_prop (Succ n) Zero) -> v)
                    (\ (i : Nat)
                       (_ : forall (contr : gt_prop (Succ n) i) . A)
                       -- see the trick that contr is reused here!!!
                       (contr : gt_prop (Succ n) (Succ i)) ->
                            rvec i contr)
                    i)
        n
        v;

head1 : forall (n : Nat) (v : Vec A (Succ n)) . A;
head1 = \ (n : Nat) (v : Vec A (Succ n)) -> at_i (Succ n) v Zero Triv;