{- LOOKMANO --no-positivity-check -} module Ornament where record One : Set where {- record Sig (S : Set)(T : S -> Set) : Set where field fst : S snd : T fst open module Sig' {S : Set}{T : S -> Set} = Sig {S}{T} _,_ : {S : Set}{T : S -> Set}(s : S) -> T s -> Sig S T s , t = record {fst = s; snd = t} -} data Sig (S : Set)(T : S -> Set) : Set where _,_ : (s : S) -> T s -> Sig S T fst : forall {S T} -> Sig S T -> S fst (s , t) = s snd : forall {S T}(x : Sig S T) -> T (fst x) snd (s , t) = t infixr 40 _,_ _/_ : {I J : Set} -> (J -> Set) -> (I -> J) -> I -> Set _/_ F f i = F (f i) _-:>_ : {I : Set} -> (I -> Set) -> (I -> Set) -> Set X -:> Y = {i : _} -> X i -> Y i Alg : {I : Set} -> ((I -> Set) -> I -> Set) -> (I -> Set) -> Set Alg F X = F X -:> X infix 40 _-:>_ infixl 50 _/_ _*_ : Set -> Set -> Set S * T = Sig S \ _ -> T data _==_ {X : Set}(x : X) : X -> Set where refl : x == x data Desc (I : Set) : Set1 where out : (o : I) -> Desc I arg : (A : Set)(D : A -> Desc I) -> Desc I _rec_ : (h : I)(D : Desc I) -> Desc I [!_!] : {I : Set} -> Desc I -> (I -> Set) -> I -> Set [! out o !] X i = o == i [! arg A D !] X i = Sig A \ a -> [! D a !] X i [! h rec D !] X i = X h * [! D !] X i data Data {I : Set}(D : Desc I)(i : I) : Set where <_> : [! D !] (Data D) i -> Data D i map : {I : Set}(D : Desc I){X Y : I -> Set} -> X -:> Y -> [! D !] X -:> [! D !] Y map (out o) f q = q map (arg A D) f (a , d) = a , map (D a) f d map (h rec D) f (x , d) = f x , map D f d fold : {I : Set}{D : Desc I}{X : I -> Set} -> Alg [! D !] X -> Data D -:> X fold {D = D} phi < d > = phi (map D (fold phi) d) data Two : Set where tt : Two ff : Two Case : {P : Two -> Set1} -> P tt -> P ff -> (b : Two) -> P b Case t f tt = t Case t f ff = f NAT : Desc One NAT = arg Two (Case (out _) (_ rec out _)) Nat : Set Nat = Data NAT _ zero : Nat zero = < tt , refl > suc : Nat -> Nat suc n = < ff , n , refl > _+_ : Nat -> Nat -> Nat _+_ x y = fold palg x where palg : Alg [! NAT !] (\ _ -> Nat) palg (tt , refl) = y palg (ff , x+y , refl) = suc x+y data _Inv_ {I J : Set}(f : J -> I) : I -> Set where inv : (j : J) -> f Inv (f j) data Orn {I : Set}(J : Set)(f : J -> I) : Desc I -> Set1 where out : {o : I}(jq : f Inv o) -> Orn J f (out o) arg : (A : Set){D : A -> Desc I} (O : (a : A) -> Orn J f (D a)) -> Orn J f (arg A D) _rec_ : {h : I}{D : Desc I} -> (jq : f Inv h)(O : Orn J f D) -> Orn J f (h rec D) new : {D : Desc I}(A : Set)(O : A -> Orn J f D) -> Orn J f D infixr 40 _rec_ oD : {I J : Set}{f : J -> I}{D : Desc I} -> Orn J f D -> Desc J oD (out (inv j)) = out j oD (arg A O) = arg A \ a -> oD (O a) oD (inv j rec O) = j rec (oD O) oD (new A O) = arg A \ a -> oD (O a) oAHelp : forall {I J f}{D : Desc I}{R : I -> Set} -> (O : Orn J f D) -> [! oD O !] (R / f) -:> [! D !] R / f oAHelp (out (inv j)) refl = refl oAHelp (arg A O) (a , o) = a , oAHelp (O a) o oAHelp (inv j' rec O) (x , o) = x , oAHelp O o oAHelp (new A O) (a , o) = oAHelp (O a) o ornAlg : {I J : Set}{f : J -> I}{D : Desc I}(O : Orn J f D) -> Alg [! oD O !] (Data D / f) ornAlg {I} {J} {f} {D} O d = < oAHelp O d > NAT-LIST : Set -> Orn One _ NAT NAT-LIST X = arg Two (Case (out (inv _) ) (new X \ _ -> inv _ rec out (inv _))) LIST : Set -> Desc One LIST X = oD (NAT-LIST X) List : Set -> Set List X = Data (LIST X) _ [l] : {X : Set} -> List X [l] = < tt , refl > _:l:_ : {X : Set} -> X -> List X -> List X x :l: xs = < ff , x , xs , refl > algOrn : {I : Set}{J : I -> Set}(D : Desc I) -> Alg [! D !] J -> Orn (Sig I J) fst D algOrn (out o) phi = out (inv (o , phi refl)) algOrn (arg A D) phi = arg A \ a -> algOrn (D a) \ d -> phi (a , d) algOrn {J = J} (h rec D) phi = new (J h) \ j -> inv (h , j) rec algOrn D \ d -> phi (j , d) LIST-VEC : (X : Set) -> Orn (One * Nat) _ (LIST X) LIST-VEC X = algOrn (LIST X) (ornAlg (NAT-LIST X)) VEC : Set -> Desc (One * Nat) VEC X = oD (LIST-VEC X) Vec : Nat -> Set -> Set Vec n X = Data (VEC X) (_ , n) [] : {X : Set} -> Vec zero X [] = < tt , refl > _::_ : {n : Nat}{X : Set} -> X -> Vec n X -> Vec (suc n) X x :: xs = < ff , x , _ , xs , refl > All : {I : Set}(D : Desc I){R : I -> Set}(P : {i : I} -> R i -> Set) {i : I} -> [! D !] R i -> Set All (out o) P x = One All (arg A D) P (a , d) = All (D a) P d All (h rec 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 : [! D !] R i) -> All D P d everywhere (out o) P p d = _ everywhere (arg A D) P p (a , d) = everywhere (D a) P p d everywhere (h rec 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 : [! 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) AOOAHelp : {I : Set}{J R : I -> Set}{Y : Sig I J -> Set} (g : R -:> J) (f : Y -:> R / fst) (D : Desc I)(phi : Alg [! D !] J) -> let Dphi = algOrn D phi in {ij : Sig I J}(d : [! oD Dphi !] Y ij) -> All (oD Dphi) (\ {ij} y -> g (f y) == snd ij) d -> phi (map D g (oAHelp Dphi (map (oD Dphi) f d))) == snd ij AOOAHelp g f (out o) phi refl H = refl AOOAHelp g f (arg A D) phi (a , d) H = AOOAHelp g f (D a) (\ d -> phi (a , d)) d H AOOAHelp g f (h rec D) phi (j , y , d) (q , H) with g (f y) AOOAHelp g f (h rec D) phi (j , y , d) (refl , H) | .j = AOOAHelp g f D (\ d -> phi (j , d)) d H AOOAThm : {I : Set}(D : Desc I){J : I -> Set}(phi : Alg [! D !] J) -> let Dphi = algOrn D phi in {ij : Sig I J}(x : Data (oD Dphi) ij) -> fold phi (fold (ornAlg Dphi) x) == snd ij AOOAThm {I} D {J} phi = let Dphi = algOrn D phi in induction (oD Dphi) (\ {ij} x -> fold phi (fold (ornAlg Dphi) x) == snd ij) (AOOAHelp {R = Data D} (fold phi) (fold (ornAlg (algOrn D phi))) D phi) data HOp : Set where PUSH : HOp SEQ : HOp ADD : HOp HCode : Desc (Nat * Nat) HCode = arg HOp args where args : HOp -> Desc (Nat * Nat) args PUSH = arg Nat \ _ -> arg Nat \ i -> out (i , suc i) args SEQ = arg Nat \ k -> arg Nat \ l -> arg Nat \ m -> (k , l) rec (l , m) rec out (k , m) args ADD = arg Nat \ i -> out (suc (suc i) , suc i) HSem : Nat * Nat -> Set HSem ij = Vec (fst ij) Nat -> Vec (snd ij) Nat HAlg : Alg [! HCode !] HSem HAlg (PUSH , n , i , refl) ns = n :: ns HAlg (SEQ , k , l , m , f , g , refl) ns = g (f ns) HAlg (ADD , i , refl) < ff , x , .(suc i) , < ff , y , .i , stk , refl > , refl > = (y + x) :: stk HAlg (ADD , i , refl) < ff , _ , ._ , < tt , () > , refl > HAlg (ADD , i , refl) < tt , () > HCodeSem : Desc (Sig (Nat * Nat) HSem) HCodeSem = oD (algOrn HCode HAlg) HExp : Desc One HExp = arg Two (Case (arg Nat \ _ -> out _) (_ rec _ rec out _ )) hEval : Data HExp _ -> Nat hEval = fold evAlg where evAlg : Alg [! HExp !] (\ _ -> Nat) evAlg ( tt , n , refl ) = n evAlg ( ff , a , b , refl ) = a + b hCompileSem : (e : Data HExp _) -> {i : Nat} -> Data HCodeSem ((i , suc i) , _::_ (hEval e)) hCompileSem = induction HExp (\e -> {i : Nat} -> Data HCodeSem ((i , suc i) , _::_ (hEval e))) help where help : (d : [! HExp !] (Data HExp) _) -> All HExp (\ e -> {i : Nat} -> Data HCodeSem ((i , suc i) , _::_ (hEval e))) d -> {i : Nat} -> Data HCodeSem ((i , suc i) , _::_ (hEval < d >)) help ( tt , n , refl ) H = < PUSH , n , _ , refl > help ( ff , a , b , refl ) ( ca , cb , _ ) = < SEQ , _ , _ , _ , _ , ca , _ , < SEQ , _ , _ , _ , _ , cb , _ , < ADD , _ , refl > , refl > , refl > hCompile : Data HExp _ -> {i : Nat} -> Data HCode (i , suc i) hCompile e = fold (ornAlg (algOrn HCode HAlg)) (hCompileSem e) hTheorem : (e : Data HExp _){i : Nat} -> fold HAlg (hCompile e {i}) == _::_ (hEval e) hTheorem e = AOOAThm HCode HAlg (hCompileSem e)