From 756631e76b62183a36add3f5e28f6c1ee95bc1b5 Mon Sep 17 00:00:00 2001 From: Harrison Grodin Date: Wed, 4 Oct 2023 04:04:54 -0400 Subject: [PATCH] Update sequential sorting --- src/Examples/Sorting/Comparable.agda | 30 +++-------- src/Examples/Sorting/Core.agda | 14 +++--- src/Examples/Sorting/Sequential.agda | 6 ++- .../Sorting/Sequential/Comparable.agda | 6 ++- src/Examples/Sorting/Sequential/Core.agda | 4 +- .../Sorting/Sequential/InsertionSort.agda | 50 ++++++++++--------- .../Sorting/Sequential/MergeSort.agda | 25 +++++----- .../Sorting/Sequential/MergeSort/Merge.agda | 39 ++++++++------- .../Sorting/Sequential/MergeSort/Split.agda | 21 ++++---- 9 files changed, 97 insertions(+), 98 deletions(-) diff --git a/src/Examples/Sorting/Comparable.agda b/src/Examples/Sorting/Comparable.agda index 92031ed4..92605e6d 100644 --- a/src/Examples/Sorting/Comparable.agda +++ b/src/Examples/Sorting/Comparable.agda @@ -1,4 +1,6 @@ -open import Calf.CostMonoid +{-# OPTIONS --rewriting #-} + +open import Algebra.Cost open import Data.Nat using (ℕ) module Examples.Sorting.Comparable @@ -6,9 +8,9 @@ module Examples.Sorting.Comparable open CostMonoid costMonoid using (ℂ) -open import Calf costMonoid -open import Calf.Types.Bool -open import Calf.Types.Bounded costMonoid +open import Calf costMonoid hiding (A) +open import Calf.Data.Bool using (bool) +open import Calf.Data.IsBounded costMonoid open import Relation.Nullary open import Relation.Nullary.Negation @@ -57,24 +59,8 @@ NatComparable = record ; ≤-antisym = ≤-antisym ; _≤?_ = λ x y → step (F (meta⁺ (Dec (x ≤ y)))) (fromℕ 1) (ret (x ≤? y)) ; ≤?-total = λ x y u → (x ≤? y) , (step/ext (F _) (ret _) (fromℕ 1) u) - ; h-cost = λ _ _ → ≲-refl + ; h-cost = λ _ _ → ≤⁻-refl } where - open import Calf.Types.Nat - - open import Data.Nat + open import Calf.Data.Nat open import Data.Nat.Properties - - ret-injective : ∀ {𝕊 v₁ v₂} → ret {U (meta 𝕊)} v₁ ≡ ret {U (meta 𝕊)} v₂ → v₁ ≡ v₂ - ret-injective {𝕊} = Eq.cong (λ e → bind {U (meta 𝕊)} (meta 𝕊) e id) - - reflects : ∀ {x y b} → ◯ (step (F bool) (fromℕ 1) (ret (x ≤ᵇ y)) ≡ ret {bool} b → Reflects (x ≤ y) b) - reflects {x} {y} {b} u h with ret-injective (Eq.subst (_≡ ret b) (step/ext (F bool) (ret (x ≤ᵇ y)) (fromℕ 1) u) h) - ... | refl = ≤ᵇ-reflects-≤ x y - - reflects⁻¹ : ∀ {x y b} → ◯ (Reflects (x ≤ y) b → step (F (U (meta Bool))) (fromℕ 1) (ret (x ≤ᵇ y)) ≡ ret b) - reflects⁻¹ {x} {y} u h with x ≤ᵇ y | invert (≤ᵇ-reflects-≤ x y) - reflects⁻¹ {x} {y} u (ofʸ x≤y) | false | ¬x≤y = contradiction x≤y ¬x≤y - reflects⁻¹ {x} {y} u (ofⁿ ¬x≤y) | false | _ = step/ext (F bool) (ret false) (fromℕ 1) u - reflects⁻¹ {x} {y} u (ofʸ x≤y) | true | _ = step/ext (F bool) (ret true) (fromℕ 1) u - reflects⁻¹ {x} {y} u (ofⁿ ¬x≤y) | true | x≤y = contradiction x≤y ¬x≤y diff --git a/src/Examples/Sorting/Core.agda b/src/Examples/Sorting/Core.agda index e7de3069..5684897f 100644 --- a/src/Examples/Sorting/Core.agda +++ b/src/Examples/Sorting/Core.agda @@ -1,4 +1,6 @@ -open import Calf.CostMonoid +{-# OPTIONS --rewriting #-} + +open import Algebra.Cost open import Data.Nat using (ℕ) open import Examples.Sorting.Comparable @@ -9,9 +11,9 @@ module Examples.Sorting.Core open Comparable M -open import Calf costMonoid -open import Calf.Types.Product -open import Calf.Types.List +open import Calf costMonoid hiding (A) +open import Calf.Data.Product using (_×⁺_; _,_; proj₁; proj₂) +open import Calf.Data.List using (list; []; _∷_; _∷ʳ_; [_]; length; _++_; reverse) open import Relation.Nullary open import Relation.Nullary.Negation @@ -86,10 +88,10 @@ uncons₂ : ∀ {x xs} → Sorted (x ∷ xs) → Sorted xs uncons₂ (h ∷ sorted) = sorted sorted-of : val (list A) → val (list A) → tp pos -sorted-of l l' = prod⁺ (meta⁺ (l ↭ l')) (sorted l') +sorted-of l l' = meta⁺ (l ↭ l') ×⁺ (sorted l') sort-result : val (list A) → tp pos -sort-result l = Σ++ (list A) (sorted-of l) +sort-result l = Σ⁺ (list A) (sorted-of l) sorting : tp neg sorting = Π (list A) λ l → F (sort-result l) diff --git a/src/Examples/Sorting/Sequential.agda b/src/Examples/Sorting/Sequential.agda index b6713cd0..c3f70a3d 100644 --- a/src/Examples/Sorting/Sequential.agda +++ b/src/Examples/Sorting/Sequential.agda @@ -1,10 +1,12 @@ +{-# OPTIONS --rewriting #-} + module Examples.Sorting.Sequential where open import Examples.Sorting.Sequential.Comparable open import Calf costMonoid -open import Calf.Types.Nat -open import Calf.Types.List +open import Calf.Data.Nat +open import Calf.Data.List open import Relation.Binary.PropositionalEquality as Eq using (_≡_) open import Data.Product using (_,_) diff --git a/src/Examples/Sorting/Sequential/Comparable.agda b/src/Examples/Sorting/Sequential/Comparable.agda index 50e1d31d..0b2844d0 100644 --- a/src/Examples/Sorting/Sequential/Comparable.agda +++ b/src/Examples/Sorting/Sequential/Comparable.agda @@ -1,7 +1,9 @@ +{-# OPTIONS --rewriting #-} + module Examples.Sorting.Sequential.Comparable where -open import Calf.CostMonoid public -open import Calf.CostMonoids +open import Algebra.Cost public + costMonoid = ℕ-CostMonoid diff --git a/src/Examples/Sorting/Sequential/Core.agda b/src/Examples/Sorting/Sequential/Core.agda index 631471cb..1888c13d 100644 --- a/src/Examples/Sorting/Sequential/Core.agda +++ b/src/Examples/Sorting/Sequential/Core.agda @@ -1,8 +1,10 @@ +{-# OPTIONS --rewriting #-} + open import Examples.Sorting.Sequential.Comparable module Examples.Sorting.Sequential.Core (M : Comparable) where -open import Calf.CostMonoid +open import Algebra.Cost open CostMonoid costMonoid hiding (zero; _+_; _≤_; ≤-refl; ≤-trans) public diff --git a/src/Examples/Sorting/Sequential/InsertionSort.agda b/src/Examples/Sorting/Sequential/InsertionSort.agda index 42698679..08a8d57c 100644 --- a/src/Examples/Sorting/Sequential/InsertionSort.agda +++ b/src/Examples/Sorting/Sequential/InsertionSort.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + open import Examples.Sorting.Sequential.Comparable module Examples.Sorting.Sequential.InsertionSort (M : Comparable) where @@ -5,13 +7,13 @@ module Examples.Sorting.Sequential.InsertionSort (M : Comparable) where open Comparable M open import Examples.Sorting.Sequential.Core M -open import Calf costMonoid -open import Calf.Types.Bool -open import Calf.Types.List -open import Calf.Types.Eq -open import Calf.Types.BoundedG costMonoid -open import Calf.Types.Bounded costMonoid -open import Calf.Types.BigO costMonoid +open import Calf costMonoid hiding (A) +open import Calf.Data.Bool using (bool) +open import Calf.Data.List +open import Calf.Data.Equality using (_≡_; refl) +open import Calf.Data.IsBoundedG costMonoid +open import Calf.Data.IsBounded costMonoid +open import Calf.Data.BigO costMonoid open import Relation.Nullary open import Relation.Nullary.Negation @@ -24,7 +26,7 @@ import Data.Nat.Properties as N open import Data.Nat.Square -insert : cmp (Π A λ x → Π (list A) λ l → Π (sorted l) λ _ → F (Σ++ (list A) λ l' → sorted-of (x ∷ l) l')) +insert : cmp (Π A λ x → Π (list A) λ l → Π (sorted l) λ _ → F (Σ⁺ (list A) λ l' → sorted-of (x ∷ l) l')) insert x [] [] = ret ([ x ] , refl , [] ∷ []) insert x (y ∷ ys) (h ∷ hs) = bind (F _) (x ≤? y) $ case-≤ @@ -54,16 +56,16 @@ insert/total x (y ∷ ys) (h ∷ hs) u with ≤?-total x y u insert/cost : cmp (Π A λ _ → Π (list A) λ _ → cost) insert/cost x l = step⋆ (length l) -insert/is-bounded : ∀ x l h → IsBoundedG (Σ++ (list A) λ l' → sorted-of (x ∷ l) l') (insert x l h) (insert/cost x l) -insert/is-bounded x [] [] = ≲-refl +insert/is-bounded : ∀ x l h → IsBoundedG (Σ⁺ (list A) λ l' → sorted-of (x ∷ l) l') (insert x l h) (insert/cost x l) +insert/is-bounded x [] [] = ≤⁻-refl insert/is-bounded x (y ∷ ys) (h ∷ hs) = - bound/bind/const {_} {Σ++ (list A) λ l' → sorted-of (x ∷ (y ∷ ys)) l'} + bound/bind/const {_} {Σ⁺ (list A) λ l' → sorted-of (x ∷ (y ∷ ys)) l'} {x ≤? y} {case-≤ _ _} 1 (length ys) (h-cost x y) - λ { (yes x≤y) → step-monoˡ-≲ (ret _) (z≤n {length ys}) + λ { (yes x≤y) → step-monoˡ-≤⁻ (ret _) (z≤n {length ys}) ; (no ¬x≤y) → insert/is-bounded x ys hs } @@ -71,8 +73,8 @@ insert/is-bounded x (y ∷ ys) (h ∷ hs) = sort : cmp sorting sort [] = ret ([] , refl , []) sort (x ∷ xs) = - bind (F (Σ++ (list A) (sorted-of (x ∷ xs)))) (sort xs) λ (xs' , xs↭xs' , sorted-xs') → - bind (F (Σ++ (list A) (sorted-of (x ∷ xs)))) (insert x xs' sorted-xs') λ (x∷xs' , x∷xs↭x∷xs' , sorted-x∷xs') → + bind (F (Σ⁺ (list A) (sorted-of (x ∷ xs)))) (sort xs) λ (xs' , xs↭xs' , sorted-xs') → + bind (F (Σ⁺ (list A) (sorted-of (x ∷ xs)))) (insert x xs' sorted-xs') λ (x∷xs' , x∷xs↭x∷xs' , sorted-x∷xs') → ret (x∷xs' , trans (prep x xs↭xs') x∷xs↭x∷xs' , sorted-x∷xs') sort/total : IsTotal sort @@ -86,18 +88,18 @@ sort/total (x ∷ xs) u = ↓ ≡⟨ Eq.cong (λ e → - bind (F (Σ++ (list A) (sorted-of (x ∷ xs)))) e λ (xs' , xs↭xs' , sorted-xs') → - bind (F (Σ++ (list A) (sorted-of (x ∷ xs)))) (insert x xs' sorted-xs') λ (x∷xs' , x∷xs↭x∷xs' , sorted-x∷xs') → + bind (F (Σ⁺ (list A) (sorted-of (x ∷ xs)))) e λ (xs' , xs↭xs' , sorted-xs') → + bind (F (Σ⁺ (list A) (sorted-of (x ∷ xs)))) (insert x xs' sorted-xs') λ (x∷xs' , x∷xs↭x∷xs' , sorted-x∷xs') → ret (x∷xs' , trans (prep x xs↭xs') x∷xs↭x∷xs' , sorted-x∷xs')) (Valuable.proof (sort/total xs u)) ⟩ - ( bind (F (Σ++ (list A) (sorted-of (x ∷ xs)))) (insert x xs' sorted-xs') λ (x∷xs' , x∷xs↭x∷xs' , sorted-x∷xs') → + ( bind (F (Σ⁺ (list A) (sorted-of (x ∷ xs)))) (insert x xs' sorted-xs') λ (x∷xs' , x∷xs↭x∷xs' , sorted-x∷xs') → ret (x∷xs' , _ , sorted-x∷xs') ) ≡⟨ Eq.cong (λ e → - bind (F (Σ++ (list A) (sorted-of (x ∷ xs)))) e λ (x∷xs' , x∷xs↭x∷xs' , sorted-x∷xs') → + bind (F (Σ⁺ (list A) (sorted-of (x ∷ xs)))) e λ (x∷xs' , x∷xs↭x∷xs' , sorted-x∷xs') → ret (x∷xs' , trans (prep x xs↭xs') x∷xs↭x∷xs' , sorted-x∷xs')) (Valuable.proof (insert/total x xs' sorted-xs' u)) ⟩ @@ -107,16 +109,16 @@ sort/total (x ∷ xs) u = ↓ sort/cost : cmp (Π (list A) λ _ → cost) sort/cost l = step⋆ (length l ²) -sort/is-bounded : ∀ l → IsBoundedG (Σ++ (list A) (sorted-of l)) (sort l) (sort/cost l) -sort/is-bounded [] = ≲-refl +sort/is-bounded : ∀ l → IsBoundedG (Σ⁺ (list A) (sorted-of l)) (sort l) (sort/cost l) +sort/is-bounded [] = ≤⁻-refl sort/is-bounded (x ∷ xs) = - let open ≲-Reasoning cost in + let open ≤⁻-Reasoning cost in begin ( bind cost (sort xs) λ (xs' , xs↭xs' , sorted-xs') → bind cost (insert x xs' sorted-xs') λ _ → step⋆ zero ) - ≤⟨ bind-monoʳ-≲ (sort xs) (λ (xs' , xs↭xs' , sorted-xs') → insert/is-bounded x xs' sorted-xs') ⟩ + ≤⟨ bind-monoʳ-≤⁻ (sort xs) (λ (xs' , xs↭xs' , sorted-xs') → insert/is-bounded x xs' sorted-xs') ⟩ ( bind cost (sort xs) λ (xs' , xs↭xs' , sorted-xs') → step⋆ (length xs') ) @@ -128,9 +130,9 @@ sort/is-bounded (x ∷ xs) = ( bind cost (sort xs) λ _ → step⋆ (length xs) ) - ≤⟨ bind-monoˡ-≲ (λ _ → step⋆ (length xs)) (sort/is-bounded xs) ⟩ + ≤⟨ bind-monoˡ-≤⁻ (λ _ → step⋆ (length xs)) (sort/is-bounded xs) ⟩ step⋆ ((length xs ²) + length xs) - ≤⟨ step⋆-mono-≲ (N.+-mono-≤ (N.*-monoʳ-≤ (length xs) (N.n≤1+n (length xs))) (N.n≤1+n (length xs))) ⟩ + ≤⟨ step⋆-mono-≤⁻ (N.+-mono-≤ (N.*-monoʳ-≤ (length xs) (N.n≤1+n (length xs))) (N.n≤1+n (length xs))) ⟩ step⋆ (length xs * length (x ∷ xs) + length (x ∷ xs)) ≡⟨ Eq.cong step⋆ (N.+-comm (length xs * length (x ∷ xs)) (length (x ∷ xs))) ⟩ step⋆ (length (x ∷ xs) ²) diff --git a/src/Examples/Sorting/Sequential/MergeSort.agda b/src/Examples/Sorting/Sequential/MergeSort.agda index 68cc99a3..01f58d0c 100644 --- a/src/Examples/Sorting/Sequential/MergeSort.agda +++ b/src/Examples/Sorting/Sequential/MergeSort.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + open import Examples.Sorting.Sequential.Comparable module Examples.Sorting.Sequential.MergeSort (M : Comparable) where @@ -5,16 +7,15 @@ module Examples.Sorting.Sequential.MergeSort (M : Comparable) where open Comparable M open import Examples.Sorting.Sequential.Core M -open import Calf costMonoid -open import Calf.Types.Unit -open import Calf.Types.Product -open import Calf.Types.Bool -open import Calf.Types.Nat -open import Calf.Types.List -open import Calf.Types.Eq -open import Calf.Types.BoundedG costMonoid -open import Calf.Types.Bounded costMonoid -open import Calf.Types.BigO costMonoid +open import Calf costMonoid hiding (A) +open import Calf.Data.Product +open import Calf.Data.Bool +open import Calf.Data.Nat +open import Calf.Data.List using (list; []; _∷_; _∷ʳ_; [_]; length; _++_; reverse) +open import Calf.Data.Equality using (_≡_; refl) +open import Calf.Data.IsBoundedG costMonoid +open import Calf.Data.IsBounded costMonoid +open import Calf.Data.BigO costMonoid open import Relation.Nullary open import Relation.Nullary.Negation @@ -134,7 +135,7 @@ sort/clocked/cost : cmp $ Π nat λ k → Π (list A) λ l → Π (meta⁺ (⌈l sort/clocked/cost k l _ = step⋆ (k * length l) sort/clocked/is-bounded : ∀ k l h → IsBoundedG (sort-result l) (sort/clocked k l h) (sort/clocked/cost k l h) -sort/clocked/is-bounded zero l h = ≲-refl +sort/clocked/is-bounded zero l h = ≤⁻-refl sort/clocked/is-bounded (suc k) l h = bound/bind/const {e = split l} @@ -211,7 +212,7 @@ sort/clocked/is-bounded (suc k) l h = 0 (merge/is-bounded (l₁' , l₂') _) λ _ → - ≲-refl + ≤⁻-refl sort : cmp (Π (list A) λ l → F (sort-result l)) diff --git a/src/Examples/Sorting/Sequential/MergeSort/Merge.agda b/src/Examples/Sorting/Sequential/MergeSort/Merge.agda index c458d5af..826639a5 100644 --- a/src/Examples/Sorting/Sequential/MergeSort/Merge.agda +++ b/src/Examples/Sorting/Sequential/MergeSort/Merge.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + open import Examples.Sorting.Sequential.Comparable module Examples.Sorting.Sequential.MergeSort.Merge (M : Comparable) where @@ -5,15 +7,14 @@ module Examples.Sorting.Sequential.MergeSort.Merge (M : Comparable) where open Comparable M open import Examples.Sorting.Sequential.Core M -open import Calf costMonoid -open import Calf.Types.Unit -open import Calf.Types.Product -open import Calf.Types.Bool -open import Calf.Types.Nat -open import Calf.Types.List -open import Calf.Types.Eq -open import Calf.Types.BoundedG costMonoid -open import Calf.Types.Bounded costMonoid +open import Calf costMonoid hiding (A) +open import Calf.Data.Product +open import Calf.Data.Bool using (bool) +open import Calf.Data.Nat using (nat) +open import Calf.Data.List using (list; []; _∷_; _∷ʳ_; [_]; length; _++_; reverse) +open import Calf.Data.Equality +open import Calf.Data.IsBoundedG costMonoid +open import Calf.Data.IsBounded costMonoid open import Relation.Nullary open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; module ≡-Reasoning) @@ -42,11 +43,11 @@ prep' {x} {xs} y {ys} {l} h = ∎ merge/type : val pair → tp pos -merge/type (l₁ , l₂) = Σ++ (list A) λ l → sorted-of (l₁ ++ l₂) l +merge/type (l₁ , l₂) = Σ⁺ (list A) λ l → sorted-of (l₁ ++ l₂) l merge/clocked : cmp $ Π nat λ k → Π pair λ (l₁ , l₂) → - Π (prod⁺ (sorted l₁) (sorted l₂)) λ _ → + Π (sorted l₁ ×⁺ sorted l₂) λ _ → Π (meta⁺ (length l₁ + length l₂ ≡ k)) λ _ → F (merge/type (l₁ , l₂)) merge/clocked zero ([] , [] ) (sorted₁ , sorted₂ ) h = ret ([] , refl , []) @@ -84,15 +85,15 @@ merge/clocked/total (suc k) (x ∷ xs , y ∷ ys) (h₁ ∷ sorted₁ , h₂ ∷ merge/clocked/cost : cmp $ Π nat λ k → Π pair λ (l₁ , l₂) → - Π (prod⁺ (sorted l₁) (sorted l₂)) λ _ → + Π (sorted l₁ ×⁺ sorted l₂) λ _ → Π (meta⁺ (length l₁ + length l₂ ≡ k)) λ _ → F unit merge/clocked/cost k _ _ _ = step⋆ k merge/clocked/is-bounded : ∀ k p s h → IsBoundedG (merge/type p) (merge/clocked k p s h) (merge/clocked/cost k p s h) -merge/clocked/is-bounded zero ([] , [] ) (sorted₁ , sorted₂ ) h = ≲-refl -merge/clocked/is-bounded (suc k) ([] , l₂ ) ([] , sorted₂ ) h = step⋆-mono-≲ (z≤n {suc k}) -merge/clocked/is-bounded (suc k) (x ∷ xs , [] ) (sorted₁ , [] ) h = step⋆-mono-≲ (z≤n {suc k}) +merge/clocked/is-bounded zero ([] , [] ) (sorted₁ , sorted₂ ) h = ≤⁻-refl +merge/clocked/is-bounded (suc k) ([] , l₂ ) ([] , sorted₂ ) h = step⋆-mono-≤⁻ (z≤n {suc k}) +merge/clocked/is-bounded (suc k) (x ∷ xs , [] ) (sorted₁ , [] ) h = step⋆-mono-≤⁻ (z≤n {suc k}) merge/clocked/is-bounded (suc k) (x ∷ xs , y ∷ ys) (h₁ ∷ sorted₁ , h₂ ∷ sorted₂) h = bound/bind/const {e = x ≤? y} @@ -100,14 +101,14 @@ merge/clocked/is-bounded (suc k) (x ∷ xs , y ∷ ys) (h₁ ∷ sorted₁ , h 1 k (h-cost x y) - λ { (yes p) → bind-mono-≲ (merge/clocked/is-bounded k (xs , y ∷ ys) _ _) (λ _ → ≲-refl) - ; (no ¬p) → bind-mono-≲ (merge/clocked/is-bounded k (x ∷ xs , ys) _ _) (λ _ → ≲-refl) + λ { (yes p) → bind-monoˡ-≤⁻ (λ _ → step⋆ zero) (merge/clocked/is-bounded k (xs , y ∷ ys) _ _) + ; (no ¬p) → bind-monoˡ-≤⁻ (λ _ → step⋆ zero) (merge/clocked/is-bounded k (x ∷ xs , ys) _ _) } merge : cmp $ Π pair λ (l₁ , l₂) → - Π (prod⁺ (sorted l₁) (sorted l₂)) λ _ → + Π (sorted l₁ ×⁺ sorted l₂) λ _ → F (merge/type (l₁ , l₂)) merge (l₁ , l₂) s = merge/clocked (length l₁ + length l₂) (l₁ , l₂) s refl @@ -116,7 +117,7 @@ merge/total (l₁ , l₂) s = merge/clocked/total (length l₁ + length l₂) (l merge/cost : cmp $ Π pair λ (l₁ , l₂) → - Π (prod⁺ (sorted l₁) (sorted l₂)) λ _ → + Π (sorted l₁ ×⁺ sorted l₂) λ _ → cost merge/cost (l₁ , l₂) s = merge/clocked/cost (length l₁ + length l₂) (l₁ , l₂) s refl diff --git a/src/Examples/Sorting/Sequential/MergeSort/Split.agda b/src/Examples/Sorting/Sequential/MergeSort/Split.agda index 9aa5c166..8ac06113 100644 --- a/src/Examples/Sorting/Sequential/MergeSort/Split.agda +++ b/src/Examples/Sorting/Sequential/MergeSort/Split.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + open import Examples.Sorting.Sequential.Comparable module Examples.Sorting.Sequential.MergeSort.Split (M : Comparable) where @@ -5,12 +7,11 @@ module Examples.Sorting.Sequential.MergeSort.Split (M : Comparable) where open Comparable M open import Examples.Sorting.Sequential.Core M -open import Calf costMonoid -open import Calf.Types.Unit -open import Calf.Types.Product -open import Calf.Types.Nat -open import Calf.Types.List -open import Calf.Types.BoundedG costMonoid +open import Calf costMonoid hiding (A) +open import Calf.Data.Product +open import Calf.Data.Nat +open import Calf.Data.List +open import Calf.Data.IsBoundedG costMonoid open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; module ≡-Reasoning) open import Data.Product using (_×_; _,_; ∃; proj₁; proj₂) @@ -18,10 +19,10 @@ open import Data.Nat as Nat using (ℕ; zero; suc; _+_; _*_; ⌊_/2⌋; ⌈_/2 open import Data.Nat.Properties as N using (module ≤-Reasoning) -pair = prod⁺ (list A) (list A) +pair = list A ×⁺ list A split/type : val nat → val nat → val (list A) → tp pos -split/type k k' l = Σ++ pair λ (l₁ , l₂) → meta⁺ (length l₁ ≡ k × length l₂ ≡ k' × l ↭ (l₁ ++ l₂)) +split/type k k' l = Σ⁺ pair λ (l₁ , l₂) → meta⁺ (length l₁ ≡ k × length l₂ ≡ k' × l ↭ (l₁ ++ l₂)) split/clocked : cmp (Π nat λ k → Π nat λ k' → Π (list A) λ l → Π (meta⁺ (k + k' ≡ length l)) λ _ → F (split/type k k' l)) split/clocked zero k' l refl = ret (([] , l) , refl , refl , refl) @@ -38,8 +39,8 @@ split/clocked/cost : cmp (Π nat λ k → Π nat λ k' → Π (list A) λ l → split/clocked/cost _ _ _ _ = step⋆ zero split/clocked/is-bounded : ∀ k k' l h → IsBoundedG (split/type k k' l) (split/clocked k k' l h) (split/clocked/cost k k' l h) -split/clocked/is-bounded zero k' l refl = ≲-refl -split/clocked/is-bounded (suc k) k' (x ∷ xs) h = bind-monoˡ-≲ _ (split/clocked/is-bounded k k' xs (N.suc-injective h)) +split/clocked/is-bounded zero k' l refl = ≤⁻-refl +split/clocked/is-bounded (suc k) k' (x ∷ xs) h = bind-monoˡ-≤⁻ _ (split/clocked/is-bounded k k' xs (N.suc-injective h)) split : cmp (Π (list A) λ l → F (split/type ⌊ length l /2⌋ ⌈ length l /2⌉ l))