这两天我想实现最近设计的逆向计算表达式生成（就是把 +* 变 /- 的这种逆序+反向，只是未知只能有一个，具体要实现一个 findPaths { it !in globals } 细节不多说）

顺便也进一步理解了 ParserKt 最常用的结构们：
Stmts (Stmt ';'|newline) -- elementIn
Stmt ('L' Expr '=' Expr) | Expr -- OpChain.disambiguate, Seq(a,b,c)
Expr opChain(Atom, "+- *\")
Atom Int|Name|Paren where
letter [a-zA-Z_]
digit [0-9]
Int {digit} -- Repeat, toDefault
Name letter {letter|digit}?
Paren '('Expr')' -- Decide, Deferred

总结就是 Seq,Decide,Repeat,item,elementIn; Deferred,toDefault,calm 以及这次要测试的 OpChain(包含 .OpTree 和 .LazyStack 的版本, 这次的 DSL 你不给 infixl/r 提供 join 那就默认是 OpTree 了哈, 真给力)
以前 Seq 不是基于 Pair/Triple 的时候肯定还有 Pattern.convert, 哈哈

悟出了一个道理，就是如果对问题的理解不对，技术越高结果乱得越吓人。

在 funcly-ParserKt 的可用化过程中，我了解了如何处理 !(obj.prop[0])+1这种常见的算符链实际上需要左递归(chainl 也行) 不然 !xs[0] 的优先级会错、明白了 Java 的 field/method 成员、 Python 式 name: type = init 如何用 concat(p1, p2) 和 OpChain.disambiguate(Name) { if (peek == ":") /**/} 表达式前缀关键字的消歧义（其实不需要真正的 lookahead 来解决）

加强了 Piped 组合器(包含 showBy,run,greedy,leftRec 等便利组合)，解决了 ParserKt 通往实际可用于 C/Java/JS/Kotlin 解析乃至文本链接/日期/关键词读取的“最后一公里”（迫真）

不过在我解决 LexerFeed 的时候出现了个问题：
首先说明，这个 LexerFeed 是利用 ParserKt 最具特点的 peek/consume() Feed 流预先跳空格的过滤流，利用嵌套流是最近才想到的点子（之前一定要像普通 PEG(parser exp. grammar) 一样非得在 Pattern 里侵入式读取/略过空格 违和感太强，是我傻逼了） （老实说这次重新设计我感觉自己以前的就是傻逼设计，竟然不把 BidirMap 提出来…… 害的存在 PairedTriePattern 这种莫名其妙的东西，简直和因为没有 peekMany 而造成的 StickyEnd 问题一样草）

如果是 C 式辣鸡文法，用单层状态机也就可以了，可咱的 Kotlin 当属语言小王子，我的 LexerFeed 是为下一层的文法定义自动过滤掉所有空格（当然也可以选择保留缩进或者剔除换行，只要不影响语义），这样 "1 + 2" 过一遍就只见 "1+2" 了。

至于 /* */ 式必须再 peek(1) 的注释就需要有请子类 SkipWhiteFeed 处理了，它实现 FeedControl.peekMany （话说我最近的设计对 instanceof interface 用得真多…… 太过分了），当然注释也是可以保留的， SkipWhite 类会有一个 beforeWhites: MutableMap? 保存 AST 对应的前部空白，具体做法是用 pat.alsoDo 。

但 Kotlin 首先支持 "${"a"}b" 这种嵌套模板字符串（现在很多语言如 C#, Groovy 都支持），其次是它的中缀链有不能跳过空格的部分（ a+b*c 你能跳， a to b in args is Boolean 你敢跳么？跳了就变单个标识符了）

对这两个问题， Kotlin 官方“利”用 ANTLR4 的丑陋回答是 KotlinLexer.g4 几乎包含了所有 Kotlin 的文法结构，远远超过词法定义该有的范围，要不然没法处理空格啊呵呵呵→_→

幸运的是 ParserKt 才没有这些破事，作为一个拥有组合解析器优越性和强大生命力的框架，它不必分出什么 tokenizer 和 parser 所以自然不会把 fun :List<T>=1 这种搞混（即便现在我部分隔离出了一个 LexerFeed 流过滤器来跳过空格）

对于第二个问题的前置部分，要么然利用原有 Function 值的解析器来读取需要保留的 字符串/关键词("fun ", "class " 里的空格，但这不科学（ funcly-ParserKt 是基于函数式内联提升性能的，不可能窥见 Seq,Decide 到底得到了。啥参数）

确实可以让部分组合读成字符串或计数的形式，但这样 LexerFeed 必然在下层请求 consume() 的时候从一个队列里拿结果，而且这等于字符串什么的都读了两遍（只能是字符流， "\"s" 这种转义还是要处理），这与 ParserKt 所推崇的 single-pass 解析是背道而驰的（本来递归下降法都会在调用栈上分配相当多的空间了，何必预读甚至多遍处理）

当然也可以选择加个 QueueFeed, 然后在另一线程同步运行 "keep" Pattern, 只要发现在运行就不跳空格，但为保证 wait condition 会调度上，每 accept(peek) 一次都得 Thread.sleep(0) 保证同步，看起来是只过一遍，实际上比过10遍还费资源（而且不支持KJS）。

于是，只能从主动读取的自顶向下解析换成被动状态转移的自底向上…… 只要 state != 0 就不跳空格

我设了几个基于 Array<Int> 的猜想，最后创建了一个基于 MutableList<LexerStateMover.T/*(chars,next,fail)*/> 的编号状态机及其构造 DSL
比如 "\"s" 的字符串可以表达为

val mover = LexerStateMover(s_zero=0)
mover.build { seq("\"") then br("\\" to seq(any), "\"" to seq("\""), any to keep) ) }

这样鬼畜的状态转移式而不定义式（其实也比较巧妙，我给它制订了 charTest 和 action 这些基础功能）

好先说第二个问题，我发觉 Lexer 流根本不可能比 parser 先知道是 "1 +2" 还是 "1 to(2)"，它连合并空格都做不到（毕竟视口只有1）

于是看起来唯有通过 peekMoreWhile {it.isBlank()} 这种黑魔法来做了，它看起来有点像 chunked():

fun <T> Iterable<T>.chunked(chunk_size:Int, op: (T)->Unit) {
  var n = chunk_size
  var list = take(n)
  while (true) {
    for (i in 0..n) op(list[i])
    n += chunk_size
    list = take(n)
  }
}

大概就是不断以 0..i<n 的 list 子集调用 op 且以 chunk_size 为批量来预取，比单层循环每次看 size 够不够再扩充或许快一些。
我应该是魔怔了，竟然觉得这个好像很有意思一样。

后来我发现了个绝妙的解决方案：让解析部分和流部分合作，不必复制粘贴解析器来写分词器。
解析器只负责处理表达式部分的空格，与 Lexer 交换解析状态和跳空格方法
这也意味着状态栈——ParserKt 部分是递归的，所以不止嵌套表达式能读取，字符串内联的递归问题也解决了（如果要跳过可嵌套注释，也能解决）
本来用 action 也能手动实现状态栈，现在给标准化了，嘿嘿(º﹃º )

总之，遇到总觉得不优雅之处还得多想想，或许会有更好的解决方法呢？

kotlin 怎么传 Function<T, R> 的参

1.4给了 fun interface的SAM

说起来我看 ice1k 的 agda 群组常年没人讨论，还打算加两条OT一样的
https://t.me/ice_learn_agda_chat/267

后来发现我这好心根本就是鬼扯，其实人家根本不缺废话；何况我不处理 Haskell/Scala 系语言和其它编程范式的

感情很复杂，这个语言 ice1k 也不是没讲过，只是他把老的入门性 agda 博客都删了，何况这些问题即便讲不好也没啥可怪的，它本身就复杂。

譬如递归 reverse 链表：

rev (x::xs) = [x] ++ (rev xs)
rev [] = []

要把这个思路切换成怎么归纳证明 rev (rev xs) = xs 从而 forall x xs. x:xs = (rev xs)++[x]
或 =(rev xs)++r x 是很困难的

（怎么今天看了就好像只是构造数据结构再相等性一样平常，之前可是很不解的……）

好吧，那我就不用 Agda 先讲讲
归纳证明是对序列的俩成立：对首项『基线』成立，对每项都基于前命题成立（命题证明不是布尔，没有失败一说）

比如咱有 listOf(1, 2, 3).fold(0) { a, b -> a+b } 需证明结果不小0:
基线 [] 恒成立
递归 (p, x) x不小0

当然加数都不小0 只是一种子集情况。
我们能以 xs.fold(true) { p,x -> x>=0 } 测试输入成立性，如果你觉得这玩意是类型，那说的就是“那个”编程了。（看不惯我混乱理论可以自己科普）

我们知道类型系统就是可以“否决”某段程序的东西，所以它实际上是在定义某种关系性的约束（比如 paramType in type.impls 这种 trait(interface) 实现约束）

如果这个可以在约束上定义些计算，或者说类型检查期也能做递归匹配的话，就是 dependent type 了（刚才的例子结果 >= 0 的实际情况只能算全再判，更像编译期计算了）。


好了看看 rev (rev xs) == xs 怎么证明，肯定一头雾水，但想想如果你构造的不是『类型』而是判定器会怎么做？肯定是算完再试等……😂 不要那样。

等式的右侧是数据，左侧是两层调用；如果下手得从左顶层的 rev, 而要证明就必须得出 (rev xs) 与 xs 本身的关系再作归纳，好像你能“解构”这个调用一样，你会怎么解构？肯定是 xs++[x] == x::(rev xs) ，当然等号反过来也一样（自反性 identity/reflexive 的交换律）

想到 xs++[x] （把 xs 全串到 x::[] 上）你一定记得 xs 在这里意味着递归栈了，因为 (xs++ys) 隐含着二者长之和+1([], nil) 的递归栈

(xs ++ ys) = cat xs ys where
cat zs (x:xs) ys = cat (x:zs) xs ys
cat zs [] (y:ys) = cat (y:zs) [] ys
cat zs [] [] = zs

这里我们用了第三个链表，是因为必须从 xs 的尾部，逆序 ::(cons) 到 ys ，其实不嫌麻烦也可以 foldRight(用栈逆序) :

(xs++(y:ys)) = xs++[y] ++ ys
(xs++[]) = xs

嘛，这个非常不动态编程(DP)弱缓存，例一用 tuple 保留zs也可实现，不得不说 Haskell 的模式匹配函数的确直观反映了各种流算法。

跑题了，假设你得出 forall x xs. x::xs == (rev xs) ++[x] 呃不是 x::(rev xs) == xs++[x]

（好吧二者是不一样的，记得主语始终在 ++[x] 的部分）
（注意要解构等式两边，都必须用到递归栈，第一个实际上是正向 rev 的定义😞）
可以通过以下方法证明 rev (rev xs) == xs ：

-- x::(rev xs) == xs ++[x]
xEqTail : (a, [a]) -> [a] -> Bool

idp = (==) -- eq path
revId (x::xs) = -- xs++[x]
xEqTail (x, ) && (revId xs)
revId [] = (idp [] [])

等等， x:(rev xs) == xs++[x] 这个等式不对，我没注意到 (rev xs) 和 xs 本身的区别…… 其实是 x:(rev xs) == (rev xs)++[x] ，意味着 x:xs == rxs++[x] ……
算了写不出来😢不多说了，入门科普而已。
顺便：代码部分可以理解为交换 ::(has type) 和 :(cons) 语义的 Haskell, 反正我不是说正经的。

上面证明 rev (rev xs) = xs 里我解构施用层 (rev xs) 到 x:(rev xs) = xs++[x] ，其实是 rev (x:xs) = (rev xs) ++[x] 的反向变形。

我显然把右边的 xs 理解成其参数了（虽然对正常程序猿 等式左边才能有未知量是直觉😂），没注意到关系解构的部分必须以 (rev xs) 描述，例 rev $ [1,2,3] 可不等于它++[1] 呢…… 但是 [2,3] ++[1] 就对了

这个点子是我在提示下独立想出来的，但思想和实践总是隔着基础模型的桥梁，虽然能设计、找到特色点也远不等于能细分并逐步实现，知道理论不等于善于实行。
不过，我仍希望这对大家有帮助，哪怕是理解别人的误区和失败。

只要可能对人有帮助，我才不怕出丑丢脸；毕竟相比技术和创造，自尊太微不足道了。

把 rev (rev xs) = xs 里的 (rev xs) 与 xs 互换即可得到 rev xs = rev xs 全等，可这不是“移项变号”或“两边同时减”那么简单（虽然也可理解为“把rev移到另一侧”呢），但不管怎么样显然是重组 a:rev$v=rev$a:v 这种关于 rev 结果的关系

以我目前这层面的水平当然仍是无法做到定理证明啦，虽然它也有意思。 #cs #plt

话说部分读者你们也被不明觉厉加入那个讨论组唉，还是劝退好了

人家千里冰封说的明明白白，必须有 dependent type 基础，并且他是不负责给你打基础的，狠心点：

菜鸟别以为和大牛在一起、或者看大佬做事就能给自己涨知识，没用的。

接近那个领域，也别以为自己看它的文档、用它的术语你就属于它。
系统的知识网络和直觉不是靠生硬的文字和无聊的名词能表达的，名词和定义规则背后隐含的是前人真切的思考，你不学他所学怎么能真懂他。

有些人就是天才，你和他差的就是人家能独立得出而你无法get到的一句话、一个小思路，有时候是因为知识和经验，有时候 1% 的灵感就是靠努力无法填补的。

不要以为自己足够热血或者“非常想”就能成功，科学说了算。

也不要自作主张认为“我需要那些东西来帮助进步”，不你不需要😡。阻塞在一个目标上不懂变通、提升知识广度，那叫环形等待、死锁。

说错了话他们不耐烦你也不开心，本就不是一路人，派系不同何必凑数。

#China #web 🤔

【品葱】
看到这个，我只想说：意料之中。

整天内斗吵架，不维护社区氛围、不鼓励创作，那么就只能慢慢的死亡了。因为品葱本身的竞争力不大，很容易就能找到替代品。真正让用户持续在品葱发表内容，都是靠用户维护出来的氛围。肆意将用户污蔑成网军，对原创内容的不重视，极大的破坏了这一氛围。品葱自然就丧失自己的独特性了。

更不用说趾高气昂的管理员。这点相信如果大家有和某些管理员接触过就知道我在说什么。

不重视内容，不重视用户体验的恶果已然显现出来。品葱站长无论是公开还是私下都多次表示品葱的目标是要“活下去”，而不是“做大”。但是品葱目前面临的问题是自身在失去“生命力”。错将维护讨论氛围、改善用户体验视为“扩张”。对于提出问题的用户刻薄与打压（甚至污蔑对方为网军），对于不满管理员决策的用户嘲弄与侮辱。品葱与半年前提出的《习惯法》沦为废纸。所谓“用户自治”彻底失败。可以说，品葱作为公共讨论空间，已完全失去“讨论”。目前品葱的定位更多的是内容农场而不是“问答式社区”

品葱的例子令人惋惜。曾经的旧品葱无论是氛围还是内容都无法挑剔，可惜在中共的威逼利诱下被迫关闭；新品葱在最初的时候虽然小众，但是质量、氛围、人气随着反送中运动的爆发而爆发，往后无论是反送中，新冠肺炎，都有着非常大量且用心的内容发表。可如今再去看品葱，关于国安法的讨论寥寥数个，首页大半部分被搬运新闻和旧贴占据。质量也不尽人意。看了看品葱曾经的archive，看到曾经品葱上的人们乐观而且满怀希望得为自己心中的信念与他人据理力争，再看看如今少有答案/评论超过一百个字。曾经置顶各种活动贴，多方联动。如今躲在角落里自己一个人玩泥巴

不禁感叹一句“时过境迁啊。

品葱已死，我们还要继续走下去。希望大家永远都要记得品葱，记得它曾经大放异彩，更要记得它是怎么落寞的。

各位晚安。

#gui #android

请教一个相机相关的问题。打开相机以及设置预览回调都在同一个子线程内。但是在onPreviewFrame回调方法中打印当前线程却是 main。 何故？

Callbacks from other methods are delivered to the event loop of the thread which called open(). If this thread has no event loop, then callbacks are delivered to the main application event loop. If there is no main application event loop, callbacks are not delivered.