Skip to content

Instantly share code, notes, and snippets.

@bond15
Created November 17, 2022 23:30
Show Gist options
  • Save bond15/4403782507132764be5c469b1a5d6ae4 to your computer and use it in GitHub Desktop.
Save bond15/4403782507132764be5c469b1a5d6ae4 to your computer and use it in GitHub Desktop.
Pattern Error
import List
import Maybe
data Parser (a : Type) = Parser (String → List (a , String))
parse : ∀ {a : Type}. Parser a → String → List (a , String)
parse (Parser p) = p
result : ∀{a : Type}. a → Parser a
result a = Parser (λs → Next (a,s) Empty)
concat : ∀{a : Type}. List (List a) → List a
concat Empty = Empty;
concat (Next xs xss) = append_list xs (concat xss)
bind : ∀{a b : Type}. Parser a → (a → Parser b)[] → Parser b
bind (Parser p) [f] = Parser (λ s → concat(lmap [λ(a,s') → parse (f a) s'] (p s)))
zero : ∀{a : Type}. Parser a
zero = Parser (λ s → let () = drop @String s in Empty)
item : Parser Char
item = Parser (λ s → case stringUncons s of
None → Empty;
Some (c,cs) → Next (c,cs) Empty)
sat : (Char → Bool)[] → Parser Char
sat [p] = item `bind` [λ c → let
[c'] : Char[] = moveChar c
in if (p c')
then (result c')
else zero]
lookup : List Char → Char → Bool
lookup Empty c = let () = drop @Char c in False;
lookup (Next c' cs) c = let
[c] : Char[] = moveChar c
in (c ≡ c') `or'` (lookup cs c)
--main : Parser Char
--main = sat [lookup (Next 'h' Empty)]
main : List (Char, String)
main = parse (sat [lookup (Next 'h' Empty)]) "h"
@bond15
Copy link
Author

bond15 commented Nov 17, 2022

src/Language/Granule/Interpreter/Eval.hs:653:44-122: Non-exhaustive patterns in lambda

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment