the parser relies on some “monadic” programming idioms
basically, parser combinator (But 非常麻烦 in Coq)
Lex
Inductive chartype := white | alpha | digit | other.
Definition classifyChar (c : ascii) : chartype :=
if isWhite c then white
else if isAlpha c then alpha
else if isDigit c then digit
else other.
Definition token := string.
Syntax
带 error msg 的 option:
Inductive optionE (X:Type) : Type :=
| SomeE (x : X)
| NoneE (s : string). (** w/ error msg **)
Arguments SomeE {X}.
Arguments NoneE {X}.
Monadic:
Notation "' p <- e1 ;; e2"
:= (match e1 with
| SomeE p ⇒ e2
| NoneE err ⇒ NoneE err
end)
(right associativity, p pattern, at level 60, e1 at next level).
Notation "'TRY' ' p <- e1 ;; e2 'OR' e3"
:= (match e1 with
| SomeE p ⇒ e2
| NoneE _ ⇒ e3
end)
(right associativity, p pattern,
at level 60, e1 at next level, e2 at next level).
Definition parser (T : Type) :=
list token → optionE (T * list token).
newtype Parser a = Parser (String -> [(a,String)])
instance Monad Parser where
-- (>>=) :: Parser a -> (a -> Parser b) -> Parser b
p >>= f = P (\inp -> case parse p inp of
[] -> []
[(v,out)] -> parse (f v) out)
combinator many
Coq vs. Haskell
- explicit recursion depth, .e. step-indexed
- explicit exception
optionE(in Haskell, it’s hidden behind theParserMonad as[]) - explicit string state
xs(in Haskell, it’s hidden behind theParserMonad asString -> String) - explicit
accepted token (in Haskell, it’s hidden behind theParserMonad asa, argument)
Fixpoint many_helper {T} (p : parser T) acc steps xs :=
match steps, p xs with
| 0, _ ⇒
NoneE "Too many recursive calls"
| _, NoneE _ ⇒
SomeE ((rev acc), xs)
| S steps', SomeE (t, xs') ⇒
many_helper p (t :: acc) steps' xs'
end.
Fixpoint many {T} (p : parser T) (steps : nat) : parser (list T) :=
many_helper p [] steps.
manyL :: Parser a -> Parser [a]
manyL p = many1L p <++ return [] -- left biased OR
many1L :: Parser a -> Parser [a]
many1L p = (:) <$> p <*> manyL p
-- or
many1L p = do x <- p
xs <- manyL p
return (x : xs)
ident
Definition parseIdentifier (xs : list token) : optionE (string * list token) :=
match xs with
| [] ⇒ NoneE "Expected identifier"
| x::xs' ⇒ if forallb isLowerAlpha (list_of_string x)
then SomeE (x, xs')
else NoneE ("Illegal identifier:'" ++ x ++ "'")
end.
ident :: Parser String
ident = do x <- lower
xs <- many alphanum
return (x:xs)
What readers say
先看读者反馈，再直接在当前页面继续讨论。公共留言需要 Waline 服务端；配置后访客只填昵称即可发布。
这类长文如果结构清楚，我会一路读到底。这里最好的地方是把概念、公式和代码示例放在同一篇里。
数据库和工程文档的风格很实用，截图、SQL 和说明都能直接拿去复盘项目。
强化学习相关文章密度很高，但排版如果更清楚，回看体验会更好。这个新版方向是对的。
我更喜欢能快速扫到标签、修改时间和文章重点的首页，现在这种卡片视图会比纯列表更容易选读。
代码块只要语言标识和层级做好，技术博客的专业感会立刻上来。
评论区不用社交账号强绑定会更愿意留言，尤其是这种偏学习记录的网站。
Quick Identity
Pick a preset and leave a note
留言方式：先选择一个预设身份，再在下方输入评论。当前若显示“需要配置 Waline”，说明站点还缺少可写评论后端。
当前未选择预设身份