Few week's progress

.gitignore

@@ -18,3 +18,4 @@ MAlonzo/
 
 # Ignore our generated main file
 src/Examples/Main-generated.agda
+src/Selective/Examples/Main-generated.agda

Makefile

@@ -23,6 +23,12 @@ selective-generated-main:
 	sed 's/__ENTRY__/$(ENTRY)/' src/Selective/Examples/Main-template.agda > src/Selective/Examples/Main-generated.agda
 	stack exec agda -- -c src/Selective/Examples/Main-generated.agda
 
+test-that-all-compliles:
+	$(MAKE) latex-clean
+	$(MAKE) latex
+	stack exec agda -- --no-main -c src/Selective/Examples/Main-generated.agda
+	stack exec agda -- --no-main -c src/Examples/Main-generated.agda
+
 clean:
 ifneq ($(strip $(agda-objects)),)
 	rm $(agda-objects)

latex.make

@@ -9,8 +9,6 @@ generated   :=  $(wildcard $(out-subdirs:%=%*.tex))
 
 $(moved): $(LATEX-OUTPUT-DIR)%.tex: src/%.lagda.tex
 	stack exec agda -- --latex-dir=$(LATEX-OUTPUT-DIR) --latex $<
-	perl postprocess-latex.pl $@ > $(LATEX-OUTPUT-DIR)$*.processed
-	mv $(LATEX-OUTPUT-DIR)$*.processed $@
 
 .PHONY: all clean
 all: $(moved)

src/Colist.agda

@@ -7,7 +7,7 @@ data Colist (i : Size) {a} (A : Set a) : Set a
 record ∞Colist (i : Size) {a} (A : Set a) : Set a where
   coinductive
   constructor delay_
-  field force : ∀ {j : Size< i} → Colist i A
+  field force : ∀ {j : Size< i} → Colist j A
 
 data Colist (i : Size) {a} (A : Set a) where
   [] : Colist i A

src/Examples/Call.lagda.tex

@@ -13,11 +13,12 @@
             using (_≡_ ; refl ; cong ; sym ; inspect ; [_] ; trans)
 open import Membership using (
             _∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] ; ⊆-refl
-            ; ⊆-trans ; ⊆-suc ; translate-⊆)
+            ; ⊆-trans ; ⊆-suc ; translate-⊆
+            ; ∈-inc ; ⊆++-refl)
 open import Data.Unit using (⊤ ; tt)
 open import Examples.SelectiveReceive using (
             selective-receive ; SelRec ; waiting-refs
-            ; add-references++ ; ∈-inc ; ⊆++-refl)
+            ; add-references++)
 open import Relation.Nullary using (yes ; no)
 
 open import Size
@@ -116,4 +117,4 @@
     return-result record { msg = (Msg Z (tag ∷ n ∷ [])) } = return n
     return-result record { msg = (Msg (S x) x₁) ; msg-ok = () }
 
-\end{code}
+\end{code}

src/Examples/Main-template.agda

@@ -14,4 +14,4 @@ infinitebindEntry = singleton-env (InfiniteBind.binder .force)
 selectiveReceiveEntry = singleton-env SelectiveReceive.spawner
 callEntry = singleton-env (Call.calltestActor .force)
 
-main = IO.run (run-env trace+actors-logger __ENTRY__)
+main = IO.run (run-env __ENTRY__)

src/Examples/Main.agda

@@ -14,4 +14,4 @@ infinitebindEntry = singleton-env (InfiniteBind.binder .force)
 selectiveReceiveEntry = singleton-env SelectiveReceive.spawner
 callEntry = singleton-env (Call.calltestActor .force)
 
-main = IO.run (run-env trace+actors-logger pingpongEntry)
+main = IO.run (run-env pingpongEntry)

src/Examples/SelectiveReceive.lagda.tex

@@ -15,7 +15,6 @@
 open import Relation.Binary.PropositionalEquality
             using (_≡_ ; refl ; cong ; sym ; inspect ; [_] ; trans)
 open import Membership
-            using (_∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] ; ⊆-refl ; ⊆-trans ; ⊆-suc)
 open import Data.Unit using (⊤ ; tt)
 
 
@@ -60,94 +59,6 @@
       ; is-ls = refl
       }) eq
 
-⊆++ : {a : Level} {A : Set a}
-      (xs ys zs : List A) →
-      xs ⊆ zs → ys ⊆ zs →
-      (xs ++ ys) ⊆ zs
-⊆++ _ ys zs [] q = q
-⊆++ _ ys zs (x₁ ∷ p) q = x₁ ∷ (⊆++ _ ys zs p q)
-
-∈-insert : ∀ {a} {A : Set a}
-           (xs ys : List A) →
-           (x : A) →
-           x ∈ (ys ++ x ∷ xs)
-∈-insert xs [] x = Z
-∈-insert xs (x₁ ∷ ys) x = S (∈-insert xs ys x)
-
--- count down both the proof and the list
--- Result depends on which is shortest
-insert-one : ∀ {a} {A : Set a} {x₁ : A}
-               (xs ys : List A) →
-               (y : A) →
-               x₁ ∈ (xs ++ ys) →
-               x₁ ∈ (xs ++ y ∷ ys)
-insert-one [] ys y p = S p
-insert-one (x ∷ xs) ys y Z = Z
-insert-one (x ∷ xs) ys y (S p) = S (insert-one xs ys y p)
-
-⊆-insert : ∀ {a} {A : Set a}
-                 (xs ys zs : List A) →
-                 (x : A) →
-                 xs ⊆ (ys ++ zs) →
-                 xs ⊆ (ys ++ x ∷ zs)
-⊆-insert [] ys zs x p = []
-⊆-insert (x₁ ∷ xs) ys zs x (x₂ ∷ p) = insert-one ys zs x x₂ ∷
-                                                 (⊆-insert xs ys zs x p)
-
-⊆-move : {a : Level} {A : Set a}
-                     (xs ys : List A) →
-                     (xs ++ ys) ⊆ (ys ++ xs)
-⊆-move [] ys rewrite (++-identityʳ ys) = ⊆-refl
-⊆-move (x ∷ xs) ys with (⊆-move xs ys)
-... | q = ∈-insert xs ys x ∷ ⊆-insert (xs ++ ys) ys xs x q
-
-⊆-skip : {a : Level} {A : Set a}
-         (xs ys zs : List A) →
-         ys ⊆ zs →
-         (xs ++ ys) ⊆ (xs ++ zs)
-⊆-skip [] ys zs p = p
-⊆-skip (x ∷ xs) ys zs p = Z ∷ (⊆-suc (⊆-skip xs ys zs p))
-
-⊆++-refl : ∀ {a} {A : Set a} →
-           (xs ys : List A) →
-           xs ⊆ (xs ++ ys)
-⊆++-refl [] ys = []
-⊆++-refl (x ∷ xs) ys = Z ∷ (⊆-suc (⊆++-refl xs ys))
-
-⊆++-l-refl : ∀ {a} {A : Set a} →
-                   (xs ys : List A) →
-                   xs ⊆ (ys ++ xs)
-⊆++-l-refl xs [] = ⊆-refl
-⊆++-l-refl xs (x ∷ ys) = ⊆-suc (⊆++-l-refl xs ys)
-
-∈-inc : ∀ {a} {A : Set a}
-              (xs ys : List A) →
-              (x : A) →
-              x ∈ xs →
-              x ∈ (xs ++ ys)
-∈-inc _ ys x Z = Z
-∈-inc _ ys x (S p) = S (∈-inc _ ys x p)
-
-⊆-inc : ∀ {a} {A : Set a}
-              (xs ys zs : List A) →
-              xs ⊆ ys →
-              (xs ++ zs) ⊆ (ys ++ zs)
-⊆-inc [] [] zs p = ⊆-refl
-⊆-inc [] (x ∷ ys) zs p = ⊆++-l-refl zs (x ∷ ys)
-⊆-inc (x ∷ xs) ys zs (px ∷ p) = ∈-inc ys zs x px ∷ (⊆-inc xs ys zs p)
-
-⊆++comm : ∀ {a} {A : Set a}
-            (xs ys zs : List A) →
-            ((xs ++ ys) ++ zs) ⊆ (xs ++ (ys ++ zs))
-⊆++comm [] ys zs = ⊆-refl
-⊆++comm (x ∷ xs) ys zs = Z ∷ (⊆-suc (⊆++comm xs ys zs))
-
-⊆++comm' : ∀ {a} {A : Set a}
-           (xs ys zs : List A) →
-           (xs ++ ys ++ zs) ⊆ ((xs ++ ys) ++ zs)
-⊆++comm' [] ys zs = ⊆-refl
-⊆++comm' (x ∷ xs) ys zs = Z ∷ ⊆-suc (⊆++comm' xs ys zs)
-
 add-references++ : ∀ {IS} → (xs ys : ReferenceTypes) →
                    (x : Message IS) →
                      add-references (xs ++ ys) x ≡
@@ -346,6 +257,6 @@
 spawner : ∀ {i} → ActorM i [] ⊤₁ [] (λ _ → [])
 spawner =
   spawn testActor ∞>>
-  ((Z ![t: Z ] ((lift false) ∷ [])) >>
+  ((Z ![t: Z ] ((lift true) ∷ [])) >>
   strengthen [])
 \end{code}

src/Membership.lagda.tex

@@ -5,8 +5,10 @@
 open import Data.List
 open import Data.List.Any using ()
 open import Data.List.All using (All ; [] ; _∷_)
+open import Data.List.Properties using (++-assoc ; ++-identityʳ)
 open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
 open import Data.Empty using (⊥)
+open import Level using (Level) renaming (zero to lzero ; suc to lsuc)
 \end{code}
 %<*ElementIn>
 \begin{code}
@@ -78,4 +80,116 @@
 ⊆-trans : ∀ {a} {A : Set a} {as bs cs : List A} → as ⊆ bs → bs ⊆ cs → as ⊆ cs
 ⊆-trans [] _ = []
 ⊆-trans (x₁ ∷ asbs) bscs = (translate-⊆ bscs x₁) ∷ (⊆-trans asbs bscs)
+
+
+⊆++ : {a : Level} {A : Set a}
+      (xs ys zs : List A) →
+      xs ⊆ zs → ys ⊆ zs →
+      (xs ++ ys) ⊆ zs
+⊆++ _ ys zs [] q = q
+⊆++ _ ys zs (x₁ ∷ p) q = x₁ ∷ (⊆++ _ ys zs p q)
+
+∈-insert : ∀ {a} {A : Set a}
+           (xs ys : List A) →
+           (x : A) →
+           x ∈ (ys ++ x ∷ xs)
+∈-insert xs [] x = Z
+∈-insert xs (x₁ ∷ ys) x = S (∈-insert xs ys x)
+
+-- count down both the proof and the list
+-- Result depends on which is shortest
+insert-one : ∀ {a} {A : Set a} {x₁ : A}
+               (xs ys : List A) →
+               (y : A) →
+               x₁ ∈ (xs ++ ys) →
+               x₁ ∈ (xs ++ y ∷ ys)
+insert-one [] ys y p = S p
+insert-one (x ∷ xs) ys y Z = Z
+insert-one (x ∷ xs) ys y (S p) = S (insert-one xs ys y p)
+
+⊆-insert : ∀ {a} {A : Set a}
+                 (xs ys zs : List A) →
+                 (x : A) →
+                 xs ⊆ (ys ++ zs) →
+                 xs ⊆ (ys ++ x ∷ zs)
+⊆-insert [] ys zs x p = []
+⊆-insert (x₁ ∷ xs) ys zs x (x₂ ∷ p) = insert-one ys zs x x₂ ∷
+                                                 (⊆-insert xs ys zs x p)
+
+⊆-move : {a : Level} {A : Set a}
+                     (xs ys : List A) →
+                     (xs ++ ys) ⊆ (ys ++ xs)
+⊆-move [] ys rewrite (++-identityʳ ys) = ⊆-refl
+⊆-move (x ∷ xs) ys with (⊆-move xs ys)
+... | q = ∈-insert xs ys x ∷ ⊆-insert (xs ++ ys) ys xs x q
+
+⊆-skip : {a : Level} {A : Set a}
+         (xs ys zs : List A) →
+         ys ⊆ zs →
+         (xs ++ ys) ⊆ (xs ++ zs)
+⊆-skip [] ys zs p = p
+⊆-skip (x ∷ xs) ys zs p = Z ∷ (⊆-suc (⊆-skip xs ys zs p))
+
+⊆++-refl : ∀ {a} {A : Set a} →
+           (xs ys : List A) →
+           xs ⊆ (xs ++ ys)
+⊆++-refl [] ys = []
+⊆++-refl (x ∷ xs) ys = Z ∷ (⊆-suc (⊆++-refl xs ys))
+
+⊆++-l-refl : ∀ {a} {A : Set a} →
+                   (xs ys : List A) →
+                   xs ⊆ (ys ++ xs)
+⊆++-l-refl xs [] = ⊆-refl
+⊆++-l-refl xs (x ∷ ys) = ⊆-suc (⊆++-l-refl xs ys)
+
+∈-inc : ∀ {a} {A : Set a}
+              (xs ys : List A) →
+              (x : A) →
+              x ∈ xs →
+              x ∈ (xs ++ ys)
+∈-inc _ ys x Z = Z
+∈-inc _ ys x (S p) = S (∈-inc _ ys x p)
+
+⊆-inc : ∀ {a} {A : Set a}
+              (xs ys zs : List A) →
+              xs ⊆ ys →
+              (xs ++ zs) ⊆ (ys ++ zs)
+⊆-inc [] [] zs p = ⊆-refl
+⊆-inc [] (x ∷ ys) zs p = ⊆++-l-refl zs (x ∷ ys)
+⊆-inc (x ∷ xs) ys zs (px ∷ p) = ∈-inc ys zs x px ∷ (⊆-inc xs ys zs p)
+
+⊆++comm : ∀ {a} {A : Set a}
+            (xs ys zs : List A) →
+            ((xs ++ ys) ++ zs) ⊆ (xs ++ (ys ++ zs))
+⊆++comm [] ys zs = ⊆-refl
+⊆++comm (x ∷ xs) ys zs = Z ∷ (⊆-suc (⊆++comm xs ys zs))
+
+⊆++comm' : ∀ {a} {A : Set a}
+           (xs ys zs : List A) →
+           (xs ++ ys ++ zs) ⊆ ((xs ++ ys) ++ zs)
+⊆++comm' [] ys zs = ⊆-refl
+⊆++comm' (x ∷ xs) ys zs = Z ∷ ⊆-suc (⊆++comm' xs ys zs)
+
+pad-pointer : ∀ {a} {A : Set a} → (l r : List A) → {v : A} → v ∈ r → v ∈ (l ++ r)
+pad-pointer [] r p = p
+pad-pointer (x ∷ l) r p = S (pad-pointer l r p)
+
+record ElemInList {a} {A : Set a} (ls : List A) : Set a where
+  field
+    elem : A
+    in-list : elem ∈ ls
+
+tabulate-suc : ∀ {a} {A : Set a} → {ls : List A} → {x : A} → List (ElemInList ls) → List (ElemInList (x ∷ ls))
+tabulate-suc [] = []
+tabulate-suc (eil ∷ tabs) =
+  let rec = tabulate-suc tabs
+      open ElemInList
+  in record { elem = eil .elem ; in-list = S (eil .in-list) } ∷ rec
+
+tabulate-∈ : ∀ {a} {A : Set a} → (ls : List A) → List (ElemInList ls)
+tabulate-∈ [] = []
+tabulate-∈ (x ∷ ls) =
+  let rec = tabulate-∈ ls
+  in record { elem = x ; in-list = Z } ∷ tabulate-suc rec
+
 \end{code}

src/NatProps.agda

@@ -0,0 +1,13 @@
+module NatProps where
+open import Data.Nat using (ℕ ; _≟_ ; _<_ ; zero ; suc ; s≤s)
+open import Data.Nat.Properties using (s≤s-injective)
+open import Relation.Nullary using (Dec ; yes ; no ; ¬_)
+open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym)
+open import Data.Empty using (⊥)
+
+<-¬≡ : ∀ {n m} → n < m → ¬ n ≡ m
+<-¬≡ {zero} {zero} ()
+<-¬≡ {zero} {suc m} p = λ ()
+<-¬≡ {suc n} {zero} p = λ ()
+<-¬≡ {suc n} {suc m} (Data.Nat.s≤s p) with (<-¬≡ p)
+... | q = λ { refl → q refl }