• R/O
  • HTTP
  • SSH

No Tags

Frequently used words (click to add to your profile)

javac++androidlinuxc#objective-cqt誰得windowscocoapythonphprubygameguibathyscaphec翻訳omegat計画中(planning stage)frameworktwittertestdomvb.netdirectxbtronarduinopreviewerゲームエンジン

A categorical programming language

File Info

Rev. caae86fc44c3d23102b8225e63fc6266edaf3fbd
Size 11,454 bytes
Time 2022-09-19 02:41:02
Author Corbin
Log Message

Honey can evaluate nat/256 in the browser!


use std::io::{Read, Write};

use log::info;

use egg::{*, rewrite as rw};

fn load_tree(handle :&mut Read) -> std::io::Result<RecExpr<SymbolLang>> {
    let mut input = String::new();
    handle.read_to_string(&mut input)?;
    input.parse().map_err(|e| std::io::Error::new(std::io::ErrorKind::InvalidData, e))

struct CAMCostModel;
impl CostFunction<SymbolLang> for CAMCostModel {
    type Cost = u64;
    fn cost<C>(&mut self, enode :&SymbolLang, mut costs :C) -> Self::Cost
    where C :FnMut(Id) -> Self::Cost {
        match enode.op.as_str() {
            // Compiles away entirely
            "id" => 1,
            "comp" => costs(enode.children[0]) + costs(enode.children[1]),
            "cons" => 1,
            // Constant terms
            "ignore" => 2,
            "zero" => 2,
            "nil" => 2,
            "t" => 2,
            "f" => 2,
            "f-zero" => 2,
            "f-one" => 2,
            // Term ops which the JIT can elide
            "fst" => 3,
            "snd" => 3,
            "dup" => 3,
            "left" => 3,
            "right" => 3,
            // Stack-allocating operations
            "pair" => 4 + costs(enode.children[0]) + costs(enode.children[1]),
            "case" => 4 + costs(enode.children[0]).max(costs(enode.children[1])),
            "curry" => 4 + costs(enode.children[0]),
            "uncurry" => 4 + costs(enode.children[0]),
            // Loops
            "pr" => 4 + 2 * costs(enode.children[0]) + 3 * costs(enode.children[1]),
            "fold" => 4 + 2 * costs(enode.children[0]) + 5 * costs(enode.children[1]),
            // Term ops which the JIT still has to residualize
            _ => 4

// Hagino 1987: https://web.sfc.keio.ac.jp/~hagino/index.html.en
// Cousineau, Curien, & Mauny 1987: https://doi.org/10.1016/0167-6423(87)90020-7
// Wadler 1989: https://www2.cs.sfu.ca/CourseCentral/831/burton/Notes/July14/free.pdf
// Elliott 2013: http://conal.net/blog/posts/optimizing-cccs

// "R when X is id" means that rule R is being specialized modulo the equality:
//     (comp id ?f) = ?f = (comp ?f id) = (comp (comp ?f id) id) = ...

// "free for X" means that the polymorphic type of X implies the underlying equality justifying
// the annotated rule, as in Wadler 1989.

// "dual from X" means that justification X formally dualizes to justify the annotated rule. For
// example, products and sums are dual.

// "inverse of R" means that rule R is run in reverse in order to open up further optimization
// opportunities.

// "jet for X" means that expression X in the hive should be replaced by the annotated rule.
// "implied by jet R" means that rule R introduces new critical pairs which need reduction.

// Rules marked "associative!" can cause explosions.

// Rules marked "improvement!" can improve IEEE 754 results in both precision and/or accuracy, so
// cannot be run backwards.

fn main() -> std::io::Result<()> {

    let rules :&[Rewrite<SymbolLang, ()>] = &[
        rw!("comp-id-left"; "(comp id ?x)" => "?x"),
        rw!("comp-id-right"; "(comp ?x id)" => "?x"),

        // associative!
        rw!("comp-assoc-left"; "(comp ?x (comp ?y ?z))" => "(comp (comp ?x ?y) ?z)"),
        rw!("comp-assoc-right"; "(comp (comp ?x ?y) ?z)" => "(comp ?x (comp ?y ?z))"),

        rw!("ignore-absorb-left"; "(comp ?x ignore)" => "ignore"),

        // free for fst
        rw!("fst-elim-pair"; "(comp (pair ?f ?g) fst)" => "?f"),
        // free for snd
        rw!("snd-elim-pair"; "(comp (pair ?f ?g) snd)" => "?g"),
        rw!("pair-fst-snd"; "(pair fst snd)" => "id"),
        rw!("pair-repack"; "(comp (pair ?f ?g) (pair (comp fst ?j) (comp snd ?k)))"
            => "(pair (comp ?f ?j) (comp ?g ?k))"),
        // pair-repack when ?j is id
        rw!("pair-repack-snd"; "(comp (pair ?f ?g) (pair fst (comp snd ?k)))"
            => "(pair ?f (comp ?g ?k))"),
        // pair-repack when ?k is id
        rw!("pair-repack-fst"; "(comp (pair ?f ?g) (pair (comp fst ?j) snd))"
            => "(pair (comp ?f ?j) ?g)"),
        // Elliott 2013
        rw!("pair-precompose"; "(pair (comp ?r ?f) (comp ?r ?g))" => "(comp ?r (pair ?f ?g))"),
        // inverse of pair-precompose
        rw!("pair-precompose-inv"; "(comp ?r (pair ?f ?g))" => "(pair (comp ?r ?f) (comp ?r ?g))"),
        // pair-precompose when ?f is id
        rw!("pair-factor-fst"; "(pair ?r (comp ?r ?g))" => "(comp ?r (pair id ?g))"),
        // pair-precompose when ?g is id
        rw!("pair-factor-snd"; "(pair (comp ?r ?f) ?r)" => "(comp ?r (pair ?f id))"),
        // pair-precompose when ?f and ?g are id
        rw!("pair-factor-both"; "(pair ?r ?r)" => "(comp ?r dup)"),

        // jet for pair/dup
        rw!("pair-dup-jet"; "(pair id id)" => "dup"),
        rw!("dup-pair-deopt"; "dup" => "(pair id id)"),
        rw!("dup-absorb-swap"; "(comp dup swap)" => "dup"),
        rw!("dup-elim-fst"; "(comp dup fst)" => "id"),
        rw!("dup-elim-snd"; "(comp dup snd)" => "id"),
        // jet for pair/swap
        rw!("pair-swap-jet"; "(pair snd fst)" => "swap"),
        rw!("swap-fst"; "(comp swap fst)" => "snd"),
        rw!("swap-snd"; "(comp swap snd)" => "fst"),

        rw!("pair-swap-invo"; "(comp swap swap)" => "id"),
        // Like pair-swap-invo, this turns braided products into symmetric products.
        rw!("pair-swap-pair"; "(comp (pair ?f ?g) swap)" => "(pair ?g ?f)"),

        // free for left
        rw!("left-elim-case"; "(comp left (case ?f ?g))" => "?f"),
        // free for right
        rw!("right-elim-case"; "(comp right (case ?f ?g))" => "?g"),
        rw!("case-left-right"; "(case left right)" => "id"),

        // dual of pair-swap-pair
        // By abstract nonsense, this turns braided sums into symmetric sums.
        rw!("case-swap-case"; "(comp (case right left) (case ?f ?g))" => "(case ?g ?f)"),

        // dual of Elliott 2013
        rw!("case-postcompose"; "(case (comp ?f ?r) (comp ?g ?r))" => "(comp (case ?f ?g) ?r)"),
        rw!("case-factor"; "(case ?r ?r)" => "(comp (case id id) ?r)"),

        rw!("curry-uncurry-cancel"; "(uncurry (curry ?f))" => "?f"),
        rw!("uncurry-curry-cancel"; "(curry (uncurry ?f))" => "?f"),

        // jet for app
        rw!("app-jet"; "(uncurry id)" => "app"),
        // Implied by jet app-jet
        rw!("curry-app"; "(curry app)" => "id"),
        rw!("beta-full"; "(comp (pair (comp ?x (curry ?f)) ?y) app)" => "(comp (pair ?x ?y) ?f)"),
        // Cousineau, Curien, & Mauny 1987
        // beta-full when ?x is id
        rw!("beta"; "(comp (pair (curry ?f) ?y) app)" => "(comp (pair id ?y) ?f)"),
        // Hagino 1987
        // This is a more powerful form of beta when ?x is (uncurry ...)
        rw!("beta-fuse"; "(comp (pair ?x ?y) (uncurry ?f))" => "(comp (pair (comp ?x ?f) ?y) app)"),

        rw!("curry-const"; "(comp ?f (curry (comp fst ?g)))" => "(curry (comp fst (comp ?f ?g)))"),
        // curry-const when ?g is id
        rw!("curry-const-delay"; "(comp ?f (curry fst))" => "(curry (comp fst ?f))"),
        rw!("curry-ignore"; "(comp ?f (curry (comp snd ?g)))" => "(curry (comp snd ?g))"),
        // curry-ignore when ?g is id
        rw!("curry-ignore-name"; "(comp ?f (curry snd))" => "(curry snd)"),

        rw!("nat-elim-pr"; "(pr zero succ)" => "id"),
        rw!("nat-unroll-pr-zero"; "(comp zero (pr ?x ?f))" => "?x"),
        rw!("nat-unroll-pr-succ-post"; "(comp succ (pr ?x ?f))" => "(comp (pr ?x ?f) ?f)"),
        rw!("nat-shift-pr-endo"; "(comp (pr ?x ?f) ?f)" => "(pr (comp ?x ?f) ?f)"),

        // jet for nat/add
        rw!("nat-add-jet"; "(pr (curry snd) (curry (comp app succ)))" => "(curry n-add)"),
        // jet for nat/pred-maybe
        rw!("nat-pred-maybe-jet"; "(pr right (comp (case succ zero) left))" => "n-pred-maybe"),

        rw!("list-elim-fold"; "(fold nil cons)" => "id"),
        rw!("list-unroll-fold-nil"; "(comp nil (fold ?x ?f))" => "?x"),
        rw!("list-unroll-fold-cons"; "(comp cons (fold ?x ?f))" => "(comp (pair fst (comp snd (fold ?x ?f))) ?f)"),

        // 2 = 1 + 1
        rw!("bool-t-either"; "(comp t either)" => "left"),
        rw!("bool-f-either"; "(comp f either)" => "right"),

        // Boolean negation
        rw!("bool-t-not"; "(comp t not)" => "f"),
        rw!("bool-f-not"; "(comp f not)" => "t"),
        rw!("bool-not-invo"; "(comp not not)" => "id"),

        // Boolean operations
        rw!("conj-comm"; "(comp swap conj)" => "conj"),
        rw!("disj-comm"; "(comp swap disj)" => "disj"),

        // Some Boolean gates
        rw!("bool-conj-f-fst"; "(comp (pair f ?b) conj)" => "f"),
        rw!("bool-conj-t-fst"; "(comp (pair t ?b) conj)" => "?b"),
        rw!("bool-conj-f-snd"; "(comp (pair ?b f) conj)" => "f"),
        rw!("bool-conj-t-snd"; "(comp (pair ?b t) conj)" => "?b"),
        rw!("bool-disj-f-fst"; "(comp (pair f ?b) disj)" => "?b"),
        rw!("bool-disj-t-fst"; "(comp (pair t ?b) disj)" => "t"),
        rw!("bool-disj-f-snd"; "(comp (pair ?b f) disj)" => "?b"),
        rw!("bool-disj-t-snd"; "(comp (pair ?b t) disj)" => "t"),

        // IEEE 754 addition
        rw!("f-add-comm"; "(comp swap f-add)" => "f-add"),
        rw!("f-add-unit-left"; "(comp (pair ?f f-zero) f-add)" => "?f"),
        rw!("f-add-unit-right"; "(comp (pair f-zero ?f) f-add)" => "?f"),
        rw!("f-add-negate-left"; "(comp (pair id f-negate) f-add)" => "f-zero"),
        rw!("f-add-negate-right"; "(comp (pair f-negate id) f-add)" => "f-zero"),

        // IEEE 754 multiplication
        rw!("f-mul-comm"; "(comp swap f-mul)" => "f-mul"),
        rw!("f-mul-unit-left"; "(comp (pair ?f f-one) f-mul)" => "?f"),
        rw!("f-mul-unit-right"; "(comp (pair f-one ?f) f-mul)" => "?f"),

        // improvement!
        rw!("f-negate-invo"; "(comp f-negate f-negate)" => "id"),
        rw!("f-recip-invo"; "(comp f-recip f-recip)" => "id"),

        // IEEE 754 even functions
        rw!("f-sign-negate-ana"; "(comp f-negate f-sign)" => "(comp f-sign not)"),
        rw!("f-sign-negate-kata"; "(comp f-sign not)" => "(comp f-negate f-sign)"),
        rw!("f-cos-even"; "(comp f-negate f-cos)" => "f-cos"),

        // IEEE 754 odd functions
        rw!("f-sin-odd-ana"; "(comp f-negate f-sin)" => "(comp f-sin f-negate)"),
        rw!("f-sin-odd-kata"; "(comp f-sin f-negate)" => "(comp f-negate f-sin)"),

        // IEEE 754 constants
        rw!("f-one-sign"; "(comp f-one f-sign)" => "t"),
        rw!("f-zero-sign"; "(comp f-zero f-sign)" => "t"),
        rw!("f-pi-sign"; "(comp f-pi f-sign)" => "t"),

        // IEEE 754 function properties
        rw!("f-recip-sign"; "(comp f-recip f-sign)" => "f-sign"),

    let tree = load_tree(&mut std::io::stdin())?;
    info!(target: "jelly",
          "Input expression has size {} and cost {}",
          AstSize.cost_rec(&tree), CAMCostModel.cost_rec(&tree));

    let runner = Runner::default().with_expr(&tree).run(rules);
    info!(target: "jelly",
          "E-graph finished running: {:?} after {} iterations",
          runner.stop_reason.unwrap(), runner.iterations.len());

    let mut extractor = Extractor::new(&runner.egraph, CAMCostModel);
    let (best_cost, best_expr) = extractor.find_best(runner.roots[0]);
    info!(target: "jelly",
          "Best expression has size {} and cost {}",
          AstSize.cost_rec(&best_expr), best_cost);