added FreshIdConor

src/extra/FreshIdConor.lagda

@@ -0,0 +1,78 @@
+---
+title     : "FreshIdConor: Generation of fresh names"
+layout    : page
+permalink : /FreshIdConor
+---
+
+\begin{code}
+module FreshIdConor where
+
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
+open Eq.≡-Reasoning
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.List
+  using (List; []; _∷_; _++_; map; foldr; replicate; length; _∷ʳ_)
+  renaming (reverse to rev)
+open import Data.List.Properties
+  using (++-assoc; ++-identityʳ)
+  renaming (unfold-reverse to revʳ;
+            reverse-++-commute to rev-++;
+            reverse-involutive to rev-inv)
+open import Data.List.All using (All; []; _∷_)
+open import Function using (_∘_)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Nullary.Negation using (¬?)
+open import Relation.Unary using (Decidable)
+
+pattern [_]       x        =  x ∷ []
+pattern [_,_]     x y      =  x ∷ y ∷ []
+pattern [_,_,_]   x y z    =  x ∷ y ∷ z ∷ []
+pattern [_,_,_,_] x y z w  =  x ∷ y ∷ z ∷ w ∷ []
+\end{code}
+
+## Conor's Break works left-to-right
+
+\begin{code}
+module Break {A : Set} where
+
+  data Break (P : A → Set) : List A → Set where
+    none : ∀ {xs} → All P xs → Break P xs
+    some : ∀ {xs y zs} → All P xs → ¬ P y → Break P (xs ++ [ y ] ++ zs)
+
+  break : ∀ {P : A → Set} (P? : Decidable P) → (xs : List A) → Break P xs
+  break P? []                                           =  none []
+  break P? (w ∷ ws) with P? w
+  ...                  | no ¬Pw                         =  some [] ¬Pw
+  ...                  | yes Pw with break P? ws
+  ...                              | none Pws           =  none (Pw ∷ Pws)
+  ...                              | some Pws ¬Py       =  some (Pw ∷ Pws) ¬Py
+\end{code}
+
+## But we want to break lists right-to-left
+
+\begin{code}
+module RevBreak {A : Set} where
+
+  open Break {A}
+
+  data RevBreak (P : A → Set) : List A → Set where
+    rnone : ∀ {xs} → All P (rev xs) → RevBreak P xs
+    rsome : ∀ {zs y xs} → ¬ P y → All P (rev xs) → RevBreak P (zs ++ [ y ] ++ xs)
+
+-- I'd like to do something along the following lines ...
+
+  revBreak : ∀ {P : A → Set} (P? : Decidable P) → (xs : List A) → RevBreak P xs
+  revBreak P? ws with break P? (rev ws)
+  ... | none {xs} Pxs = ?
+--    rewrite rev-inv ws
+--    = rnone {xs = rev xs} Pxs
+  ... | some {xs} {y} {zs} Pxs ¬Py = ?
+--    rewrite rev-inv ?xs | rev-inv ?zs   -- not clear how to bind ?xs and ?zs
+--    = rsome {zs = rev zs} {y = y} {xs = rev xs} ¬Py Pxs
+
+-- ... but even the pattern matching gets into trouble
+-- It complains that it cannot be sure that
+--   xs ++ [ y ] ++ zs = rev ws
+-- Doesn't this property follow immediately from the fact that break typechecks?
+\end{code}