From 80670b447b973820643cfe63f4607eb6973c348c Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Thu, 4 Jul 2024 15:19:15 +0200 Subject: [PATCH 1/2] Remove obsolete commented code with holes --- src/Framework/Compiler.agda | 29 ----------------------------- src/Lang/FST.agda | 3 --- 2 files changed, 32 deletions(-) diff --git a/src/Framework/Compiler.agda b/src/Framework/Compiler.agda index 91de6ea8..57a734c4 100644 --- a/src/Framework/Compiler.agda +++ b/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₁)) diff --git a/src/Lang/FST.agda b/src/Lang/FST.agda index 7a5ba31c..b68b37d6 100644 --- a/src/Lang/FST.agda +++ b/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) From 3a2c1bde28275e946065b636f778ba2faa8dc02b Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Thu, 4 Jul 2024 17:16:03 +0200 Subject: [PATCH 2/2] Create a script for finding and documenting inconsistency sources --- scripts/find-inconsistency-sources.sh | 82 +++++++++++++++++++++++++++ 1 file changed, 82 insertions(+) create mode 100755 scripts/find-inconsistency-sources.sh diff --git a/scripts/find-inconsistency-sources.sh b/scripts/find-inconsistency-sources.sh new file mode 100755 index 00000000..b564dd76 --- /dev/null +++ b/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