就技术来说,鸿蒙OS到底是个什么层面的东西?


#83

说点能看懂的,给我们小白参与个机会


#84

这两个太丟人了,外行都不如。我个 hobbist 都知道 IOKit。


#85

就我个人的读yin技巧,yin的意思全在开头那个链接到模仿lisp machine设计的思路的文章里,剩下的基本可以当屁话。 :joy:


#87

:joy::joy:


#88

我看的时候就想“这不是lisp machine吗”www


#89

好吧好吧,已经听不懂了,占楼留个mark,提醒自己可以不用往下翻了,你不懂 image


#90

层主那个例子感觉看不出什么东西,因为这个main函数本质是纯的。。。

如果能有修改全局变量的非纯函数就好了。


#91

我说了全局变量是简单粗暴直接禁止的


#92

问题是:如果有一段程序(使用C语言)里使用了全局变量怎么办?

使用clightgen转换那段程序,会产生什么?

是否会变成一个输入一个状态返回一个状态的函数?

对嵌套结构里的成员进行更新,会产生像lens那样代码吗?

对同一个变量连续赋值呢?(自动变成函数compose做组合transform?)


#93

我理解的 CompCert 是允许副作用的。关于全局变量可以看 VST 里面用到的例子 global.c 和对应的用 clightgen 得到的 global.v。我觉得文档里这张图说的只是把副作用从表达式中抽取出来,而不是说消除副作用。


#94

华为做了一件”牛逼”的产品,有的人专注于把它变得更牛逼,有的人执着于”你怎么证明它就是牛逼”?

我很好奇,安卓刚出来的时候都做了啥验证吗?


#95

就只能手改成函数传参。编译器没有这么聪明,不支持的特性全部要手改。

lens 是因为 Haskell 沒有 linear type 才搞的,能 destructive update 的用不着 lens。


#96

这没有全局变量,只有常量。也就是说,全局“变量”要保证不能被修改才能转化。


#97

确实这里都是常量,没仔细看。不过我试了一下用 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))))
|}.

#98

我們还是別在这里瞎猜了,直接看 formal semantics 比啥都快。


#99

只是把副作用从表达式中抽取出来,而不是说消除副作用。

我一开始是想说这个意思。不过确实看图瞎猜不太好 :see_no_evil:


#100

我给的这个例子确实没有全局变量,我这个只是展示了表达式中的side-effect.