这两个太丟人了,外行都不如。我个 hobbist 都知道 IOKit。
就我个人的读yin技巧,yin的意思全在开头那个链接到模仿lisp machine设计的思路的文章里,剩下的基本可以当屁话。
我看的时候就想“这不是lisp machine吗”www
好吧好吧,已经听不懂了,占楼留个mark,提醒自己可以不用往下翻了,你不懂
层主那个例子感觉看不出什么东西,因为这个main函数本质是纯的。。。
如果能有修改全局变量的非纯函数就好了。
我说了全局变量是简单粗暴直接禁止的
问题是:如果有一段程序(使用C语言)里使用了全局变量怎么办?
使用clightgen转换那段程序,会产生什么?
是否会变成一个输入一个状态返回一个状态的函数?
对嵌套结构里的成员进行更新,会产生像lens那样代码吗?
对同一个变量连续赋值呢?(自动变成函数compose做组合transform?)
我理解的 CompCert 是允许副作用的。关于全局变量可以看 VST 里面用到的例子 global.c 和对应的用 clightgen 得到的 global.v。我觉得文档里这张图说的只是把副作用从表达式中抽取出来,而不是说消除副作用。
华为做了一件”牛逼”的产品,有的人专注于把它变得更牛逼,有的人执着于”你怎么证明它就是牛逼”?
我很好奇,安卓刚出来的时候都做了啥验证吗?
就只能手改成函数传参。编译器没有这么聪明,不支持的特性全部要手改。
lens 是因为 Haskell 沒有 linear type 才搞的,能 destructive update 的用不着 lens。
这没有全局变量,只有常量。也就是说,全局“变量”要保证不能被修改才能转化。
确实这里都是常量,没仔细看。不过我试了一下用 clightgen 编译下面这段代码,看起来还是能改全局变量的:
int g = 1;
int h(void) {
g += 1;
return g;
}
int main(void) {
int y;
y = h();
return y;
}
生成的 Coq 中的主要部分是:
Definition v_g := {|
gvar_info := tint;
gvar_init := (Init_int32 (Int.repr 1) :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition f_h := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_t'2, tint) :: (_t'1, tint) :: nil);
fn_body :=
(Ssequence
(Ssequence
(Sset _t'2 (Evar _g tint))
(Sassign (Evar _g tint)
(Ebinop Oadd (Etempvar _t'2 tint) (Econst_int (Int.repr 1) tint) tint)))
(Ssequence
(Sset _t'1 (Evar _g tint))
(Sreturn (Some (Etempvar _t'1 tint)))))
|}.
Definition f_main := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_y, tint) :: (_t'1, tint) :: nil);
fn_body :=
(Ssequence
(Ssequence
(Ssequence
(Scall (Some _t'1) (Evar _h (Tfunction Tnil tint cc_default)) nil)
(Sset _y (Etempvar _t'1 tint)))
(Sreturn (Some (Etempvar _y tint))))
(Sreturn (Some (Econst_int (Int.repr 0) tint))))
|}.
只是把副作用从表达式中抽取出来,而不是说消除副作用。
我一开始是想说这个意思。不过确实看图瞎猜不太好
我给的这个例子确实没有全局变量,我这个只是展示了表达式中的side-effect.
开源了,会像当年 linux 一样吸引大量的开发者吗?
小声点,说好的11月开源呢 留点面子给牢厂。
现在好像说明年什么时候开源
挖个坟 就技术来说,鸿蒙OS到底是个什么层面的东西,现在有答案了,楼上的各位都想多了