{-# OPTIONS --type-in-type
    #-}

open import NeilPrelude
open import Nat
open import List

module Recursion where

-- Primitive Recursion -----------------------------------------------

listrec : {A : Set}  {P : List A  Set}  P []  ({a : A}  {as : List A}  P as  P (a  as))  Π (List A) P
listrec base step [] = base
listrec {_} {P} base step (_  as) = step (listrec {_} {P} base step as)

listrec' : {A : Set}  {P : List A  Set}  P []  ((a : A)  (as : List A)  P as  P (a  as))  Π (List A) P
listrec' base step = listrec base  {a} {as}  step a as)

-----------------------------------------------------

natrec : {P :   Set}  P O  ({m : }  P m  P (S m))  Π  P
natrec     base step O = base
natrec {P} base step (S n) = step (natrec {P} base step n)

-- Primitive Recursion on two arguments.  I'm not sure if this is the best/right way to do this, but it seems to work

natrec2 : {P :     Set}  ((n : )  P O n)  ((m : )  P m O)  ({m n : }  P m n  P (S m) n  P m (S n)  P (S m) (S n))  (m n : )  P m n
natrec2 baseL baseR step O n = baseL n
natrec2 baseL baseR step m O = baseR m
natrec2 {P} baseL baseR step (S m) (S n) = step (natrec2 {P} baseL baseR step m n)
                                                (natrec2 {P} baseL baseR step (S m) n)
                                                (natrec2 {P} baseL baseR step m (S n))


natrec2simpl : {P :     Set}  ((n : )  P O n)  ((m : )  P m O)  ({m n : }  P m n  P (S m) (S n))  (m n : )  P m n
natrec2simpl baseL baseR step O n = baseL n
natrec2simpl baseL baseR step m O = baseR m
natrec2simpl {P} baseL baseR step (S m) (S n) = step (natrec2simpl {P} baseL baseR step m n)


-- Course of Values (or Complete) Recursion {May also be called transfinite induction} ------------------------

CRec : (  Set)    Set
CRec P O     = True
CRec P (S n) = P n × CRec P n

mutual

  comrec : {P :   Set}  ((m : )  CRec P m  P m)  Π  P
  comrec step n = step n (covrec step n)
  
  covrec : {P :   Set}  ((m : )  CRec P m  P m)  Π  (CRec P)
  covrec step O     = _
  covrec step (S n) = comrec step n , covrec step n


-- Complete Recursion on Lists

CReclist : {A : Set}  (List A  Set)  List A  Set
CReclist P []       = True
CReclist P (_  as) = P as × CReclist P as

mutual

  comreclist : {A : Set}  {P : List A  Set}  ((bs : List A)  CReclist P bs  P bs)  Π (List A) P
  comreclist step as = step as (covreclist step as)

  covreclist : {A : Set}  {P : List A  Set}  ((bs : List A)  CReclist P bs  P bs)  Π (List A) (CReclist P)
  covreclist step []       = _
  covreclist step (_  as) = comreclist step as , covreclist step as


-- Well Founded Recursion --------------------------------------------

data W (A : Set) (B : A  Set) : Set where
  sup : (a : A)  (B a  W A B)  W A B

wrec : {A : Set}  {B : A  Set}  (P : W A B  Set)  ((a : A)  (f : B a  W A B)  ((b : B a)  P (f b))  P (sup a f))  Π (W A B) P
wrec P step (sup a f) = step a f  b  wrec P step (f b))

initialW : {A : Set}  {B : A  Set}  Σ A (Not  B)  W A B
initialW (a , nb) = sup a (absurd  nb) 

terminatingW : {A : Set}  {B : A  Set}  W A B  Not (Π A B)
terminatingW (sup a fw) fb = terminatingW (fw (fb a)) fb


-- Data-type of Accessible Elements

data Acc (A : Set) (_≺_ : A  A  Set) (a : A) : Set where
  acc : ((y : A)  y  a  Acc A _≺_ y)  Acc A _≺_ a

mutual

  wfrec : {A : Set}  {_≺_ : A  A  Set}  {P : A  Set}  (a : A)  ((y : A)  Acc A _≺_ y  ((z : A)  z  y  P z)  P y)  Acc A _≺_ a  P a
  wfrec a step Aa = step a Aa (wfrec' step Aa)
  
  wfrec' : {A : Set}  {_≺_ : A  A  Set}  {P : A  Set}  {a : A}  ((y : A)  Acc A _≺_ y  ((z : A)  z  y  P z)  P y)  Acc A _≺_ a  (z : A)  z  a  P z
  wfrec' step (acc f) z za = wfrec z step (f z za)


acc-init : {A : Set}  {_≺_ : A  A  Set}  {a : A}  ((y : A)  Not (y  a))  Acc A _≺_ a
acc-init f = acc  y  absurd  f y)


{-

-- Making more arguments implicit makes for a simpler definition
-- It matches up closer with W types now as well

data Acc' (A : Set) (_≺_ : A → A → Set) (a : A) : Set where
  acc : ({y : A} → y ≺ a → Acc' A _≺_ y) → Acc' A _≺_ a

rec : {A : Set} → {_≺_ : A → A → Set} → {P : A → Set} → {a : A} → ({y : A} → Acc' A _≺_ y → ({z : A} → z ≺ y → P z) → P y) → Acc' A _≺_ a → P a
rec step (acc f) = step (acc f) (\lt → rec step (f lt))

-}