Mercurial > hg > Members > kono > Proof > automaton
changeset 276:a14999c44cf9
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 20 Dec 2021 07:54:09 +0900 |
| parents | 7828beb7d849 |
| children | 42563cc6afdf |
| files | automaton-in-agda/src/cfg.agda automaton-in-agda/src/cfg1.agda |
| diffstat | 2 files changed, 12 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/automaton-in-agda/src/cfg.agda Sat Dec 18 19:34:19 2021 +0900 +++ b/automaton-in-agda/src/cfg.agda Mon Dec 20 07:54:09 2021 +0900 @@ -11,7 +11,7 @@ open import Relation.Nullary using (¬_; Dec; yes; no) -- open import Data.String --- open import nfa +left : {t : Set } → List data IsTerm (Token : Set) : Set where isTerm : Token → IsTerm Token
--- a/automaton-in-agda/src/cfg1.agda Sat Dec 18 19:34:19 2021 +0900 +++ b/automaton-in-agda/src/cfg1.agda Mon Dec 20 07:54:09 2021 +0900 @@ -235,19 +235,26 @@ pda-ce-test2 = PushDownAutomaton.paccept pnc c1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ [] ) [] pda-ce-test3 = PushDownAutomaton.paccept pnc c1 ( e[ ∷ e1 ∷ e] ∷ e1 ∷ [] ) [] -record PNC : Set where +record PNC (accept : Bool ) : Set where field - pnc-q : CG1 + orig-x : List E1Token + pnc-q : CG1 pnc-st : List CG1 + pnc-p : CG1 → List CG1 → Bool + success : accept ≡ true → pnc-p pnc-q pnc-st ≡ true → PushDownAutomaton.paccept pnc c1 orig-x [] ≡ true + failure : accept ≡ false → pnc-p pnc-q pnc-st ≡ false → PushDownAutomaton.paccept pnc c1 orig-x [] ≡ false open import Data.Unit {-# TERMINATING #-} -expr1P : {n : Level } {t : Set n } → (x : List E1Token ) → PNC → ( fail : List E1Token → PNC → t ) → ( next : List E1Token → PNC → t ) → t +expr1P : {n : Level } {t : Set n } → (x : List E1Token ) → PNC true + → ( fail : List E1Token → PNC false → t ) → ( next : List E1Token → PNC true → t ) → t expr1P x _ _ _ = {!!} expr1P-test : (x : List E1Token ) → ⊤ -expr1P-test x = expr1P x record {pnc-q = c1 ; pnc-st = [] } (λ x p → {!!} ) (λ x p → {!!} ) +expr1P-test x = expr1P x record { orig-x = x ; pnc-q = c1 ; pnc-st = [] + ; pnc-p = λ q st → PushDownAutomaton.paccept pnc q x st ; success = λ _ p → p ; failure = λ _ p → p } + (λ x p → {!!} ) (λ x p → {!!} )