navesspiwack.mlt

(* -*- compile-command: "ocamlbuild -classic-display navesspiwack.pdf"  -*- *)

open Mlpost
open Latex
open Slides.Iterator
open Prelude

##plugin coqdoc
##verbatim '@' = coqdoc
##verbatim '#' = ocaml_code


let prelude = concat_with_sep [
  input "style.tex";
  color_prelude;
] par

let packages = [
  "inputenc" , "utf8" ;
]

let array_line = array_line ~sep:(`Mm 1.)


(** printing the intermediate structures of the algorithm with mlpost *)

type 'a tree =
| Node of 'a tree * 'a * 'a tree
| Leaf
| Leaf1

type 'a alt =
| Pivot of bool*'a (** [true] if selected for next step *)
| Tree of 'a tree

module Algo = struct

  open Mlpost

  (** parameters *)
  let bsize = Num.cm 0.7
  let height = bsize
  let width = bsize
  let textsize = large3
  let treesep = Num.cm 0.7
  let treebase_color = Color.mediumgray

  (** basic boxes *)
  let emptyb ?fill () =
    Box.empty ?fill ~height ~width ()

  let texbox ?fill x =
    let x' = textsize x in
    let () = Format.printf \"%s@.\" (Latex.to_string x') in
    let x'' = Melt.picture_of_latex x' in
    Box.pic ?fill x''

  let numb ?fill i = texbox ?fill (mode M (latex_of_int i))

  (** Make all boxes the same size then draw their borders. *)
  let normalize l =
    Box.same_height (Box.same_width l) |>
    List.map (fun b -> Box.rect ~dx:(Num.pt 0.) ~dy:(Num.pt 0.) b) |>
    List.map begin fun b ->
      match Box.get_fill (Box.nth 0 b) with
      | None -> b
      | Some c -> Box.set_fill c b
    end

  (** Draws a list of numbers. *)
  let pr_int_list l =
    emptyb ()::List.map numb l |>
    normalize |> (* uses emptyb to normalize the box size. *)
    List.tl |>
    Box.hbox

  (** Draws a tree bottom up *)
  let rec tree_height = function
    | Leaf -> 0
    | Leaf1 -> 1
    | Node (l,_,r) -> 1+max (tree_height l) (tree_height r)

  let rec expint a = function
    | 0 -> 1
    | n when n mod 2 = 0 -> expint (a*a) (n/2)
    | n -> a*(expint (a*a)) (n/2)

  let base_size t =
    let h = tree_height t in
    (expint 2 h) - 1

  let rec tree_map f = function
    | Node(l,x,r) -> Node (tree_map f l , f x , tree_map f r)
    | Leaf -> Leaf
    | Leaf1 -> Leaf1

  (* precondition: [base_size t = List.length ps] *)
  let assign_base_depth ps t =
    assert (base_size t = List.length ps);
    let push x (l,y,r) = (x::l,y,r) in
    let rec split_at n = function
      | a::l when n > 0 -> push a (split_at (n-1) l)
      | a::l when n = 0 -> ([],a,l)
      | _ -> assert false
    in
    let rec assign_base_depth ps size d = function
      | Node (l,x,r) ->
        let hsize = (size - 1)/2 in
        let (pl,a,pr) = split_at hsize ps in
        Node (
          assign_base_depth pl hsize (d+1) l ,
          (a,d,x) ,
          assign_base_depth pr hsize (d+1) r )
      | Leaf -> Leaf
      | Leaf1 -> Leaf1
    in
    assign_base_depth ps (base_size t) 0 t

  let pr_tree pr_elt ps t =
    let at = assign_base_depth ps t in
    let h = tree_height t in
    let pos_of_bd p d =
      let height = h - d in
      Point.shift p Point.(mult (Num.multf (float_of_int height) treesep) up)
    in
    let placed_t =
      tree_map begin fun (p,d,x) ->
        texbox (pr_elt x) |>
        Box.center (pos_of_bd p d)
      end at
    in
    let arrow_style = Arrow.(add_line empty) in
    (** [p] is the parent box *)
    let rec draw_arrows p = function
      | Leaf1 -> Command.nop
      | Leaf -> Command.nop
      | Node (l,x,r) ->
        let open Command in
        draw_arrows x l ++
        Arrow.box_to_box ~kind:arrow_style p x ++
        draw_arrows x r
    in
    let arrows =
      match placed_t with
      | Leaf -> Command.nop
      | Leaf1 -> Command.nop
      | Node (l,x,r) -> Command.(draw_arrows x l ++ draw_arrows x r)
    in
    let rec draw_boxes = function
      | Leaf -> Command.nop
      | Leaf1 -> Command.nop
      | Node (l,x,r) ->
        let open Command in
        draw_boxes l ++
        Box.draw x ++
        draw_boxes r
    in
    Command.(draw_boxes placed_t ++ arrows)

  let pr_alt_list_gen pr_pivot l =
    let rec genempty n =
      if n = 0 then []
      else (emptyb ~fill:treebase_color ()) :: genempty (n-1)
    in
    let rec gen_base = function
      | Pivot (b,i) :: l ->
        let (r,q) = gen_base l in
        let fill =
          if b then Some Color.lightblue
          else None
        in
        texbox ?fill (pr_pivot i) ::r , q
      | Tree t :: l ->
        let tq = genempty(base_size t) in
        let (r,q) = gen_base l in
        tq @ r , (t,tq)::q
      | [] -> [],[]
    in
    let (base,queue) = gen_base l in
    let base =
      normalize (base) |>
      Box.hbox
    in
    let trees =
      List.map begin fun (t,q) ->
        let ps =
          List.map begin fun b ->
            Box.ctr (Box.sub b base)
          end q
        in
        pr_tree pr_pivot ps t
      end queue
    in
    let open Command in
    Box.group [base;Box.pic(Picture.make(seq trees))]
    (* Box.draw base ++ *)
    (* seq trees *)

    let pr_alt_list l = Box.draw (pr_alt_list_gen (fun i -> (mode M (latex_of_int i))) l)

    (** The actual algorithm, in an incremental fashion *)

    (* mostly duplicated from [simple.ml] *)

    type state =
    | Init of int list
    | Unmarked of int alt list (** inv bools are all false *)
    | Marked of int alt list

    let pr_state = function
      | Init l -> Box.draw (pr_int_list l)
      | Unmarked l | Marked l -> pr_alt_list l

    let join l x r = Tree(Node(l,x,r))

    let complete list =
      let n = List.length list in
      let rec pow2 i = if i <= n then pow2 (2*i) else i in
      let missing = (pow2 1) - n - 1 in
      let rec pad missing = function
        | head::tail when missing <> 0 -> Tree Leaf1 :: Pivot (false,head) :: pad (missing - 1) tail
        | odd::even::others -> join Leaf odd Leaf :: Pivot(false,even) :: pad 0 others
        | [single] -> [join Leaf single Leaf]
        | [] -> []
      in
      pad missing list

    let rec select = function
      | Tree left :: Pivot (false,root) :: Tree right :: Pivot (false,e) :: others ->
        Tree left :: Pivot (true,root) :: Tree right :: Pivot (false,e) :: select others
      | [Tree left ; Pivot (false,root) ; Tree right] ->
        [Tree left ; Pivot (true,root) ; Tree right]
      | _ -> assert false

    let rec pass = function
      | Tree left :: Pivot (true,root) :: Tree right :: Pivot (false,e) :: others ->
        join left root right :: Pivot (false,e) :: pass others
      | [Tree left; Pivot (true,root); Tree right] -> [join left root right]
      | _ -> assert false

    let step = function
      | Init l -> Some (Unmarked (complete l))
      | Unmarked [Tree _] -> None
      | Unmarked l -> Some (Marked (select l))
      | Marked l -> Some (Unmarked (pass l))

    let run l =
      let rec run = function
        | None -> []
        | Some s -> s::(run (step s))
      in
      run (Some (Init l))

    let put_frame ?logo ?title l =
      let seq = list (run l) in
      let the_frame q =
        center (rule_ (`Pt 0.) (`Textheight 0.35) ^^ mlpost (pr_state q))
      in
      put seq (frame ?logo ?title the_frame)

end

(** /algo *)



let doc = ([
  title_put (list [1]) begin title_frame (fun _ ->
    textbf (huge2 "Balancing lists" ^^ newline ^^ large3"A proof pearl")
          ^^ newline_size (`Mm 6.) ^^ large2"Guyslain Naves \& Arnaud Spiwack"
  )end;

  put (list[1]) begin frame ~title:"Have you read this book?" (fun _ ->
    center (includegraphics ~height:Slides.(unit (height*.0.75)) "okasaki.png")
  )end;

  put (list[1]) begin frame ~title:"Lists as exponentiation" (fun _ ->
    "List of size $n$: type exponentiation $A^n$
     {displaymath (just_left `Brace (array [`L;`L;`L] [
       array_line [$A^0$;$=$;$1$];
       array_line [exponent$A$ $n+1$;$=$;$A{times}A^n$];
     ]))}{newline_size(`Mm 4.)}

     Example:
     {displaymath$[1;2;3;4;5;6;7;8;9;10;11]$}"
  )end;

  put (list[1]) begin frame ~title:"Lists as fast exponentiation" (fun _ ->
    "List of size $n$: still type exponentiation $A^n$
     {displaymath (just_left `Brace (array [`L;`L;`L] [
       array_line [$A^0$;$=$;$1$];
       array_line [exponent$A$ $2n$;$=$;$(A{times}A)^n$];
       array_line [exponent$A$ $2n+1$;$=$;$A{times}(A{times}A)^n$];
     ]))}{newline_size(`Mm 4.)}

     Example ($11 = {overline$1101$}^2$):
     {let thin = text\"\\\\,\" in
       displaymath$[1;(2,3);{thin^^cdot^^thin};(((4,5),(6,7)),((8,9),(10,11)))]$}"
  )end;

  put (list[1]) begin frame ~title:"Binary list datatype" (fun _ ->
    "{array [`L;`Vert;`L;`L] [
      array_line ~layout:[3,`L] ["<@Inductive BList (A:Type) : Type :=@>"];
      array_line ["";"<@zero@>";""];
      array_line ["";"<@twice@>";"<@(l:BList (A*A))@>"];
      array_line ["";"<@tpo@>";"<@(a:A) (l:BList (A*A)).@>"];
    ]}{newline_size(`Mm 10.)}

     Example ($11 = {overline$1101$}^2$):
     {let thin = text\"\\\\,\" in
       displaymath (array [`C] [
         array_line [$[1;(2,3);{thin^^cdot^^thin};(((4,5),(6,7)),((8,9),(10,11)))]$];
         array_line ["<@tpo 1 (tpo (2,3) (twice (tpo (((4,5),(6,7)),((8,9),(10,11))) zero)))@>"];
       ])}"
  )end;

  Algo.put_frame ~title:"From list to trees" [1;2;3;4;5;6;7;8;9;10;11;12;13;14;15];

  Algo.put_frame  ~title:"Fill up to $2^n-1$" [1;2;3;4;5;6;7;8;9;10;11];

  put (list[1;2;3;4]) begin frame ~title:"Restricting to length $2^n-1$" (fun p ->
    let c x =
      x |>
      apply (color black) ~at:(p=1) |>
      apply (color blue) ~at:(p=2) |>
      apply (color white) ~at:(p>2)
    in
    let def =
      only ~at:(p<=2) "<@Inductive BList (A:Type) : Type :=@>" ^^
      only ~at:(p>2) "<@Inductive PowerList (A:Type) : Type :=@>"
    in
    "{array [`L;`Vert;`L;`L] [
      array_line ~layout:[3,`L] [def];
      array_line ["";"<@zero@>";""];
      array_line ["";c "<@twice@>";c "<@(l:BList (A@"*"@A))@>"];
      array_line ["";"<@tpo@>";"<@(a:A) (l:BList (A*A)).@>"];
    ]}
    {newline_size (`Mm 10.)}

    {apply (color white) ~at:(p<=3) "
      Example:
      {displaymath (array [`C] [
        array_line [$[ 1 ; (2,3) ; ((4,5),(6,7)) ]$];
        array_line ["<@tpo 1 (tpo (2,3) (tpo ((4,5),(6,7)) zero ))@>"];
      ])}"}"
  )end;

  put (list[1]) begin frame ~title:"Non-uniform recursion" (fun _ ->
    "{array [`L;`Vert;`L;`L] [
      array_line ~layout:[3,`L] ["<@Inductive PowerList (A:Type) : Type :=@>"];
      array_line ["";"<@zero@>";""];
      array_line ["";"<@tpo@>";"<@(a:A) (l:PowerList (A*A)).@>"];
    ]}
    {newline_size (`Mm 10.)}
    {array [`L;`L;`Vert;`L;`Sep (quad^^rightarrow_^^quad); `L] [
      (let a = color blue "<@A@>" in
       let b = color blue "<@B@>" in
       array_line ~layout:[4,`L] ["<@Fixpoint map @{a}@ @{b}@ (f:A->B) (l:PowerList A) : PowerList B :=@>"]);
      array_line ~layout:[(1,`L);(3,`L)] ["";"<@match l with@>"];
      array_line ["";"";"<@zero@>"; "<@zero@>"];
      (let aa = color blue "<@(A*A)@>" in
       let bb = color blue "<@(B*B)@>" in
       array_line ["";"";"<@tpo a l'@>"; "<@tpo (f a) (map @{aa}@ @{bb}@ (f×f) l')@>"]);
      array_line ~layout:[(1,`L);(3,`L)] ["";"<@end.@>"]
     ]}"
  )end;

  put (list[1]) begin frame ~title:"Alternation" (fun _ ->
    "<@Definition AlternatingPowerList (A B:Type) := A*PowerList (B*A)@>"
  )end;

  put (list[`Unmarked;`Marked;`Chunked]) begin frame ~title:"Four by four" (fun p ->
    let n = 15 in
    let leaf = Tree Leaf1 in
    let emptyp x = Pivot(x,empty) in
    let three_chunk mark = [leaf;emptyp mark;leaf] in
    let four_chunk mark = [emptyp false;leaf;emptyp mark;leaf] in
    let rec four_chunks n mark =
      if n<= 0 then []
      else four_chunk mark :: four_chunks (n-1) mark
    in
    let chunks n mark =
      three_chunk mark :: four_chunks ((n-3)/4) mark
    in
    let unmarked = Algo.pr_alt_list_gen (fun x -> x) (List.concat (chunks n false)) in
    let marked = Algo.pr_alt_list_gen (fun x -> x) (List.concat (chunks n true)) in
    let picify b = b |> Box.draw |> Picture.make |> Box.pic in
    let split =
      List.map (fun b-> Algo.pr_alt_list_gen (fun x -> x) b |> picify) (chunks n true) |>
      Box.hbox ~padding:(Num.cm 0.3)
    in
    center (mlpost begin
      match p with
      | `Unmarked -> Box.draw unmarked
      | `Marked -> Box.draw marked
      | `Chunked -> Box.draw split
      (* List.map picify [unmarked;marked;split] |> *)
      (* Box.vbox ~padding:(Num.cm 1.5) |> *)
      (* Box.draw *)
    end )
  )end;

  put (list[1]) begin frame ~title:"Main loop" (fun _ ->
    let hsp = `Mm 10. in
    "{array [`L;`L;`Vert;`L;`Sep (quad^^rightarrow_^^quad); `L] [
      array_line ~layout:[4,`L] ["<@Definition pass l :=@>"];
      array_line ~layout:[(1,`L);(3,`L)] ["";"<@match l with@>"];
      array_line ["";"";"<@(a,zero)@>";"<@(a,zero)@>"];
      array_line ["";"";"<@(a,tpo (x,b) q)@>";"<@(node a x b,map join q)@>"];
    ]}
    {newline_size hsp}
    {quad}{color blue "<@q : ((A*Tree A)*(A*Tree A)) PowerList@>"}
    (* {newline_size hsp} *)
    (* <@Definition join xayb := let '((x,a),(y,b)) := xayb in (x , node a y b)@> *)
    {newline_size (`Mm (-3.)) }
    { let vx = "<@x@>" and vy = "<@y@>" in
      let va = "<@a@>" and vb = "<@b@>" in
      let thelist x = [
        Pivot(false,vx);
        Tree (Node (Leaf,va,Leaf));
        Pivot (x,vy);
        Tree (Node (Leaf,vb,Leaf));
      ] in
      let mkbox x =Algo.pr_alt_list_gen (fun x -> x) (thelist x) in
      let thelist' = [
        Pivot(false,vx);
        Tree begin
          Node (
            Node(Leaf,va,Leaf),
            vy,
            Node(Leaf,vb,Leaf)
          )
        end
      ] in
      let box' = Algo.pr_alt_list_gen (fun x -> x) thelist' in
      let rwest b = Box.(west (nth 0 b)) in
      let reast b = Box.(east (nth 0 b)) in
      center (mlpost begin
        let left = mkbox false in
        let right = mkbox true in
        let both = Box.hbox ~padding:(Num.cm 1.) ~pos:`Bottom [left;right;box'] in
        let left = Box.sub left both in
        let right = Box.sub right both in
        let box' = Box.sub box' both in
        let arrow1 = Arrow.point_to_point (reast left) (rwest right) in
        let arrow2 =
          Arrow.point_to_point ~tex:(Latex.to_string"<@join@>") ~anchor:`Top
            (reast right) (rwest box')
        in
        Command.( Box.draw both ++ arrow1 ++ arrow2 )
      end)}
    "
  )end;

  put (list[1]) begin frame ~title:"Full trees" (fun _ ->
    let thin = text\"\\\\,\" in
    "{array [`L;`Vert;`L;`Sep(${thin}:{thin}$);`L] [
      array_line ~layout:[3,`L] ["<@Inductive FullTree (A:Type) : nat -> Type :=@>"];
      array_line ["";"<@Leaf₀@>";"<@FullTree A 0@>"];
      array_line ["";"<@Leaf₁@>";"<@FullTree A 1@>"];
      array_line ["";"<@Node {k:nat}@>";"<@FullTree A k -> A -> FullTree A k -> FullTree A (S k)@>"];
    ]}"
  )end;

  put (list[1]) begin frame ~title:"But how do I make a power list?" (fun _ ->
    array [`L;`L] [
      array_line ["";"<@a::l : List A@>"];
      array_line [leadsto;"<@tpo a (?:PowerList (A*A))@>"];
      array_line [leadsto;"<@l':list (A*A)@> {longrightarrow_} elements of <@l@> grouped by two (with default if odd)"];
      array_line [leadsto;"<@x::l'' = l'@>"];
      array_line [leadsto;"<@tpo a (tpo x (?:PowerList ((A*A)*(A*A))))@>"];
      array_line ["";qquad^^command\"vdots\" [] A];
      array_line [leadsto;"<@: PowerList A@>"];
    ]
  )end;

  put (list[1]) begin frame ~title:"Learning how to count" (fun _ ->
    let decorate n = exponent (overline n) $2'$ in
    let b2 x =
      let put d n = n^^d in
      let rec b2 = function
      | 0                        -> empty
      | n when n mod 2 == 1      -> put $1$ (b2 ((n-1)/2))
      | n (*when n mod 2 == 0 *) -> put $2$ (b2 ((n-2)/2))
      in
      if x == 0 then decorate (phantom$0$ ^^ hspace (`Ex (-1.)) ^^cdot)
      else decorate (b2 x)
    in
    let line x =
      array_line [ b2 x ; $=$ ; ${latex_of_int x}$ ]
    in
    let rec lines n m =
      if n > m then []
      else line n :: lines (n+1) m
    in
    let examples n m =
      just_left `Brace (array [`R;`C;`L] (lines n m))
    in
    "Unique representation: base $2$, digits $\{1;2\}$
     {newline_size (`Mm 7.)}
     {qquad}{(examples 0 7)}"
  )end;

  put (list[1]) begin frame ~title:"Arithmetic" (fun _ ->
    let (mult2t,mult2) =
    "Eliminate the $0$ (multiply by $2$):",
     just_left `Brace (array [`L;`L;`L] [
       array_line [$0$ ; leadsto ; cdot];
       array_line [$x10$ ; leadsto ; $x02$];
       array_line [$x20$ ; leadsto ; $x12$];
      ])
     in
     let (succt,succ,succs1,succs2) =
     "Successor:",
     just_left `Brace (array [`L;`L;`L] [
       array_line [$s~{cdot}$ ; leadsto ; $1$];
       array_line [$s(x1)$ ; leadsto ; $x2$];
       array_line [$s(x2)$ ; leadsto ; $(s x)1$];
      ]),
     "Convert from Peano integer:", "amortised $O(n)$"
     in
     array [`L;`Sep(hspace(`Mm 12.));`L] [
       array_line [succt;mult2t];
       array_line [succ;mult2];
       array_line [succs1;empty];
       array_line [succs2;empty];
     ]
  )end;

  put (list[1]) begin frame ~title:"Yet another binary list datatype" (fun _ ->
    "{array [`L;`Vert;`L;`L] [
      array_line ~layout:[3,`L] ["<@Inductive BList' (A:Type) : Type :=@>"];
      array_line ["";"<@zero@>";""];
      array_line ["";"<@tpo@>";"<@(a:A) (l:BList (A*A)).@>"];
      array_line ["";"<@tpt@>";"<@(a b:A) (l:BList (A*A))@>"];
    ]}
    {newline_size (`Mm 15.)}
    With a bit of extra work: complete to a powerlist and complete the algorithm"
  )end;

  title_put (list [1]) begin title_frame (fun _ ->
    textbf (huge2 "There. I'm full!") (* ^^ newline_size (`Mm 6.) *)
    (* ^^ large3"(Be reassured: I'm done)" *)
  )end;
])


let file = \"navesspiwack.tex\"

let _ = emit ~file 
             (Slides.document ~prelude ~packages doc)
  (* arnaud: rafiner les modes plus tard *)

let _ =
  let s = Metapost_tool.read_prelude_from_tex_file file  in
  Defaults.set_prelude s

let _ =
  Defaults.set_required_files [
    \"style.tex\"
  ]

let _ = match Arg.mode with
	 | `Cairo -> Cairost.dump_pdf ()
	 | `Mps -> Mps.dump ()
	 | _ -> assert false