Merge pull request #62 from pmbittner/find-inconsistencies

Create a script for finding inconsistencies

scripts/find-inconsistency-sources.sh

@@ -0,0 +1,82 @@
+#!/usr/bin/env bash
+
+cd "$(dirname ${BASH_SOURCE[0]})/.."
+
+possible-inconsistencies() {
+  echo 'postulates:'
+  grep 'postulate' -r src --include '*agda*'
+
+  echo
+  echo 'terminating pragmas:'
+  grep 'TERMINATING' -r src --include '*agda*'
+
+  echo
+  echo 'holes:'
+  (
+    grep -F '{!' -r src --include '*agda*'
+    grep ' ?\( \|$\)' -r src --include '*agda*'
+  )
+}
+
+with-doc() {
+  # Used for alignment.
+  # Cannot use 'column' because it doesn't exist on MAC.
+  columnCount="$(possible-inconsistencies | awk 'BEGIN { max=0 } { if (max < length($0)) max=length($0) } END { print max }')"
+
+  POSIXLY_CORRECT=1 awk '
+    BEGIN {
+      doc[""]=""
+      doc["postulates:"]=""
+      doc["terminating pragmas:"]=""
+      doc["holes:"]=""
+
+      doc["src/Util/String.agda:  where postulate trustMe : _"]="Also proposed in the Agda issue tracker to make String propositions provable. Only used in examples."
+      # Note: this above postulate appears four times
+      doc["src/Show/Lines.agda:{-# NON_TERMINATING #-}"]="Only used for printing and thus not proof relevant. Also, NON_TERMINATING functions do not reduce during type checking."
+      doc["src/Tutorial/A_NewLanguage.lagda.md:We are using the `{-# TERMINATING -#}` flag here:"]="This is actually a comment."
+      doc["src/Tutorial/A_NewLanguage.lagda.md:{-# TERMINATING #-}"]="Simplification of the tutorial. Not used in the anything else."
+      doc["src/Tutorial/A_NewLanguage.lagda.md:MyConfig = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
+      doc["src/Tutorial/A_NewLanguage.lagda.md:⟦_⟧ = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
+      doc["src/Tutorial/B_Translation.lagda.md:conf e c²ᶜᶜ = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
+      doc["src/Tutorial/B_Translation.lagda.md:fnoc e cᵐʸ = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
+      doc["src/Tutorial/B_Translation.lagda.md:preservation-⊆[] e c = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
+      doc["src/Tutorial/B_Translation.lagda.md:preservation-⊇[] e c = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
+      doc["src/Tutorial/B_Translation.lagda.md:translate (D ⟨ l , r ⟩) = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
+      doc["src/Tutorial/B_Translation.lagda.md:translate (a -< cs >-)  = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
+      doc["src/Tutorial/C_Proofs.lagda.md:  {!!}   -- write down the proof of correctness in this hole"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
+      doc["src/Tutorial/C_Proofs.lagda.md:  {!!} , -- write down the expression in this hole"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
+      doc["src/Tutorial/C_Proofs.lagda.md:2CC≽MyLang = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
+      doc["src/Tutorial/C_Proofs.lagda.md:MyLang-is-Sound = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
+
+      exitCode=0
+    }
+
+    {
+      padding='"$columnCount"' - length($0) + 3
+      if ($0 in doc) {
+        printf "%s% *s%s\n", $0, padding, "", doc[$0]
+      } else {
+        printf "\033[30;41m%s% *s%s\033[39;49m\n", $0, padding, "", "UNDOCUMENTED!!!"
+        exitCode=1
+      }
+    }
+
+    END {
+      exit exitCode
+  }
+  '
+}
+
+if [ "$1" = "--with-documentation" ]
+then
+  possible-inconsistencies | with-doc
+  exitCode=$?
+else
+  possible-inconsistencies
+  exitCode=$?
+fi
+
+echo
+echo "Hint: Use '$0 --with-documentation | less -S' to be able to see documentation to each source and to scroll horizontally"
+
+exit $exitCode

src/Framework/Compiler.agda

@@ -93,32 +93,3 @@ _⊕_ {V} {Γ₁} {Γ₂} {Γ₃} L₁→L₂ L₂→L₃ = record
         -- this pattern is very similar of ⊆[]-trans
         p : ∀ {A : 𝔸} (e : L₁ A) → ⟦ e ⟧₁ ≅[ conf' e ][ fnoc' e ] ⟦ compile L₂→L₃ (compile L₁→L₂ e) ⟧₃
         p e = ≅[]-trans (preserves L₁→L₂ e) (preserves L₂→L₃ (compile L₁→L₂ e))
-
--- _⊕ᶜ_ : ∀ {K} {VC₁ VC₂ VC₃ : VariabilityConstruct K}
---   → ConstructCompiler VC₁ VC₂
---   → ConstructCompiler VC₂ VC₃
---   → ConstructCompiler VC₁ VC₃
--- _⊕ᶜ_ {K} {VC₁} {_} {VC₃} 1→2 2→3 = record
---   { compile = compile 2→3 ∘ compile 1→2
---   ; config-compiler = cc
---   ; stable = stb
---   ; preserves = Pres.p
---   }
---   where open ConstructCompiler
---         open VariabilityConstruct VC₁ renaming (Construct to C₁; construct-semantics to sem₁)
---         open VariabilityConstruct VC₃ renaming (construct-semantics to sem₃)
-
---         cc : ConfigCompiler K K
---         cc = config-compiler 1→2 ⊕ᶜᶜ config-compiler 2→3
-
---         stb : Ktable cc
---         stb = ⊕ᶜᶜ-stable (config-compiler 1→2) (config-compiler 2→3) (stable 1→2) (stable 2→3)
-
---         module Pres {V : 𝕍} {A : 𝔸} where
---           open IVSet V A using (_≅_; ≅-trans)
-
---           p : ∀ {Γ : VariabilityLanguage V K}
---               → (c : C₁ (Expression Γ) A)
---               → sem₁ Γ id c ≅ sem₃ Γ (to cc) (compile 2→3 (compile 1→2 c))
---           p c = ≅-trans (preserves 1→2 c) {!preserves 2→3 (compile 1→2 c)!} --
---           -- p c₁ = ≅-trans (preserves 1→2 c₁) (preserves 2→3 (compile 1→2 c₁))

src/Lang/FST.agda

@@ -168,9 +168,6 @@ module Impose (AtomSet : 𝔸) where
   _==_ : ∀ {i} → Decidable (_≈_ {AtomSet} {i})
   (a -< _ >-) == (b -< _ >-) = a ≟ b
 
-  -- ≟-refl : ∀ (x : A) → x ≡ x
-  -- ≟-refl = {!!}
-
   mutual
     infixr 5 _⊕_
     _⊕_ : ∀ {i} → List (FSTA i) → List (FSTA i) → List (FSTA i)