Agda.Primitive.Cubical

From 9b3a308c7248fd2fa94162e4401726327cc66aa3 Mon Sep 17 00:00:00 2001 From: Peter Mikkelsen Date: Wed, 23 Jun 2021 16:20:51 +0000 Subject: Add some agda test --- .../_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 insertions(+) create mode 100644 sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html create mode 100644 sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html create mode 100644 sites/pmikkelsen.com/_tmp/agda-dfa/Agda.css create mode 100644 sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html (limited to 'sites') diff --git a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html new file mode 100644 index 0000000..1be20f5 --- /dev/null +++ b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html @@ -0,0 +1,55 @@ + +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 new file mode 100644 index 0000000..5829754 --- /dev/null +++ b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html @@ -0,0 +1,35 @@ + +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 new file mode 100644 index 0000000..3a4b225 --- /dev/null +++ b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.css @@ -0,0 +1,39 @@ +/* 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 new file mode 100644 index 0000000..308e205 --- /dev/null +++ b/sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html @@ -0,0 +1,115 @@ + +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