wky / pi-calculus Goto Github PK

type_subst is not complete.
type of the free variable system in

new x in (x!0.O| system!(1+2+3+4).O |
new y in
*(x?n.y!n+1.O|
y?n.x!n+1.O))

should be Chan(Int), but simpletype.ml gives Chan(TVar5).

我已经把simple type写好了， 现在需要 @Mestway 把 simple type 的形式化定义写出来，以及选择一个合适的更强的类型系统，并给出形式化定义，我根据这个定义继续开发

词法、语法分析已经写好，现在能够生成最基本的语法树。大家测试一下 @featheryleaf @Mestway

@Mestway 形式化证明，研究subtype
@wky 词法语法分析， 信道传输数据的类型匹配 + 传输方向

@featheryleaf 自己过来领任务

重点：提取usage(cap + ob), 列出限制，求解

待确认：

1. usage subtype relation -- 是否syntax directed
2. usage reduction -- 顺序，可能需要回溯，是否逐步求解

扩展
基本类型（int，bool，chan*）
基本表达式 if then else， + - x, < <= > >=
解释执行

Is it possible to get a brief description of your code and what it does?