From 9cb56dabb676391a9382731347e8d2b07b9437a5 Mon Sep 17 00:00:00 2001 From: Peter Mikkelsen Date: Sun, 7 Apr 2024 13:25:49 +0200 Subject: big cleanup --- .../_tmp/agda-dfa/Agda.Primitive.Cubical.html | 55 ---------- .../_tmp/agda-dfa/Agda.Primitive.html | 35 ------- sites/pmikkelsen.com/_tmp/agda-dfa/Agda.css | 39 ------- sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html | 115 --------------------- 4 files changed, 244 deletions(-) delete mode 100644 sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html delete mode 100644 sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html delete mode 100644 sites/pmikkelsen.com/_tmp/agda-dfa/Agda.css delete mode 100644 sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html (limited to 'sites/pmikkelsen.com/_tmp') diff --git a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html deleted file mode 100644 index 1be20f5..0000000 --- a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html +++ /dev/null @@ -1,55 +0,0 @@ - -Agda.Primitive.Cubical
{-# OPTIONS --cubical --no-subtyping #-}
-
-module Agda.Primitive.Cubical where
-
-{-# BUILTIN INTERVAL I  #-}  -- I : Setω
-
-{-# BUILTIN IZERO    i0 #-}
-{-# BUILTIN IONE     i1 #-}
-
-infix  30 primINeg
-infixr 20 primIMin primIMax
-
-primitive
-    primIMin : I → I → I
-    primIMax : I → I → I
-    primINeg : I → I
-
-{-# BUILTIN ISONE    IsOne    #-}  -- IsOne : I → Setω
-
-postulate
-  itIsOne : IsOne i1
-  IsOne1  : ∀ i j → IsOne i → IsOne (primIMax i j)
-  IsOne2  : ∀ i j → IsOne j → IsOne (primIMax i j)
-
-{-# BUILTIN ITISONE  itIsOne  #-}
-{-# BUILTIN ISONE1   IsOne1   #-}
-{-# BUILTIN ISONE2   IsOne2   #-}
-
--- Partial : ∀{ℓ} (i : I) (A : Set ℓ) → Set ℓ
--- Partial i A = IsOne i → A
-
-{-# BUILTIN PARTIAL  Partial  #-}
-{-# BUILTIN PARTIALP PartialP #-}
-
-postulate
-  isOneEmpty : ∀ {ℓ} {A : Partial i0 (Set ℓ)} → PartialP i0 A
-
-{-# BUILTIN ISONEEMPTY isOneEmpty #-}
-
-primitive
-  primPOr : ∀ {ℓ} (i j : I) {A : Partial (primIMax i j) (Set ℓ)}
-            → (u : PartialP i (λ z → A (IsOne1 i j z)))
-            → (v : PartialP j (λ z → A (IsOne2 i j z)))
-            → PartialP (primIMax i j) A
-
-  -- Computes in terms of primHComp and primTransp
-  primComp : ∀ {ℓ} (A : (i : I) → Set (ℓ i)) {φ : I} (u : ∀ i → Partial φ (A i)) (a : A i0) → A i1
-
-syntax primPOr p q u t = [ p ↦ u , q ↦ t ]
-
-primitive
-  primTransp : ∀ {ℓ} (A : (i : I) → Set (ℓ i)) (φ : I) (a : A i0) → A i1
-  primHComp  : ∀ {ℓ} {A : Set ℓ} {φ : I} (u : ∀ i → Partial φ A) (a : A) → A
-
\ No newline at end of file diff --git a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html deleted file mode 100644 index 5829754..0000000 --- a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html +++ /dev/null @@ -1,35 +0,0 @@ - -Agda.Primitive
-- The Agda primitives (preloaded).
-
-{-# OPTIONS --without-K --no-subtyping #-}
-
-module Agda.Primitive where
-
-------------------------------------------------------------------------
--- Universe levels
-------------------------------------------------------------------------
-
-infixl 6 _⊔_
-
--- Level is the first thing we need to define.
--- The other postulates can only be checked if built-in Level is known.
-
-postulate
-  Level : Set
-
--- MAlonzo compiles Level to (). This should be safe, because it is
--- not possible to pattern match on levels.
-
-{-# BUILTIN LEVEL Level #-}
-
-postulate
-  lzero : Level
-  lsuc  : (ℓ : Level) → Level
-  _⊔_   : (ℓ₁ ℓ₂ : Level) → Level
-
-{-# BUILTIN LEVELZERO lzero #-}
-{-# BUILTIN LEVELSUC  lsuc  #-}
-{-# BUILTIN LEVELMAX  _⊔_   #-}
-
-{-# BUILTIN SETOMEGA Setω #-}
-
\ No newline at end of file diff --git a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.css b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.css deleted file mode 100644 index 3a4b225..0000000 --- a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.css +++ /dev/null @@ -1,39 +0,0 @@ -/* Aspects. */ -.Agda .Comment { color: #B22222 } -.Agda .Background {} -.Agda .Markup { color: #000000 } -.Agda .Keyword { color: #CD6600 } -.Agda .String { color: #B22222 } -.Agda .Number { color: #A020F0 } -.Agda .Symbol { color: #404040 } -.Agda .PrimitiveType { color: #0000CD } -.Agda .Pragma { color: black } -.Agda .Operator {} - -/* NameKinds. */ -.Agda .Bound { color: black } -.Agda .Generalizable { color: black } -.Agda .InductiveConstructor { color: #008B00 } -.Agda .CoinductiveConstructor { color: #8B7500 } -.Agda .Datatype { color: #0000CD } -.Agda .Field { color: #EE1289 } -.Agda .Function { color: #0000CD } -.Agda .Module { color: #A020F0 } -.Agda .Postulate { color: #0000CD } -.Agda .Primitive { color: #0000CD } -.Agda .Record { color: #0000CD } - -/* OtherAspects. */ -.Agda .DottedPattern {} -.Agda .UnsolvedMeta { color: black; background: yellow } -.Agda .UnsolvedConstraint { color: black; background: yellow } -.Agda .TerminationProblem { color: black; background: #FFA07A } -.Agda .IncompletePattern { color: black; background: #F5DEB3 } -.Agda .Error { color: red; text-decoration: underline } -.Agda .TypeChecks { color: black; background: #ADD8E6 } -.Agda .Deadcode { color: black; background: #808080 } -.Agda .ShadowingInTelescope { color: black; background: #808080 } - -/* Standard attributes. */ -.Agda a { text-decoration: none } -.Agda a[href]:hover { background-color: #B4EEB4 } diff --git a/sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html b/sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html deleted file mode 100644 index 308e205..0000000 --- a/sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html +++ /dev/null @@ -1,115 +0,0 @@ - -DFA
module DFA where
-
--- A pair type 
-record _×_ (A B : Set) : Set where
-  constructor _,_
-  field
-    fst : A
-    snd : B
-
--- A list type
-infixr 5 _∷_
-data List (a : Set) : Set where
-  [] : List a
-  _∷_ : a → List a → List a
-
--- Elements of type x ∈ xs is a proof that x is somewhere in xs
-data _∈_ {A : Set}(x : A) : (xs : List A) → Set where
-  here : ∀ {xs} → x ∈ (x ∷ xs)
-  there : ∀ {y xs} → x ∈ xs → x ∈ (y ∷ xs)
-
--- Elements of type a ≡ b is a proof that a and b are the same
-data _≡_ {A : Set}(x : A) : A → Set where
-  refl : x ≡ x
-
--- The empty type. There are no members of this type, so it is the same as false
-data ⊥ : Set where
-
--- Negation is defined by a function that takes a proof and returns ⊥, which is impossible. In agda an inhabited type means a proof, and an uninhabited means no proof.
-¬_ : Set → Set
-¬ A = A → ⊥
-
--- A DFA is a five tuple of Q Σ q₀ δ F
-record DFA (Q : Set) (Σ : Set) (q₀ : Q) (δ : Q × Σ → Q) (F : List Q) : Set where
-
--- The DFArun data type keeps track of a running dfa.
-data DFArun {Q Σ q₀ δ F}(dfa : DFA Q Σ q₀ δ F) : (q : Q) → (w : List Σ) → Set where
-  empty : {q : Q} → q ∈ F → DFArun dfa q []
-  acceptOne : {ws : List Σ} →
-              (w : Σ) →
-              (q : Q) →
-              DFArun dfa (δ (q , w)) ws →
-              DFArun dfa q (w ∷ ws)
-
--- Accepts dfa w is a proof that running the dfa with input w is possible form the start state q₀
-data Accepts {Q Σ q₀ δ F}(dfa : DFA Q Σ q₀ δ F) : (w : List Σ) → Set where
-  accepts : ∀{w} → DFArun dfa q₀ w → Accepts dfa w
-
--- CantAccept dfa q w is a proof that running the dfa on imput w is impossible if we want to start at state q₀. It has to start in q instead.
-data CantAccept {Q Σ q₀ δ F}(dfa : DFA Q Σ q₀ δ F) : (q : Q) → (w : List Σ) → Set where
-  cantAccept : ∀ {w q} → DFArun dfa q w → ¬(q ≡ q₀) → CantAccept dfa q w
-
-
--- w ∈Lang dfa gives either a proof that w is in the language of the dfa, or that it isn't.
-data _∈Lang_ {Q Σ q₀ δ F}(w : List Σ)(dfa : DFA Q Σ q₀ δ F) : Set where
-  inLang : Accepts dfa w → w ∈Lang dfa
-  notInLang : ∀{q} → CantAccept dfa q w → w ∈Lang dfa
-
-
-
-
--- Test stuff. Create a DFA which only accepts an input with an even number of a's
-
-data TestQ : Set where
-  evenNumberOfAs : TestQ
-  oddNumberOfAs : TestQ
-
-data TestΣ : Set where
-  a : TestΣ
-  b : TestΣ
-
-Testδ : TestQ × TestΣ → TestQ
-Testδ (evenNumberOfAs , a) = oddNumberOfAs
-Testδ (evenNumberOfAs , b) = evenNumberOfAs
-Testδ (oddNumberOfAs , a) = evenNumberOfAs
-Testδ (oddNumberOfAs , b) = oddNumberOfAs
-
-TestF : List TestQ
-TestF = evenNumberOfAs ∷ []
-
-TestDFA : DFA TestQ TestΣ evenNumberOfAs Testδ TestF
-TestDFA = _ -- Since a DFA is a record with no fields, agda can infer it
-
--- Try to construct proofs for different input strings
-
-input₁ input₂ input₃ : List TestΣ
-input₁ = [] -- Empty string
-input₂ = a ∷ b ∷ a ∷ a ∷ b ∷ [] -- Three a's
-input₃ = b ∷ b ∷ a ∷ b ∷ a ∷ [] -- Two a's
-
-
--- The proofs are found automatically by agda, and no other proofs would type check
-proof₁ : input₁ ∈Lang TestDFA -- Proof that input₁ is in the language
-proof₁ = inLang (accepts (empty here))
-
-proof₂ : input₂ ∈Lang TestDFA -- Proof that input₂ is not in the language
-proof₂ = notInLang
-           (cantAccept
-            (acceptOne a oddNumberOfAs
-             (acceptOne b evenNumberOfAs
-              (acceptOne a evenNumberOfAs
-               (acceptOne a oddNumberOfAs
-                (acceptOne b evenNumberOfAs (empty here))))))
-            (λ ()))
-
-proof₃ : input₃ ∈Lang TestDFA -- Proof that input₃ is in the language
-proof₃ = inLang
-           (accepts
-            (acceptOne b evenNumberOfAs
-             (acceptOne b evenNumberOfAs
-              (acceptOne a evenNumberOfAs
-               (acceptOne b oddNumberOfAs
-                (acceptOne a oddNumberOfAs (empty here)))))))
-
-
\ No newline at end of file -- cgit v1.2.3