A categorical programming language
| 修订版 | 703331d6e4d103091a82d1698b41e09868565978 (tree) |
|---|---|
| 时间 | 2021-08-17 04:09:26 |
| 作者 | Corbin <cds@corb...> |
| Commiter | Corbin |
Try to unroll primitive recursion.
The egg library does make this very neat. We explain that it is possible
to speculatively unroll primitive recursion for the successor case, but
don't have to worry about whether it will be worthwhile to do so.
compile.sh (diff)
hive/nat/lte.cammy (diff) hive/nat/pot.cammy (diff) jelly/src/main.rs (diff) shell.nix (diff)| @@ -29,3 +29,4 @@ csc -O3 -o "$name" "$tmpdir/$name.scm" | ||
| 29 | 29 | |
| 30 | 30 | # Clean up temporary files. |
| 31 | 31 | rm -r "$tmpdir" |
| 32 | +rm a.out |
| @@ -0,0 +1 @@ | ||
| 1 | +(curry (comp (uncurry nat/monus) nat/is_zero)) |
| @@ -0,0 +1 @@ | ||
| 1 | +(comp (pair id (comp (comp (comp ignore zero) succ) succ)) (uncurry nat/exp)) |
| @@ -16,10 +16,15 @@ fn load_tree(handle :&mut Read) -> std::io::Result<RecExpr<SymbolLang>> { | ||
| 16 | 16 | // "free for X" means that the polymorphic type of X implies the underlying equality justifying |
| 17 | 17 | // the annotated rule, as in Wadler 1989. |
| 18 | 18 | |
| 19 | +// Rules marked "associative!" can cause explosions. | |
| 20 | + | |
| 19 | 21 | fn main() -> std::io::Result<()> { |
| 20 | 22 | let rules :&[Rewrite<SymbolLang, ()>] = &[ |
| 21 | 23 | rw!("comp-id-left"; "(comp id ?x)" => "?x"), |
| 22 | 24 | rw!("comp-id-right"; "(comp ?x id)" => "?x"), |
| 25 | + | |
| 26 | + // associative! | |
| 27 | + rw!("comp-assoc-left"; "(comp ?x (comp ?y ?z))" => "(comp (comp ?x ?y) ?z)"), | |
| 23 | 28 | rw!("comp-assoc-right"; "(comp (comp ?x ?y) ?z)" => "(comp ?x (comp ?y ?z))"), |
| 24 | 29 | |
| 25 | 30 | rw!("ignore-absorb-left"; "(comp ?x ignore)" => "ignore"), |
| @@ -62,6 +67,8 @@ fn main() -> std::io::Result<()> { | ||
| 62 | 67 | rw!("name-desugar"; "(name ?f)" => "(curry (comp snd ?f))"), |
| 63 | 68 | |
| 64 | 69 | rw!("nat-elim-pr"; "(pr zero succ)" => "id"), |
| 70 | + rw!("nat-unroll-pr-zero"; "(comp zero (pr ?x ?f))" => "?x"), | |
| 71 | + rw!("nat-unroll-pr-succ"; "(comp succ (pr ?x ?f))" => "(comp (pr ?x ?f) ?f)"), | |
| 65 | 72 | |
| 66 | 73 | rw!("list-elim-fold"; "(fold nil cons)" => "id"), |
| 67 | 74 |
| @@ -12,6 +12,8 @@ in pkgs.stdenv.mkDerivation { | ||
| 12 | 12 | ocamlformat |
| 13 | 13 | # debugging stub.ml |
| 14 | 14 | ocamlPackages.utop |
| 15 | + # working with sexps | |
| 16 | + ocamlPackages.sexp | |
| 15 | 17 | # running compile.sh |
| 16 | 18 | ocaml |
| 17 | 19 | # publishing |
Fork