Mercurial > hg > Members > kono > Proof > automaton

changeset 381:113330c6e896

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 24 Jul 2023 15:49:41 +0900
parents 646ce1064288
children 9fba498b0a7a
files automaton-in-agda/src/derive.agda automaton-in-agda/src/deriveUtil.agda
diffstat 2 files changed, 37 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/derive.agda	Mon Jul 24 14:29:12 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Mon Jul 24 15:49:41 2023 +0900
@@ -211,13 +211,32 @@
      fb00 record { s = (z & (x *)) ; is-sub = (sub*& z x lt is-sub) } = case1 record { z = z ; is-sub = is-sub ; lt = lt }
 
 toSB : (r : Regex   Σ) →  ISB r → Bool
-toSB r cr = ?
+toSB r record { s = s ; is-sub = is-sub } with rg-eq? r s
+... | yes _ = true
+... | no _ = false
 
 sbempty? : (r : Regex Σ) → (ISB r → Bool) → Bool
-sbempty? r = ?
+sbempty? ε f with f record { s = ε ; is-sub = sunit  }
+... | true = true
+... | false = false
+sbempty? φ f = false
+sbempty? (r *) f with f record { s = r * ; is-sub = sunit  }
+... | true = true 
+... | false = false 
+sbempty? (r & r₁) f with f record { s = r & r₁ ; is-sub = sunit  }
+... | false = false
+... | true = empty? r /\ empty? r₁
+sbempty? (r || r₁) f with f record { s = r || r₁ ; is-sub = sunit  }
+... | false = false
+... | true = empty? r \/ empty? r₁ 
+sbempty? < x > f = false
 
 sbderive : (r : Regex Σ) →  (ISB r → Bool) → Σ → ISB r  → Bool
-sbderive = ?
+sbderive r f s record { s = t ; is-sub = is-sub } with rg-eq? (derivative r s) t | f record { s = r ; is-sub = sunit  }
+... | yes _ | true = true
+... | no _ | true = false
+... | yes _ | false = false
+... | no _ | false = false
 
 -- finDerive : (r : Regex Σ) → FiniteSet (Derived r)
 --    this is not correct because it contains s || s || s || .....
--- a/automaton-in-agda/src/deriveUtil.agda	Mon Jul 24 14:29:12 2023 +0900
+++ b/automaton-in-agda/src/deriveUtil.agda	Mon Jul 24 15:49:41 2023 +0900
@@ -58,12 +58,21 @@
 open import derive alpha2 fin-a a-eq?
 test11 = regex→automaton ( < a > & < b > )
 
-test12 = accept test11 record { state =  < a > & < b > ; is-derived = unit } ( a ∷ b ∷ [] )
-test13 = accept test11 record { state =  < a > & < b > ; is-derived = unit } ( a ∷ a ∷ [] )
+test12 = accept test11 record { state =  < a > & < b > ; is-derived = unit refl } ( a ∷ b ∷ [] )
+test13 = accept test11 record { state =  < a > & < b > ; is-derived = unit refl } ( a ∷ a ∷ [] )
 
 test14 = regex-match ( (  < a > & < b > ) * ) ( a ∷ b ∷ a ∷ a ∷ [] )
 
-test15 = regex-derive ( (  < a > & < b > ) * ∷ [] )
-test16 = regex-derive test15
-test17 : regex-derive test16 ≡ test16
-test17 = refl
+test15 = derive-step ( ( < a > & < b > ) * ) record { state = ( < a > & < b > ) *  ; is-derived = unit refl } a
+-- test16 = derive-step ? -- test15
+-- test17 : derive-step ? -- test16 ≡ test16
+-- test17 = refl
+
+stest11 = regex→automaton1 ( < a > & < b > )
+stest12 = accept stest11 (toSB ( < a > & < b > )) ( a ∷ b ∷ [] )
+stest13 = accept stest11 (toSB ( < a > & < b > )) ( a ∷ a ∷ [] )
+
+
+
+
+