module Desc where open import Basics public data Desc (I : Set) : Set1 where say : I -> Desc I sg : (S : Set)(D : S -> Desc I) -> Desc I ask_*_ : I -> Desc I -> Desc I : forall {I} -> Desc I -> (I -> Set) -> (I -> Set) X i = i' == i X i = Sg S \ s -> X i X i = X i' * X i _-:>_ : {I : Set} -> (I -> Set) -> (I -> Set) -> Set X -:> Y = {i : _} -> X i -> Y i infix 40 _-:>_ data Data {I : Set}(D : Desc I)(i : I) : Set where <<_>> : (Data D) i -> Data D i map : forall {I X Y}(D : Desc I) -> (X -:> Y) -> X -:> Y map (say i) f q = q map (sg S D) f (s , xs) = s , map (D s) f xs map (ask i * D) f (x , xs) = f x , map D f xs {- fold : forall {I X}{D : Desc I} -> ( X -:> X) -> Data D -:> X fold {D = D} phi << ds >> = phi (map D (fold phi) ds) -} mutual fold : forall {I}{D : Desc I}{X : I -> Set} -> ( X -:> X) -> Data D -:> X fold {D = D} phi << ds >> = phi (mapFold D D phi ds) mapFold : forall {I X}(D' D : Desc I) -> ( X -:> X) -> (Data D') -:> X mapFold D' (say i) phi q = q mapFold D' (sg S D) phi (s , xs) = s , mapFold D' (D s) phi xs mapFold D' (ask i * D) phi (x , xs) = fold phi x , mapFold D' D phi xs mutual foldFact : forall {I X}(D : Desc I)(phi : X -:> X) -> {i : I}(ds : (Data D) i) -> fold {D = D} phi << ds >> == phi (map D (fold phi) ds) foldFact D phi ds = cong phi (mapFoldFact D D phi ds) mapFoldFact : forall {I X}(D' D : Desc I)(phi : X -:> X) -> {i : I}(ds : (Data D') i) -> mapFold D' D phi ds == map D (fold phi) ds mapFoldFact D' (say i) phi ds = refl mapFoldFact D' (sg S D) phi (s , ds) = cong (_,_ s) (mapFoldFact D' (D s) phi ds) mapFoldFact D' (ask i * D) phi (d , ds) = cong (_,_ (fold phi d)) (mapFoldFact D' D phi ds) All : {I : Set}(D : Desc I){R : I -> Set}(P : {i : I} -> R i -> Set) {i : I} -> R i -> Set All (say i) P x = One All (sg S D) P (s , d) = All (D s) P d All (ask i * D) P (x , d) = P x * All D P d {- everywhere : {I : Set}(D : Desc I){R : I -> Set} (P : {i : I} -> R i -> Set) -> ({i : I}(x : R i) -> P x) -> {i : I}(d : R i) -> All D P d everywhere (say i) P p d = _ everywhere (sg S D) P p (s , d) = everywhere (D s) P p d everywhere (ask i * D) P p (x , d) = p x , everywhere D P p d -} {- induction : {I : Set}(D : Desc I)(P : {i : I} -> Data D i -> Set) -> ({i : I}(d : (Data D) i) -> All D P d -> P << d >) -> {i : I}(x : Data D i) -> P x induction D P p << d >> = p d (everywhere D P (induction D P p) d) -} mutual induction : {I : Set}(D : Desc I)(P : {i : I} -> Data D i -> Set) -> ({i : I}(d : (Data D) i) -> All D P d -> P << d >>) -> {i : I}(x : Data D i) -> P x induction D P p << d >> = p d (everywhereInduction D D P p d) everywhereInduction : {I : Set}(D' D : Desc I) (P : {i : I} -> Data D' i -> Set) -> ({i : I}(d : (Data D') i) -> All D' P d -> P << d >>) -> {i : I}(d : (Data D') i) -> All D P d everywhereInduction D' (say i) P p d = _ everywhereInduction D' (sg S D) P p (s , d) = everywhereInduction D' (D s) P p d everywhereInduction D' (ask i * D) P p (x , d) = induction D' P p x , everywhereInduction D' D P p d