OCaml code snippets proposed as CC-BY-SA 4.0 candidates

[Gopiandcode]

@SpiceGuid

Note that Program Fixpoint subset does not compile as it is now (any help appreciated).

Oh, how I have waited for this moment! Finally, a copyleft-style project that I can actually meaningfully contribute to!

Anyway, here is a proof of the Program fixpoint subset’s obligations:

(* l'arbre ta est-il un sous-ensemble de l'arbre tb ? *)
Program Fixpoint subset (ta : tree) (tb : tree) {measure (cardinal ta + cardinal tb)} : bool :=
  match ta,tb with
  | Empty,_ => true
  | _,Empty => false
  | Fork la na ra,Fork lb nb rb => 
      match na ?= nb with
      | Lt => subset (Fork la na Empty) lb && subset ra tb
      | Gt => subset (Fork Empty na ra) rb && subset la tb
      | Eq => subset la lb && subset ra rb
      end
  end.
Obligation 1.
Proof.
  simpl.
  do 4 rewrite <- Nat.add_assoc.
  do 2 apply plus_lt_compat_l.
  rewrite Nat.add_comm.
  rewrite Nat.add_assoc.
  rewrite (Nat.add_comm (cardinal ra)).
  do 2 rewrite <- Nat.add_assoc.
  apply plus_lt_compat_l.
  apply Nat.lt_lt_add_r.
  auto.
Qed.
Obligation 2.
Proof.
  simpl.
  rewrite (Nat.add_comm (cardinal la + 1)).
  do 2 rewrite <- Nat.add_assoc.
  apply plus_lt_compat_l.
  rewrite Nat.add_assoc.
  rewrite (Nat.add_comm (cardinal la + 1)).
  do 3 rewrite <- Nat.add_assoc.
  do 2 apply plus_lt_compat_l.
  apply Nat.lt_add_pos_r.
  rewrite Nat.add_1_r.
  apply Nat.lt_0_succ.
Qed.
Obligation 3.
Proof.
  simpl.
  rewrite (Nat.add_comm (_) 1); rewrite <- Nat.add_shuffle1.
  rewrite Nat.add_shuffle0; rewrite (Nat.add_assoc 1).
  rewrite <- (Nat.add_assoc _ (cardinal la)).
  rewrite (Nat.add_comm (cardinal la)).
  do 4 rewrite <- Nat.add_assoc; do 2 apply plus_lt_compat_l.
  apply Nat.lt_add_pos_r.
  rewrite Nat.add_1_r.
  apply (Nat.lt_lt_add_l 0 (S (cardinal lb)) (cardinal la)).
  apply Nat.lt_0_succ.
Qed.
Obligation 4.
Proof.
  simpl.
  rewrite Nat.add_shuffle0. 
  rewrite <- (Nat.add_assoc _ (cardinal ra)). 
  rewrite (Nat.add_comm (cardinal ra)); rewrite (Nat.add_assoc (cardinal _ + _)). 
  rewrite <- (Nat.add_assoc _ 1); rewrite (Nat.add_comm 1 (_ + _)).
  do 5 rewrite <- Nat.add_assoc.
  do 3 apply plus_lt_compat_l.
  apply Nat.lt_add_pos_r.
  rewrite Nat.add_1_l.  
  apply Nat.lt_0_succ.
Qed.
Obligation 5.
Proof.
  simpl.
  rewrite Nat.add_shuffle0; rewrite <- (Nat.add_assoc _ 1).
  rewrite (Nat.add_comm 1 _); do 4 rewrite <- Nat.add_assoc.
  apply plus_lt_compat_l.
  apply Nat.lt_add_pos_r.
  rewrite Nat.add_1_l.  
  apply Nat.lt_0_succ.
Qed.
Obligation 6.
Proof.
  simpl.
  rewrite (Nat.add_comm (_ + 1));  rewrite Nat.add_shuffle2.
  apply Nat.lt_add_pos_r; rewrite (Nat.add_comm _ 1).
  rewrite Nat.add_1_l; apply Nat.lt_0_succ.
Qed.

Mainly just a bit of number pushing, nothing really fancy here, and I’m pretty sure there is probably a nicer way of writing this (omega?).

Naturally, CC-BY-SA.

[Armael]

@Gopiandcode

Mainly just a bit of number pushing, nothing really fancy here, and I’m pretty sure there is probably a nicer way of writing this (omega?).

Indeed, a simple simpl; lia will be able to solve each of the obligations here.

[Gopiandcode]

@Armael

Indeed, a simple simpl; lia will be able to solve each of the obligations here.

Ah, nice; thanks. Don’t usually do too much pure numerical stuff, and mostly stick to ssreflect, so I’m not that familiar with the vanilla coq tactics. The more you know.

Updated proof, indeed everything seems to go through with just lia.

Require Import Lia.
(* l'arbre ta est-il un sous-ensemble de l'arbre tb ? *)
Program Fixpoint subset (ta : tree) (tb : tree) {measure (cardinal ta + cardinal tb)} : bool :=
  match ta,tb with
  | Empty,_ => true
  | _,Empty => false
  | Fork la na ra,Fork lb nb rb => 
      match na ?= nb with
      | Lt => subset (Fork la na Empty) lb && subset ra tb
      | Gt => subset (Fork Empty na ra) rb && subset la tb
      | Eq => subset la lb && subset ra rb
      end
  end.
Next Obligation. Proof. simpl; lia. Qed.
Next Obligation. Proof. simpl; lia. Qed.
Next Obligation. Proof. simpl; lia. Qed.
Next Obligation. Proof. simpl; lia. Qed.
Next Obligation. Proof. simpl; lia. Qed.
Next Obligation. Proof. simpl; lia. Qed.

[SpiceGuid]

@Gopiandcode

Oh, how I have waited for this moment! Finally, a copyleft-style project that I can actually meaningfully contribute to!

It feels like magic.
Many thanks to you and @Armael

Of course the challenge continues.
Then if you complete it you will have to write almost all the chapter 5 (Certifying your code with Coq) of my copyleft book project.
Please, if possible, no ssreflect, just vanilla coq tactics.

(* specification des opérations ensemblistes *)

Theorem interval_main_property :
  forall low high n t, member n (interval low high t) <-> member n t /\ low <= n <= high.
Proof.
Admitted.

Theorem remove_main_property :
  forall n t, ~ member n (remove n t).
Proof.
Admitted.

Theorem remove_is_conservative :
  forall m n t, member m t /\ m <> n -> member m (remove n t).
Proof.
Admitted.

Theorem filter_main_property :
  forall n t cond, member n (filter cond t) <-> member n t /\ cond n.
Proof.
Admitted.

Theorem union_main_property :
  forall n ta tb, member n ta \/ member n tb <-> member n (union ta tb).
Proof.
Admitted.

Theorem intersection_main_property :
  forall n ta tb, member n ta /\ member n tb <-> member n (intersection ta tb).
Proof.
Admitted.

Theorem subset_main_property :
  forall n ta tb, (member n ta -> member n tb) <-> subset ta tb.
Proof.
Admitted.

Theorem disjoint_main_property :
  forall n ta tb, (member n ta -> ~ member n tb) <-> disjoint ta tb = true.
Proof.
Admitted.

Theorem difference_main_property :
  forall n ta tb, (member n ta /\ ~ member n tb) <-> member n (difference ta tb).
Proof.
Admitted.

Theorem interval_preserves_order :
  forall t, tree_ordered t ->
  forall low high, tree_ordered (interval low high t).
Proof.
Admitted.

Theorem remove_preserves_order :
  forall t, tree_ordered t ->
  forall n, tree_ordered (remove n t).
Proof.
Admitted.

Theorem filter_preserves_order :
  forall t, tree_ordered t ->
  forall cond, tree_ordered (filter cond t).
Proof.
Admitted.

Theorem union_preserves_order :
  forall ta tb, tree_ordered ta /\ tree_ordered tb -> tree_ordered (union ta tb).
Proof.
Admitted.

Theorem intersection_preserves_order :
  forall ta tb, tree_ordered ta /\ tree_ordered tb -> tree_ordered (intersection ta tb).
Proof.
Admitted.

Theorem difference_preserves_order :
  forall ta tb, tree_ordered ta /\ tree_ordered tb -> tree_ordered (difference ta tb).
Proof.
Admitted.

[SpiceGuid]

An adventure in data collections
(This is my own original code)

(* categorical functor *)
module type Functor =
sig
   type 'a t
   val map : ('a -> 'b) -> 'a t -> 'b t
end

(* minimalist intuition about a polymorph data collection *)
module type DataCollection =
sig
   include Functor
   val size : 'a t -> int 
   type index
   val member : index -> 'a t -> 'a
end

(* Stdlib.List *)
module StdList
:
sig
   include DataCollection
   with type 'a t = 'a list 
   with type index = int 
end
=
struct
   type 'a t =
      'a list
   let map =
      List.map
   let size =
      List.length
   type index =
      int
   let member n l =
      List.nth l n
end

(* Stdlib.Array *)
module StdArray
:
sig
   include DataCollection
   with type 'a t = 'a array
   with type index = int 
end
=
struct
   type 'a t =
      'a array
   let map =
      Array.map
   let size =
      Array.length
   type index =
      int
   let member n a =
      Array.get a n
end

(* type PairIndex.index *)
module PairIndex
=
struct
   type index = Fst | Snd
end

(* a pair of values *)
module Pair
:
sig
   include DataCollection
   with type 'a t = 'a * 'a
   with type index = PairIndex.index
end
=
struct
   type 'a t =
      'a * 'a
   let map f (x,y) =
      (f x,f y)
   let size t =
      2
   type index =
      PairIndex.index
   let member i (x,y) =
      let open PairIndex in
      match i with
      | Fst -> x
      | Snd -> y
end


(* Braun min-heap *)
module BraunHeap
:
sig
   include DataCollection
   with type index = unit
   val empty : 'a t
   val add : 'a -> 'a t -> 'a t 
   val replace : 'a -> 'a t -> 'a t
   val remove : 'a t -> 'a t 
end
=
struct
   type 'a t =
      | Empty
      | Fork of 'a t * 'a * 'a t
   let rec map f = function
      | Empty -> Empty
      | Fork(l,n,r) -> Fork(map f l,f n,map f r)
   let rec diff n = function
      | Empty -> if n = 0 then 0 else assert false
      | Fork(l,_,r) ->
         if n = 0 then 1
         else if n mod 2 = 1 then diff ((n - 1) / 2) l
         else diff ((n - 2) / 2) r
   let rec size = function
      | Empty -> 0
      | Fork(l,_,r) -> let m = size r in 2 * m + 1 + diff m l
   type index =
      unit
   let member () = function
      | Empty -> invalid_arg "BraunHeap.member"
      | Fork(_,n,_) -> n
   let empty =
      Empty
   let rec add n = function
      | Empty -> Fork(Empty,n,Empty)
      | Fork(l,m,r) ->
         if n < m then Fork(add m r,n,l)
         else Fork(add n r,m,l)
   let rec replace n = function
      | Empty -> invalid_arg "BraunHeap.replace"
      | Fork((Fork(_,m,_) as l),_,Empty)
         when m < n ->
         Fork(replace n l,m,Empty)
      | Fork((Fork(_,na,_) as l),_,(Fork(_,nb,_) as r))
         when na < n || nb < n ->
         if na < nb
         then Fork(replace n l,na,r)
         else Fork(l,nb,replace n r)
      | Fork(l,_,r) -> Fork(l,n,r)
   let rec remove = function
      | Empty -> invalid_arg "BraunHeap.remove"
      | Fork(t,_,Empty) -> t
      | Fork(Empty,_,_) -> assert false
      | Fork((Fork (_,na,_) as l),_,(Fork( _,nb,_) as r)) ->
         if na < nb
         then Fork(r,na,remove l)
         else Fork(replace na r,nb,remove l)
end


(* type 'a NestT.t *)
module NestT
=
struct
   type 'a t =
      | Nil
      | Cons of 'a * ('a * 'a) t
end

(* a nested datatype from the paper "Nested Datatypes"
 * by Richard Bird and Lambert Meertens 1998
 *)
module Nest
:
sig
   include DataCollection
   with type 'a t = 'a NestT.t
   with type index = int
end
=
struct
   type 'a t =
      'a NestT.t
   let rec map : 'a 'b . ('a -> 'b) -> 'a t -> 'b t = 
      fun f -> function
      | Nil -> Nil
      | Cons(h,t) -> Cons(f h,map (Pair.map f) t)
   let rec size : 'a . 'a t -> int = function
      | Nil -> 0
      | Cons(_,t) -> 1 + 2 * size t
   type index =
      int
   let rec member : 'a . index -> 'a t -> 'a =
      fun n -> function
      | Nil -> failwith "Nest.member"
      | Cons(h,t) ->
            if n=0 then h else
            let x,y = member (n/2) t in
            if n mod 2 = 0 then x else y
end

[SpiceGuid]

Brute force functional 8-Queens problem
(This is my own original code except the permute function is borrowed from a book whose title i don’t remember)

The 8-queens problem is to place 8 queens on a regular chessboard without any threatening possible.

let rec distribute a l =
   match l with 
   | []   -> [[a]]
   | h::t -> (a::l) :: List.map (fun x -> h::x) (distribute a t)
  
let rec permute = function
   | []   -> [[]]
   | h::t -> List.flatten (List.map (distribute h) (permute t))

let rec one_safe low high = function
   | []   -> true
   | h::t -> h <> low && h <> high && one_safe (low - 1) (high + 1) t

let rec all_safe = function
   | []   -> true
   | h::t -> one_safe (h - 1) (h + 1) t && all_safe t  

let _ =
   List.filter all_safe (permute [1;2;3;4;5;6;7;8])

This is more elegant than the OOP backtracking version. Unfortunately it’s slow and memory hungry.
Does anyone know a 8-queens solution that retains the smart functional style and yet still compete with the backtracking version ?

[SpiceGuid]

@yawaramin

What is a ‘Statement of Rights violation’? Are you referring to the fact that currently all user contributions to this Discourse are licensed under CC BY-NC-SA ( Terms of Service - OCaml )?

The best code (or the more appropriate code) may be found on a blogpost like this one. Then you know the author’s name but you have no more information. You don’t know how to contact him / her. You don’t know if the ocaml code is copyleft or copyright. The knowledge is there but you can’t reuse it.

This thread motivation is : i post my code or code found in a blogspot or La lettre de Caml or wherever.
If nobody complains about copyright then i tend to consider that the code snippet becomes de-facto CC-BY-SA 4.0 or compatible.

[jjb]

@SpiceGuid

If nobody complains about copyright then i tend to consider that the code snippet becomes de-facto CC-BY-SA 4.0 or compatible.

Do you know of any legal support for such a position? IANAL but that seems very suspect to me.

[SpiceGuid]

A good code, publicly available, does not deserve to be forgotten forever just because no law supports me to declare it as creative-commons.
Do you suggest i could do without a queue module just because Chris Okasaki published it before i do?
Plus the more people like @Armael & @Gopiandcode post their own contribution here, the less educational programming books will be boring due to code attrition.

(PS: i have liked your post because technically you are right)

[xavierleroy]

@SpiceGuid

If nobody complains about copyright then i tend to consider that the code snippet becomes de-facto CC-BY-SA 4.0 or compatible.

I am not a lawyer, but this sounds like you’re walking on very thin legal ice.

What about exercising your Right to quote - Wikipedia ? Taking small code snippets and integrating them into a textbook sounds like a valid case of quoting to me. (But again: I am not a lawyer.) Make sure to credit the original authors, though.

[yawaramin]

@SpiceGuid

If nobody complains about copyright then i tend to consider that the code snippet becomes de-facto CC-BY-SA 4.0…

IANAL but I don’t think it works like that. Anyway keeping the focus on this Discourse, the copyright for all contributions here including code samples is already defined (as I mentioned earlier). Again, I’m not a lawyer, but I don’t think we can override the license defined in the Terms of Service just by saying so.

[SpiceGuid]

To facilitate the lawyers work i have marked as such each and every occurrence of outrageous plagiarism.
Just press Ctrl + F and enter “plagiarism” to find all the stolen work.

[SpiceGuid]

The Marvin Minsky universal turing machine, 1962
(This is my own original code)

OCaml does an amazing work of tail-call optimization.

(* the 4 colors *)
type color =
  | C3 (* red   *)
  | C2 (* green *)
  | C1 (* blue  *)
  | C0 (* white *)

(* a transition: write color c, cursor + i, state s *)
let trans (c3,c2,c1,c0) (i3,i2,i1,i0) (s3,s2,s1,s0) tape cursor =
  match tape.(cursor) with
  | C3 -> tape.(cursor) <- c3; s3 tape (i3 cursor)
  | C2 -> tape.(cursor) <- c2; s2 tape (i2 cursor)
  | C1 -> tape.(cursor) <- c1; s1 tape (i1 cursor)
  | C0 -> tape.(cursor) <- c0; s0 tape (i0 cursor)

(* halt the machine *)
let stop cursor = cursor
let halt tape cursor = () 

(* the 7 states and the machine transition matrix *)
let
rec s0 t = trans (C2,C0,C3,C2) (pred,pred,succ,succ) (s4,s1,s0,s0) t
and s1 t = trans (C1,C0,C3,C0) (pred,pred,succ,pred) (s1,s1,s0,s1) t
and s2 t = trans (C1,C2,C3,C2) (succ,succ,succ,pred) (s2,s2,s2,s4) t
and s3 t = trans (C1,C2,C3,C3) (succ,succ,succ,pred) (s3,s3,s3,s4) t
and s4 t = trans (C1,C2,C3,C0) (pred,pred,pred,stop) (s5,s4,s4,halt) t
and s5 t = trans (C1,C2,C1,C2) (pred,pred,pred,succ) (s5,s5,s6,s2) t
and s6 t = trans (C0,C0,C1,C2) (succ,succ,succ,succ) (s0,s6,s6,s3) t

[SpiceGuid]

Multi-precision natural numbers
(This is my own original code)

Includes Karatsuba multiplication and Burnikel-Ziegler division.
For maximal performance compile with the -noassert flag.

type big_nat = int array
type t = big_nat


let base =
  match Sys.word_size with
  | 32 -> 10000 
  | 64 -> 1000000000 
  | _  -> 10

(* let base = 10;; *)

let zero_big = ([|0|]: big_nat)

let unit_big = ([|1|]: big_nat)

let big_of_int n =
  assert (0 <= n && n < base * base);
  if n < base then ([|n|]: big_nat)
  else ([|n / base;n mod base|]: big_nat)

let print_big (a: big_nat) =
  let print i n =
    if i=0 then print_int n
    else if base=10 then print_int n
    else if base=10000 then Printf.printf "%04d" n
    else Printf.printf "%09d" n
  in Array.iteri print a

let add_big (a: big_nat) (b: big_nat) =
  assert (Array.length a >= Array.length b);
  let result = ref a
  and carry  = ref 0
  and i = ref (Array.length a - 1)
  and j = ref (Array.length b - 1)
  in begin
    while !j >= 0 do
      let d = a.(!i) + b.(!j) + !carry
      in if d < base then begin
        carry := 0; a.(!i) <- d 
      end else begin
        carry := 1; a.(!i) <- d - base
      end;
      decr i; decr j; 
    done;
    while !carry > 0 do
      if !i >= 0 then begin
        let d = a.(!i) + !carry
        in if d < base then begin
          carry := 0; a.(!i) <- d 
        end else begin
          a.(!i) <- d - base
        end;
        decr i;
      end else begin
        result := Array.make (Array.length a + 1) 0;
        Array.blit a 0 !result 1 (Array.length a);
        !result.(0) <- 1; carry := 0;
      end;
    done;
    !result
  end
  

let sum_big (a: big_nat) (b: big_nat) =
  if Array.length a >= Array.length b then
    add_big (Array.copy a) b
  else 
    add_big (Array.copy b) a


let compare_big (a: big_nat) (b: big_nat) =
  if Array.length a < Array.length b then -1
  else if Array.length a > Array.length b then 1
  else
    let i = ref 0 in
    begin
      while !i < Array.length a && a.(!i) = b.(!i) do
        incr i;
      done;
      if !i = Array.length a then 0
      else if a.(!i) > b.(!i) then 1
      else -1
    end

let min_big (a: big_nat) (b: big_nat) =
  if compare_big a b < 0 then a else b

let max_big (a: big_nat) (b: big_nat) =
  if compare_big a b > 0 then a else b

let sub_big (a: big_nat) (b: big_nat) =
  assert (compare_big a b >= 0);
  let result = ref a
  and carry  = ref 0
  and i = ref (Array.length a - 1)
  and j = ref (Array.length b - 1)
  in begin
    while !j >= 0 do
      let d = a.(!i) - b.(!j) - !carry
      in if d >= 0 then begin
        carry := 0; a.(!i) <- d 
      end else begin
        carry := 1; a.(!i) <- d + base
      end;
      decr i; decr j; 
    done;
    while !carry > 0 do
      let d = a.(!i) - !carry
      in if d >= 0 then begin
        carry := 0; a.(!i) <- d 
      end else begin
        a.(!i) <- d + base
      end;
      decr i;
    done;
    if !i < 0 then begin
      i := 0; j := Array.length a - 1;
      while a.(!i) = 0 && !i < !j  do incr i; done;
      if !i >= 0 then result := Array.sub a !i (Array.length a - !i);
    end;  
    !result
  end


let diff_big (a: big_nat) (b: big_nat) =
  assert (compare_big a b >= 0);
  sub_big (Array.copy a) b


let scale_up_big (a: big_nat) n =
  assert (0 <= n && n < base);
  if n = 0 then zero_big
  else 
    let accu  = ref 0 
    and carry = ref 0
    and result: big_nat = Array.make (Array.length a + 1) 0
    in begin
      for i = (Array.length a) downto 1 do
        accu := a.(i-1) * n + !carry; 
        result.(i) <- !accu mod base; carry := !accu/base
      done;
      result.(0) <- !carry;
      if !carry = 0 then
        (Array.sub result 1 (Array.length a): big_nat)
      else
        result  
    end


let shift_big (a: big_nat) n =
  assert (n >= 0);
  if a = zero_big then zero_big
  else
    let result: big_nat = Array.make (Array.length a + n) 0
    in begin
      Array.blit a 0 result 0 (Array.length a);
      result
    end


let long_mult_big (a: big_nat) (b: big_nat) =
  let i = ref 0
  and j = ref (Array.length b-1) in
  let result = ref (shift_big (scale_up_big a b.(!i)) !j) 
  in begin
    while !j > 0 do
      incr i; decr j;
      result := add_big !result (shift_big (scale_up_big a b.(!i)) !j)
    done;  
    !result
  end


let array_sub (a: big_nat) start len = 
  let i = ref start and n = ref len in
  while a.(!i)=0 && !n > 1 do
    incr i; decr n;
  done;
  (Array.sub a !i !n : big_nat)


let karatsuba_threshold = 30

let rec mult_big (a: big_nat) (b: big_nat) =
  if Array.length a < Array.length b then
    mult_big b a
  else if Array.length b < karatsuba_threshold then
    long_mult_big a b
  else 
    karatsuba_big a b
and karatsuba_big (p: big_nat) (q: big_nat) =
  assert (Array.length p >= Array.length q);
  let len_p = Array.length p  in
  let len_q = Array.length q  in
  let     n = len_p / 2       in
  let     a = array_sub p 0 (len_p - n)  in
  let     b = array_sub p (len_p - n) n  in
  if len_q > n then  
    let      c = array_sub q 0 (len_q - n)  in
    let      d = array_sub q (len_q - n) n  in
    let     ac = mult_big a c  in
    let     bd = mult_big b d  in
    let  ad_bc = sub_big (sub_big (mult_big (sum_big a b) (sum_big c d)) ac) bd
    in
    add_big (add_big (shift_big ac (2*n)) (shift_big ad_bc n)) bd
  else  
    let     aq = mult_big a q in
    let     bq = mult_big b q in
    add_big (shift_big aq n) bq


let square_big (a: big_nat) = mult_big a a


let rec power_big (a: big_nat) n =
  assert (n >= 0);
  if n=0 then unit_big
  else if n=1 then a
  else
    let b = power_big a (n/2) in
    if (n mod 2 = 0) then mult_big b b 
    else mult_big (mult_big b b) a


let scale_down_big (a: big_nat) n =
  assert (0 < n && n < base * base);
  let last  = Array.length a - 1 in
  let accu  = ref 0 
  and carry = ref 0
  and result: big_nat = Array.copy a
  in begin
    for i = 0 to last do
      accu := a.(i) + !carry * base; 
      result.(i) <- !accu/n; carry := !accu mod n
    done;
    if (result.(0) = 0) && (last > 0) then
      (array_sub result 1 last: big_nat),!carry
    else
      result,!carry
  end


let rec burnikel_ziegler_big (a: big_nat) (b: big_nat) =
  if Array.length b <= 2 then
    let b2 = if Array.length b < 2 then b.(0) else b.(0)*base + b.(1) in
    let q,r = scale_down_big a b2
    in  q,big_of_int r
  else    
    let   len_a = Array.length a               in
    let   len_b = Array.length b               in
    let       n = (len_b - 1) / 2              in
    let      a0 = array_sub a (len_a - n) n    in
    let      a1 = array_sub a 0 (len_a - n)    in
    if compare_big a1 b >= 0 then
      let q1,r1 = burnikel_ziegler_big a1 b    in
      let q0,r0 = burnikel_ziegler_big (sum_big (shift_big r1 n) a0) b
      in  sum_big (shift_big q1 n) q0,r0
    else
      let    b0 = array_sub b (len_b - n) n    in
      let    b1 = array_sub b 0 (len_b - n)    in
      let q1,r1 = burnikel_ziegler_big a1 b1   in
      let a0_r1 = sum_big (shift_big r1 n) a0  in
      let b0_q1 = mult_big b0 q1               in
      if compare_big a0_r1 b0_q1 >= 0 then
        let plus_x = diff_big a0_r1 b0_q1
        in  q1,plus_x
      else
        let minus_x = diff_big b0_q1 a0_r1 in
        diff_big q1 unit_big, diff_big b minus_x


let quomod_big (a: big_nat) (b: big_nat) =
  if b = zero_big then raise Division_by_zero
  else if compare_big a b < 0 then zero_big,a
  else burnikel_ziegler_big a b

let div_big (a: big_nat) (b: big_nat) =
  let q,r = quomod_big a b in q

let mod_big (a: big_nat) (b: big_nat) =
  let q,r = quomod_big a b in r

[SpiceGuid]

@shenlebantongying

Can u put them in a git repo later?

I will do no repo. Press Ctrl + A and paste the whole in your favourite text editor. Then you can search and save.
What i will do is that all code in the future book will be available as a single zip archive file.

[SpiceGuid]

Braun-tree as a stack datatype
(The concat function is a translation from hackage/Data.Tree.Braun)
(The diff & size functions are from a paper by Chris Okasaki)

type t =
   | Empty
   | Fork of t * int * t

let empty =
   Empty 

let singleton n =
   Fork(Empty,n,Empty)  
   
let rec add n = function
   | Empty -> singleton n
   | Fork(l,m,r) -> Fork(add m r,n,l)
   
let rec member i = function 
   | Empty -> invalid_arg "BraunStack.member"
   | Fork(l,n,r) ->
      if i = 0 then n else
      if i land 1 = 1 then member (i / 2) l
      else member (i / 2 - 1) r
      
let rec concat ta tb =
   match ta with
   | Empty -> Empty
   | Fork(l,n,r) -> Fork(tb,n,concat l r)

let remove = function
   | Empty -> invalid_arg "BraunStack.remove"
   | Fork(l,_,r) -> concat l r

let rec replace i x = function 
   | Empty -> invalid_arg "BraunStack.replace"
   | Fork(l,y,r) ->
      if i = 0 then Fork(l,x,r) else
      if i land 1 = 1 then Fork(replace (i / 2) x l,y,r)
      else Fork(l,y,replace (i / 2 - 1) x r)
      
let rec diff n = function
   | Empty -> if n = 0 then 0 else assert false
   | Fork(l,_,r) ->
      if n = 0 then 1
      else if n mod 2 = 1 then diff ((n - 1) / 2) l
      else diff ((n - 2) / 2) r
      
let rec size = function
   | Empty -> 0
   | Fork(l,_,r) -> let m = size r in 2 * m + 1 + diff m l

[SpiceGuid]

ℝ → ℝ functions :

type t = 
	| X			 (* the x variable *)
	| R of float (* a real number  *)
	| Add of t * t
	| Mul of t * t
	| Sin of t
	| Cos of t
	| Tan of t
	| Log of t
	| Exp of t
	| Power of t * float

Recursion for derive :

let rec recu c = function
	| X -> c#x
	| R k -> c#r
	| Add (u,v) -> c#add (recu c u) (recu c v)
	| Mul (u,v) -> c#mul u (recu c u) v (recu c v)
	| Sin u -> c#sin u (recu c u)
	| Cos u -> c#cos u (recu c u)
	| Tan u -> c#tan u (recu c u)
	| Log u -> c#log u (recu c u)
	| Exp u -> c#exp u (recu c u)
	| Power (u,2.) -> c#power_2 u (recu c u)
	| Power (u,a)  -> c#power_a u a (recu c u)

Laws for derive :

let derive =  
	recu (		
		object 
			method x = R 1.
			method r = R 0.
			method add du dv = Add (du,dv)
			method mul u du v dv = Add (Mul(du,v),Mul (u,dv))
			method sin u du = Mul (du,Cos(u))
			method cos u du = Mul (R(-1.),Mul (du,Sin(u)))
			method tan u du = Mul (du,Power(Cos(u),-2.))
			method log u du = Mul (du,Power(u,-1.))
			method exp u du = Mul (du,Exp u)
			method power_2 u du = Mul(R(2.),Mul(du,u))
			method power_a u a du = Mul(R(a),Mul(du,Power(u,a-.1.)))
		end )

When ocaml 4.14.0+ is used you can remove unnecessary parentheses.

[SpiceGuid]

Code demonstration for recursors.

type 'a set =
	| Empty
	| Fork of 'a node 
and 'a node =
	{left:'a set;item:'a;right:'a set}

Our recursor boilerplate code :

(* strict catamorphism *)
type ('a,'b) fold =
	<empty: 'a; fork: 'a -> 'b -> 'a -> 'a>
let rec fold s (case:('a,'b) fold) =
	match s with
	| Empty -> case#empty
	| Fork n -> case#fork (fold n.left case) n.item (fold n.right case)
(* lazy catamorphism *)
type ('a,'b) cata =
	<empty: 'a; fork: (unit -> 'a) -> 'b -> (unit -> 'a) -> 'a>
let rec cata s (case:('a,'b) cata) () =
	match s with
	| Empty -> case#empty
	| Fork n -> case#fork (cata n.left case) n.item (cata n.right case)

(* strict paramorphism *)
type ('a,'b) recu =
	<empty: 'b;
	 fork: 'a node -> 'b -> 'b -> 'b>
let rec recu s (case:('a,'b) recu) =
	match s with
	| Empty ->
			case#empty
	| Fork n ->
			case#fork n (recu n.left case) (recu n.right case)
(* lazy paramorphism *)
type ('a,'b) para =
	<empty: 'b;
	 fork: 'a node -> (unit -> 'b) -> (unit -> 'b) -> 'b>
let rec para s (case:('a,'b) para) () =
	match s with
	| Empty ->
			case#empty
	| Fork n ->
			case#fork n (para n.left case) (para n.right case)

Yes we will pass a lot of immediate objects as argument so ocaml 4.14.0+ is recommended here (so you can remove unnecessary parentheses).

let strahler s =
	fold s (
		object
			method empty = 0
			method fork l _ r =
				if l = r then r+1 else max l r
		end )
let cardinal s =
	fold s (
		object
			method empty = 0
			method fork l _ r = l + 1 + r
		end )
let singleton item =
	Fork {left=Empty;item;right=Empty}
let add x s =
	para s (
		object
			method empty =
				singleton x
			method fork n l r =
				let y = n.item in
				if x < y then Fork {n with left = l ()}
				else if x > y then Fork {n with right = r ()}
				else Fork n
		end ) ()
let member x s =
	cata s (
		object
			method empty = false
			method fork l y r =
				if x < y then l()
				else if x > y then r()
				else true
		end ) ()

let interval low high s =
	cata s (
		object
			method empty = Empty
			method fork l x r =
				if high < x then l ()
				else if low > x then r()
				else Fork {left=l ();item=x;right=r ()}
		end ) ()

let minimum n =
	fold n.left (
		object
			method empty acc = acc
			method fork l x r acc = l x 
		end ) n.item
		
let remove_minimum n =
	recu n.left (
		object
			method empty acc = acc
			method fork n l r acc = Fork {n with left=l n.right}
		end ) n.right
	
(* concatenation of sa + sb where max(sa) < min(sb) *)				
let concat sa sb =
	if sa = Empty then sb else
	match sb with
	| Empty -> sa
	| Fork n ->
		let item = minimum n
		and right = remove_minimum n
		in Fork {left=sa;item;right}

let remove x s =
	para s (
		object
			method empty =
				Empty
			method fork n l r =
				if x < n.item then Fork {n with left=l()}
				else if x > n.item then Fork {n with right=r()}
				else concat n.left n.right
		end ) ()	
	
let split x s =
	para s (
		object
			method empty =
				Empty,false,Empty
			method fork n l r =
				let y = n.item in
				if x < y then
					let a,b,c = l() in
					a,b,Fork {n with left = c}
				else if x > y then
					let a,b,c = r() in
					Fork {n with right = a},b,c
				else
					n.left,true,n.right
		end ) ()
let for_all cond s =
	cata s (
		object
			method empty = true
			method fork l y r =
				l() && cond y && r()
		end ) ()

(* set operations *)
let union sa sb =
	fold sa (
		object
			method empty s =
				s
			method fork la na ra s =
				match s with
				| Empty ->
					sa
				| Fork _ ->
					let lb,_,rb = split na s in
					Fork {left=la lb;item=na;right=ra rb}
		end ) sb
let intersection sa sb =
	fold sa (
		object
			method empty s =
				Empty
			method fork la na ra s =
				match s with
				| Empty ->
					Empty
				| Fork _ ->
					let lb,b,rb = split na s in
					if b then Fork {left=la lb;item=na;right=ra rb}
					else concat (la lb) (ra rb)
		end ) sb
let difference sa sb =
	recu sa (
		object
			method empty s =
				Empty
			method fork n la ra s =
				match s with
				| Empty ->
					Fork n
				| Fork _ ->
					let lb,b,rb = split n.item s in
					if b then concat (la lb) (ra rb)
					else Fork {left=la lb;item=n.item;right=ra rb}
		end ) sb
let disjoint sa sb =
	fold sa (
		object
			method empty s =
				true
			method fork la na ra s =
				match s with
				| Empty ->
					true
				| Fork _ ->
					let lb,b,rb = split na s in
					if b then false
					else la lb && ra rb
		end ) sb
let subset sa sb =
	fold sa (
		object
			method empty s =
				s = Empty
			method fork la na ra s =
				match s with
				| Empty ->
					false
				| Fork _ ->
					let lb,b,rb = split na s in
					if b then la lb && ra rb
					else false
		end ) sb

let equal sa sb =
	subset sa sb && subset sb sa