Makefile

all:
	ocamlfind opt -g -rectypes -syntax camlp5o -package ocanren,ocanren.syntax,GT,GT.syntax.all -linkpkg -o poly poly.ml

clean:
	rm *.cm[oix] *.o poly

Polynomial.ml

open MiniKanrenCore
open MiniKanrenStd

module Poly =
  struct
    type bop = ADD | MUL

    module T =
      struct
        @type ('int, 'nat, 'var, 'bop, 't) t =
          | Const of 'int
          | Var   of 'var * 'nat
          | Bop   of 'bop * 't * 't
        with gmap;;

        let fmap fa fb fc fd fe x = GT.gmap(t) (fa) (fb) (fc) (fd) (fe) x
      end

    type tt = (Nat.ground, Nat.ground, string, bop, tt) T.t

    type tl = inner logic
      and inner = (Nat.logic, Nat.logic, string logic, bop logic, tl) T.t

    type ti = (tt, tl) injected

    module FT = Fmap5(T)

    let const i     = inj @@ FT.distrib @@ T.Const i
    let var x n     = inj @@ FT.distrib @@ T.Var (x, n)
    let bop op l r  = inj @@ FT.distrib @@ T.Bop (op, l, r)
    let sum         = bop !!ADD
    let prod        = bop !!MUL

    let rec inj : tt -> tl = fun t -> to_logic (T.fmap (Nat.inj) (Nat.inj) (to_logic) (to_logic) (inj) t)

    (* let _:int = inj *)

    let rec reify' h = FT.reify (Nat.reify) (Nat.reify) (reify) (reify) (reify') h
    let reify = reify'

    let rec diff p dp x = conde [
      fresh (i)
        (p  === const i)
        (dp === const Nat.zero);

      fresh (n m)
        (p === var x n)
        (conde [
          fresh (i)
            (n  === Nat.one)
            (dp === const n);
          fresh (m)
            (Nat.gto n Nat.one !!true)
            (n  === Nat.succ m)
            (dp === prod (const n) (var x m));
        ]);

      fresh (y n)
        (x  =/= y)
        (p  === var y n)
        (dp === p);

      fresh (l r dl dr)
        (p  === sum  l  r )
        (dp === sum  dl dr)
        (diff l dl x)
        (diff r dr x);

      fresh (l r a b dl dr)
        (p  === prod l  r )
        (dp === sum  a  b )
        (a  === prod dl r )
        (b  === prod l  dr)
        (diff l dl x)
        (diff r dr x);
    ]

    let rec show_helper p = T.(
      let show_nat n = GT.show(Nat.logic) n in
      let show_var x = GT.show(logic) (GT.show(GT.string)) x in
      let show_op op = GT.show(logic) (fun op -> match op with | ADD -> "+" | MUL -> "*") op in
      match p with
      | Const i         -> show_nat i
      | Var (x, n)      -> Printf.sprintf "%s^%s" (show_var x) (show_nat n)
      | Bop (op, l, r)  -> Printf.sprintf "(%s) %s (%s)" (show l) (show_op op) (show r)
      )
    and show p = GT.show(logic) show_helper p

    let print p = Printf.printf "%s\n" (show @@ p#reify reify ~inj)
  end

open Poly

let one   = Nat.one
let two   = Nat.succ one
let three = Nat.succ two

let x = !!"x"


let () = Printf.printf "Differentiation of x^2 + x + 1\n"

let p = sum (var x two) (sum (var x one) (const one))

let () =
  run q
    (fun q  -> diff p q x)
    (fun qs -> Stream.iter print qs)

let () = Printf.printf "Integration of 2*x + 1\n"

let dp = sum (prod (const two) (var x one)) (const one)

let () =
  run q
    (fun q  -> diff q dp x)
    (fun qs -> Stream.iter print qs)