[Agda] Type mismatch? Tipo miskongruas?
Serge Leblanc
33dbqnxpy7if at gmail.com
Thu Sep 13 17:01:48 CEST 2018
Dear all, how do indicate that p₀ and p have the same type in this above
example? Apparently, {R = R} is not enough.
Estimata ĉiuj, kiel oni indikas ke p₀ kaj p havas la saman tipon en ĉi
supra ekzemplo ? Ŝajne, {R = R} ne sufiŝas.
{-# NON_TERMINATING #-}
parse′ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
parse′ {R} p₀ = parse″ p₀
where
parse″ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
parse″ {xs = xs} p [] = Colist.fromList xs
parse″ {R = R}{xs = xs} p (t ∷ s) with t ≐ '\n'
... | false = parse″ (∂ p t) (♭ s)
... | true = (Colist.fromList xs) ++ (parse″ p₀ (♭ s))
Sinceran dankon pro via venonta helpo.
--
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180913/c6f3a560/attachment.html>
-------------- next part --------------
module Short3 where
open import Coinduction --using (♯_ ; ♭ ; ∞)
open import Codata.Musical.Colist as Colist using (Colist ; [] ; _∷_ ; [_] ; _++_ ; fromList)
open import Codata.Musical.Costring
open import Data.List as List renaming ([] to ⟬⟭ ; [_] to ⟬_⟭ ; _++_ to _⊎_ ) -- U+27EC U+27ED U+228E
open import Data.Char renaming (_==_ to _≐_ ; show to toString) -- U+2250
open import Data.String as String renaming (_==_ to _≛_ ; _++_ to _⊍_; show to showString) -- U+225B U+228D
open import Data.Bool using (Bool ; true ; false ; if_then_else_ ; _∧_)
open import IO renaming (_>>=_ to _>>=IO_)
using (run ; getContents ; mapM′ ; putStrLn)
------------------------------------------------------------------------
-- Helper functions
open import Function using (_$_ ; _∘_ ; _∘′_)
open import Data.Maybe
open import Level using (zero)
open import Data.List.Categorical using (monadPlus)
open import Category.Monad
open RawMonadPlus {f = Level.zero} Data.List.Categorical.monadPlus
using ()
renaming (_>>=_ to _>>=′_)
infix 7 _⋆ _+
infixl 6 _>>=_ _>>=app_
infixl 5 _∣_
flatten : {A : Set} → Maybe (List A) → List A
flatten nothing = ⟬⟭
flatten (just xs) = xs
app : {A B : Set} → Maybe (A → List B) → A → List B
app nothing x = ⟬⟭
app (just f) x = f x
_>>=app_ : {A B : Set} → List A → Maybe (A → List B) → List B
xs >>=app nothing = ⟬⟭
xs >>=app just f = xs >>=′ f
------------------------------------------------------------------------
-- Parsers
mutual
data Parser : (R : Set) → List R → Set₁ where
return : ∀ {R} (x : R) → Parser R ⟬ x ⟭
flush : ∀ {R} → Parser R ⟬⟭
fail : ∀ {R} → Parser R ⟬⟭
token : Parser Char ⟬⟭
_∣_ : ∀ {R xs₁ xs₂}
(p₁ : Parser R xs₁ )
(p₂ : Parser R xs₂) →
Parser R (xs₁ List.++ xs₂)
_>>=_ : ∀ {R₁ R₂ xs} {f : Maybe (R₁ → List R₂)}
(p₁ : ∞⟨ f ⟩Parser R₁ (flatten xs) )
(p₂ : (x : R₁) → ∞⟨ xs ⟩Parser R₂ (app f x)) →
Parser R₂ (flatten xs >>=app f)
∞⟨_⟩Parser : {R₂ : Set} → Maybe R₂ → (R₁ : Set) → List R₁ → Set₁
∞⟨ nothing ⟩Parser R₁ xs = ∞ (Parser R₁ xs)
∞⟨ just _ ⟩Parser R₁ xs = Parser R₁ xs
------------------------------------------------------------------------
-- Derived combinators
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Data.Nat using (ℕ ; _≤?_ ; _∸_ ; _*_ ; _+_)
open import Data.Nat.Show renaming (show to showℕ)
sat : ∀ {R} → (Char → Maybe R) → Parser R ⟬⟭
sat {R} p = token >>= (ok ∘ p)
where
ok-index : Maybe R → List R
ok-index nothing = ⟬⟭
ok-index (just x) = ⟬ x ⟭
ok : (x : Maybe R) → Parser R (ok-index x)
ok nothing = fail
ok (just x) = return x
tok : Char → Parser Char ⟬⟭
tok t = sat (λ t′ → if t ≐ t′ then just t′ else nothing)
return⋆ : ∀ {R} (xs : List R) → Parser R xs
return⋆ ⟬⟭ = fail
return⋆ (x ∷ xs) = return x ∣ return⋆ xs
mutual
_⋆ : ∀ {R} → Parser R ⟬⟭ → Parser (List R) _
p ⋆ = return ⟬⟭ ∣ p +
_+ : ∀ {R} → Parser R ⟬⟭ → Parser (List R) _
p + = p >>= λ x → ♯ (
p ⋆ >>= λ xs →
return (x ∷ xs) )
digit = sat (λ t → if in-range t then just (to-number t) else nothing)
where
in-range : Char → Bool
in-range t = ⌊ toNat '0' ≤? toNat t ⌋ ∧
⌊ toNat t ≤? toNat '9' ⌋
to-number : Char → ℕ
to-number t = toNat t ∸ toNat '0'
number = digit + >>= return ∘ foldl (λ n d → 10 * n + d) 0
------------------------------------------------------------------------
-- Parser interpreter
delayed? : ∀ {R R′ xs} {m : Maybe R′} → ∞⟨ m ⟩Parser R xs → Maybe R′
delayed? {m = m} _ = m
delayed?′ : ∀ {R₁ R₂ R′ : Set} {m : Maybe R′} {f : R₁ → List R₂} →
((x : R₁) → ∞⟨ m ⟩Parser R₂ (f x)) → Maybe R′
delayed?′ {m = m} _ = m
∂-initial : ∀ {R xs} → Parser R xs → Char → List R
∂-initial (return x) t = ⟬⟭
∂-initial fail t = ⟬⟭
∂-initial flush t = ⟬⟭
∂-initial token t = ⟬ t ⟭
∂-initial (p₁ ∣ p₂) t = ∂-initial p₁ t List.++ ∂-initial p₂ t
∂-initial (p₁ >>= p₂) t with delayed? p₁ | delayed?′ p₂
... | just f | nothing = ∂-initial p₁ t >>=′ f
... | just f | just xs = (∂-initial p₁ t >>=′ f) List.++
(xs >>=′ λ x → ∂-initial (p₂ x) t)
... | nothing | nothing = ⟬⟭
... | nothing | just xs = xs >>=′ λ x → ∂-initial (p₂ x) t
∂ : ∀ {R xs} (p : Parser R xs) (t : Char) → Parser R (∂-initial p t)
∂ (return x) t = fail
∂ fail t = fail
∂ flush t = fail
∂ token t = return t
∂ (p₁ ∣ p₂) t = ∂ p₁ t ∣ ∂ p₂ t
∂ (p₁ >>= p₂) t with delayed? p₁ | delayed?′ p₂
... | just f | nothing = ∂ p₁ t >>= (λ x → ♭ (p₂ x))
... | just f | just xs = ∂ p₁ t >>= (λ x → p₂ x)
∣ return⋆ xs >>= λ x → ∂ (p₂ x) t
... | nothing | nothing = ♯ ∂ (♭ p₁) t >>= (λ x → ♭ (p₂ x))
... | nothing | just xs = ♯ ∂ (♭ p₁) t >>= (λ x → p₂ x)
∣ return⋆ xs >>= λ x → ∂ (p₂ x) t
parse : ∀ {R xs} → Parser R xs → List Char → List R
parse {xs = xs} p ⟬⟭ = xs
parse p (t ∷ s) = parse (∂ p t) s
data Expr : Set where
num : (n : ℕ) → Expr
plus : (e₁ e₂ : Expr) → Expr
times : (e₁ e₂ : Expr) → Expr
⟦_⟧ : Expr → ℕ
⟦ num n ⟧ = n
⟦ plus e₁ e₂ ⟧ = ⟦ e₁ ⟧ + ⟦ e₂ ⟧
⟦ times e₁ e₂ ⟧ = ⟦ e₁ ⟧ * ⟦ e₂ ⟧
showExpr : Expr → String
showExpr (num n) = "(num " ⊍ (showℕ n) ⊍ ")"
showExpr (plus e₁ e₂) = "(" ⊍ (showExpr e₁) ⊍ "+" ⊍ (showExpr e₂) ⊍ ")"
showExpr (times e₁ e₂) = "(" ⊍ (showExpr e₁) ⊍ "*" ⊍ (showExpr e₂) ⊍ ")"
showListExpr : List Expr → String
showListExpr l = String.concat (List.map showExpr l)
mutual
term = factor
∣ ♯ term >>= λ e₁ →
tok '+' >>= λ _ →
factor >>= λ e₂ →
return (plus e₁ e₂)
factor = atom
∣ ♯ factor >>= λ e₁ →
tok '*' >>= λ _ →
atom >>= λ e₂ →
return (times e₁ e₂)
atom = (number >>= return ∘ num)
∣ tok '(' >>= λ _ →
♯ term >>= λ e →
tok ')' >>= λ _ →
return e
{-# NON_TERMINATING #-}
parse′ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
parse′ {R} p₀ = parse″ p₀
where
parse″ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
parse″ {xs = xs} p [] = Colist.fromList xs
parse″ {R = R}{xs = xs} p (t ∷ s) with t ≐ '\n'
... | false = parse″ (∂ p t) (♭ s)
... | true = (Colist.fromList xs) ++ (parse″ p₀ (♭ s))
main = run $ ♯ getContents >>=IO
λ s → ♯ mapM′ (putStrLn ∘ showExpr) (parse′ term s)
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180913/c6f3a560/attachment.sig>
More information about the Agda
mailing list