#lang pie

(claim list1
  (List Nat))
(define list1
  (:: 1
    (:: 2
      (:: 3 nil))))

(claim list2
  (List Nat))
(define list2
  (:: 4
    (:: 5
      (:: 6 nil))))

(claim list3
  (List Atom))
(define list3
  (:: 'eleeins
    (:: 'elezwei
      (:: 'eledrei nil))))

(claim list4
  (List Atom))
(define list4
  (:: 'elevier
    (:: 'elefünf
      (:: 'elesechs nil))))

(claim append ;(append Nat list1 list2) -> für listen mit listen zusammenfügen / (append Atom list3 list4)
  (Pi ((E U))
    (-> (List E)
        (List E)
        (List E))))
(define append
  (lambda (E start end)
    (rec-List start
      end
      (lambda (e es rec)
        (:: e rec)))))

(claim snoc ;(snoc Nat list1 4) -> für listen mit Nat zusammenfügen / (snoc Atom list3 'pie)
  (Pi ((E U))
    (-> (List E) E
        (List E))))
(define snoc
  (lambda (E list end)
    (rec-List list
      (:: end nil)
      (lambda (e es rec)
        (:: e rec)))))

(claim concat
  (Pi ((E U))
    (-> (List E)(List E)
        (List E))))

(claim step-concat
  (Pi((E U ))
    (-> E (List E) (List E)
        (List E))))

(define step-concat
  (lambda(E)
    (lambda(e es concat)
      (snoc E concat e))))

(define concat ;(concat Nat list1 list2) dabei wird hintere liste immer umgedreht
  (lambda(E)
    (lambda(start end)
      (rec-List end
        start
        (step-concat E)))))

(claim reverse
  (Pi ((E U))
    (-> (List E)
        (List E))))

(claim step-reverse
  (Pi((E U ))
    (-> E (List E) (List E)
        (List E))))
  

(define step-reverse
  (lambda(E)
    (lambda(e es reverse)
      (snoc E reverse e))))

(define reverse ;(reverse Nat list1)
  (lambda(E)
    (lambda(es)
      (rec-List es
        (the(List E)nil)
        (step-reverse E)))))


(claim correct-concat
  (Pi ((E U))
    (-> (List E)(List E)
        (List E))))
(define correct-concat
  (lambda (E start end)
    (concat E start (reverse E end))))



(claim map
  (Pi ((A U)
       (B U))
    (-> (-> A B)
        (List A)
        (List B))))
(define map ;(map Nat Nat (lambda(y)(add1 y)) list1)
  (lambda (A B f l)
    (rec-List l
      (the (List B) nil)
      (lambda (e es rec)
        (:: (f e) rec)))))








(claim vec1
  (Vec Nat 3))
(define vec1
  (vec:: 1
    (vec:: 2
      (vec:: 3 vecnil))))


(claim vec2
  (Vec Nat 4))
(define vec2
  (vec:: 4
    (vec:: 3
      (vec:: 2
        (vec:: 1 vecnil)))))


(claim first ;(first Nat 2 vec1) / (first Nat 3 vec2)
    (Pi ((E U)
         (l Nat))
        (-> (Vec E (add1 l))
            E)))
(define first
  (lambda (E l)
    (lambda (vec)
      (head vec))))

(claim rest ;(rest Nat 2 vec1) / (rest Nat 3 vec2)
    (Pi ((E U)
         (l Nat))
        (-> (Vec E (add1 l))
           (Vec E l))))
(define rest
  (lambda (E l)
    (lambda (vec)
      (tail vec))))

        
      

(claim + (-> Nat Nat Nat))
(define + (lambda (x y)(iter-Nat x y (lambda (a) (add1 a)))))


(claim sub1 (-> Nat Nat))
(define sub1 (lambda (a) (rec-Nat a 0 (lambda (n-1 akk) n-1))))


(claim - (-> Nat Nat Nat))
(define - (lambda (x y) (iter-Nat y x (lambda (a) (sub1 a)))))


(claim first-nats ;(first-nats 5)
  (Pi ((n Nat))
    (Vec Nat n)))
(define first-nats
  (lambda (n)
    (ind-Nat n
      (lambda (x) (Vec Nat x))
      vecnil
      (lambda (n-1 first_n-1)
        (vec:: (add1 n-1) first_n-1)))))

(claim count-from ;(count-from 1 10) von 1 zehn drauf
  (Pi ((start Nat)
       (n Nat))
    (Vec Nat n)))
(define count-from
  (lambda (start n)
    (ind-Nat n
      (lambda (x) (Vec Nat x))
      vecnil
      (lambda (n-1 rec)
        (vec:: (sub1 (- (+ start n) n-1)) rec)))))


(claim also-rec-Nat
  (Pi ((X U))
    (-> Nat
        X
        (-> Nat X
            X)
        X)))
(define also-rec-Nat ; k ist dim wird also ignoriert
  (lambda (X)
    (lambda (target base step)
      (ind-Nat target
        (lambda (k) X)
        base
        step))))