Coq2RustCoq to Rust程序提取
Coq提取为Rust程序,采用OCaml实现。代码数基于原生Co代码。
从input.v
文件,可查看提取Coq条件示例。
尝试:
$ ./configure -local $ ./compile.sh
提取示例代码:
enum Empty_set<> { } enum Unit<> { Tt } enum Bool<> { True, False } fn xorb(b1: Bool, b2: Bool) -> Bool { match b1 { Bool::True => (match b2 { Bool::True => Bool::False, Bool::False => Bool::True }), Bool::False => b2 } } enum Nat<> { O, S(Box<Nat>) } enum Prod< a, b> { Pair(Box<a>, Box<b>) } fn fst<p,a2>(p: Prod<p,a2>) -> p { match p { Prod::Pair(box x,box y) => x } } enum List< a> { Nil, Cons(Box<a>, Box<(List<a>)>) } fn app<m0>(l: List<m0>, m0: List<m0>) -> List<m0> { match l { List::Nil => m0, List::Cons(box a,box l1) => List::Cons((box () a), (box () (app (l1,m0)))) } } fn add(n0: Nat, m0: Nat) -> Nat { match n0 { Nat::O => m0, Nat::S(box p) => Nat::S((box () (add (p,m0)))) } } fn n() -> Unit { Unit::Tt } fn m() -> Bool { Bool::True } enum Emp<> { } type Single = Unit; // singleton inductive, whose constructor was s fn o() -> Single { Unit::Tt } enum Double<> { D0(Box<Unit>), D1 } fn d() -> Double { Double::D0((box () Unit::Tt)) } fn e() -> Double { Double::D1 } enum Two_arg<> { Ta(Box<Unit>, Box<Unit>) } fn tv() -> Two_arg { Two_arg::Ta((box () Unit::Tt), (box () Unit::Tt)) } fn num() -> Nat { Nat::S((box () (Nat::S((box () Nat::O))))) } fn f(d0: Double) -> Unit { Unit::Tt } fn g(d0: Double) -> Double { match d0 { Double::D0(box u) => Double::D1, Double::D1 => Double::D0((box () Unit::Tt)) } } enum Even<> { O0, Eo(Box<Odd>) } enum Odd<> { Oe(Box<Even>) }
评论
Coq2RustCoq to Rust程序提取
Coq提取为Rust程序,采用OCaml实现。代码数基于原生Co代码。从input.v文件,可查看提取Coq条件示例。尝试:$ ./configure -local$ ./compile.sh提取示例
Coq2RustCoq to Rust程序提取
0
Mustang完全用 Rust 构建程序
Mustang是一个用于构建完全用Rust构建的程序的系统,这意味着它们不依赖于libc或crt1.o的任何部分,并且不链接任何C代码。作者表示,Mustang最初只是为了好玩而创建,练习一些为其他目
Mustang完全用 Rust 构建程序
0
Newspaper基于 Python 的文章提取程序
Newspaper可以用来提取新闻、文章和内容分析。使用多线程,支持10多种语言等。作者从requests库的简洁与强大得到灵感,使用python开发的可用于提取文章内容的程序。支持10多种语言并且所
Newspaper基于 Python 的文章提取程序
0