SATySFiで文書作ったときに思ったこととか

これはSATySFi Advent Calendar 2020の十六日目の記事です．昨日は@zr_tex8rさんの「SATySFiの「最短コード」」でした．明日はmonaqaさんの予定です．

最近それなりに長い文書（100ページほど）をSATySFiで書いているのですが，そのときに必要になってやったものを適当に書いてみようと思います．だらだら書いている記事です．

クラスファイル

jlreq for SATySFiを使っています．ライブラリの方でもっと抽象化を進めたいのですが，まだまだなので中身をいじくりつつ使っています．

定理環境とか

jlreq for SATySFiの中に用意しておいたので，それ．こんな感じで+thmが定義できます．

let-mutable thm-counter <- 0
let-block ctx +thm = JLReqTheorem.theorem-scheme JLReqTheorem.default-config-theorem {定理} thm-counter ctx

節とかない文書なので，定理番号は全て通し．こんな感じで使う環境にしている．

+thm<
  +p{
    あれこれが成り立つ．
  }
>

実装はjlreq for SATySFi内にあるけど，可変参照利用．+thm内では「定理」とかの見出しを変数に入れて，+pはその変数をチェックして空じゃなければ段落頭に出力するように．

証明環境はjlreq for SATySFiには入れていない．頭にでる「証明」の文字は最初と同じ．最後に証明終了マークを入れているけれど，当初手動で書いていたのだがたまに忘れてしまう．Slackで相談したら「それ相互参照でできるよ」と賢いこと言われた．大体こんな感じ．

let-mutable proof-counter <- 0
let-mutable number-of-paragraph-in-proof <- -1
let-mutable paragraph-counter <- 0

let-block ctx +proof inner =
  let () = proof-counter <- !proof-counter + 1 in
  let ref-key = `number-of-paragraph-in-proof` ^ (arabic !proof-counter) in
  let ib = (read-inline ctx {証明}) ++ (inline-skip 10pt) in
  let () = JLReqParagraph.set-paragraph-top-text ib in
  let () = number-of-paragraph-in-proof <- (
    match get-cross-reference ref-key with
      | None -> 1
      | Some(s) -> (match Int.of-string-opt s with
        | None -> 1
        | Some(n) -> n
      )
    )
  in
  let () = paragraph-counter <- 0 in
  let bb = (read-block ctx inner) in
  let () = register-cross-reference ref-key (arabic !paragraph-counter) in
  let () = number-of-paragraph-in-proof <- -1 in
  bb

let qedsymbol ctx =
  let ib = read-inline ctx {阿} in
  let (aw,h,d) = get-natural-metrics ib in
  let w = aw *' 0.6 in
  let xshift = 3pt in
  inline-fil ++ 
  (
    inline-graphics (w +' xshift) h d (fun (x,y) ->
      [
        stroke 0.5pt Color.black 
          (start-path (x +' xshift, y -' d) 
            |> line-to (x +' xshift +' w, y -' d)
            |> line-to (x +' xshift +' w, y +' h)
            |> line-to (x +' xshift, y +' h)
            |> close-with-line
          );
      ]
    )
  )

let-block ctx +p it =
  let bb = 
    (JLReqParagraph.get-paragraph-boxes (| indent = Length(10pt);|) ctx it) ++ (
      if !number-of-paragraph-in-proof >= 0 then
        let () = paragraph-counter <- !paragraph-counter + 1 in
        if !number-of-paragraph-in-proof == !paragraph-counter then
          qedsymbol ctx
        else inline-nil
      else inline-nil
    )
  in
  line-break true true ctx bb

JLReq***みたいなのはjlreq for SATySFi内で定義されているやつです．+proof内の+pで変数paragraph-counterを一つずつ増やしていって，+proofの最後でそれをいったん保存．二回目でその回数を取り出して+proof内の最後の+pを特定しています．特定しちゃえば後は適当なマークを出すだけ．白四角をグラフィックで書いて出力しています．

マージン

定理環境にせよ証明環境にせよ，前後に空きを入れています．最初はこんな感じにしていました．

let-block +proof bt =
...
let bb = <構築したblock-boxes>
(block-skip 10pt) +++ bb +++ (block-skip 10pt)

しかしこれだと，定理環境と証明環境が続いた時に（もちろんすげーよくある）でかめの空きが来てしまいます．そこで，途中でblock-skipで入れるのではなくcontextに入っているマージンを使うことにしました．マージンは二つ続いた時に大きい方のみ有効になるという性質があります．これならば，定理環境と証明環境が続いても片方のマージンのみが効いてきてでかめの空きが現れることはありません．しかし，試してみると思ったより空きがでかい．定理環境の中にある+pのマージンが効いているようです．これを消すために，定理環境の中身の前後に馬鹿でかいマージンを入れて，それを差し引くblock-skipを入れることにしました．こうすれば，中身の+pから来るマージンはこのでかいマージンによって消されます．（マージンが続くと大きい方のみが有効なのでした．）具体的には次のようにしました．

let set-margin ctx before-breakable after-breakable before-margin after-margin inner =
  let large-skip = 1000000pt in
  let inline-bb = inline-graphics 10pt 10pt 10pt (fun pt -> []) in
  let dummy-txt = line-break false false (set-paragraph-margin 0pt 0pt ctx) (inline-bb ++ inline-fil) in
  let dummy-len = get-natural-length (dummy-txt +++ dummy-txt) in
  (line-break before-breakable false (set-paragraph-margin before-margin large-skip ctx) (inline-bb ++ inline-fil)) +++
  (block-skip (0pt -' (large-skip *' 2.0) -' dummy-len)) +++
  (line-break false false (set-paragraph-margin 0pt large-skip ctx) (inline-bb ++ inline-fil)) +++
  inner +++
  (line-break false false (set-paragraph-margin large-skip 0pt ctx) (inline-bb ++ inline-fil)) +++
  (block-skip (0pt -' (large-skip *' 2.0) -' dummy-len)) +++
  (line-break false after-breakable (set-paragraph-margin large-skip after-margin ctx) (inline-bb ++ inline-fil))

set-margin <context> <前で改行可能か> <後ろで改行可能か> <前マージン> <後マージン> <中身block-boxes>で使い，<中身block-boxes>の前後を指定されたマージンに設定し直して出力します．

AZmath

AZmathパッケージが現れました．便利なので使うことにしています．次の点がお気に入りです．

• \alignの書式が\eqnの書式に近く，使うときにあまり悩まずにすみます．具体的には，\eqnが

  \eqn(${<数式中身>});

  であるのに対して，\alignは

  \align(${
    | <式1> | = <式2>
    | | = <式3>
  |});
  

  です．縦棒が式の区切りなんだと覚えておけば後は同じです．デフォルトだと数式番号がでますが殆どつけないので，

  let-inline \align m = {\align?:(AZMathEquation.notag) (m);}

  として抑制しています．これだと\labelがついた数式のみ番号がつくようです．引用しない数式に番号をふるのはちょっとなぁと思うので，ありがたい仕様です．
• 括弧{}が「普通」でよいです．SATySFiの{}はなかなかくせがあって，また場合分けの時は数式と重なっちゃったりするという実用上の問題もあったりします．ちょっと括弧の命令が変わったりしています．\parenが\pになっていて，かなり攻めているなぁという気分．他の括弧はドキュメントの12ページとかをご覧ください．

その他数式について

\Homとかを定義しないとならないのはLaTeXと同じです．

let-math \Hom = math-char MathOp `Hom`

チルダは（AZmathにもありますが必要になったときにAZmathがまだなかったので）適当にグラフィックスでつくりました．上線も適当に．

let-math \tilde it =
  let make ctx =
    let ib = read-inline ctx {${#it}} in
    let (w,h,d) = get-natural-metrics ib in
    let xshift = 1.5pt in
    let ht = h *' 0.3 in
    let draw (xx,yy) = 
      let (x,y) = (xx +' xshift -' w,yy +' h) in
      [
        stroke 0.5pt Color.black (start-path (x,y +' ht *' 0.7)
          |> bezier-to (x +' w *' 0.1,y +' ht *' 1.5) (x +' (w *' 0.4),y +' ht *'1.5) (x +' (w *' 0.5),y +' ht)
          |> bezier-to (x +' (w *' 0.6),y +' ht *' 0.5) (x +' w *' 0.9,y +' ht *' 0.5) (x +' w,y +' ht *' 1.3)
          |> terminate-path
        )]
    in
    ib ++ (inline-graphics 0pt 0pt 0pt draw)
  in
  text-in-math MathOrd make 

let-math \overline x = 
  let pads = (0pt,2pt,2pt,0pt) in
  let line (x,y) w h d = [
    stroke 0.5pt Color.black (Gr.line (x,y +' h) (x +' w, y +' h))
  ] in
  let make ctx =
    let ib = read-inline ctx {${#x}} in
    inline-frame-inner pads line ib
  in
  text-in-math MathInner make

\xrightarrowも作りました．satysfi-matrixcdでもできるのですが，面倒なので．矢印の形を\toのそれと同じくするために，\toに線をひっつける形で作りました．各種値は手動調整です．フォント変わったら破綻しそう．

let-math \xrightarrow lab = 
  let make ctx =
    let font-size = get-font-size ctx in
    let ib = read-inline (set-font-size (font-size *' 0.75) ctx) {${#lab}} in
    let ab = read-inline ctx {${\to}} in
    let (w,h,d) = get-natural-metrics ib in
    let (aw,ah,ad) = get-natural-metrics ab in
    let shift = 2.75pt in
    inline-graphics (w +' aw) ah ad (fun (x,y) ->[
      (stroke 0.45pt Color.black (Gr.line (x,y +' shift) (x +' w, y +' shift)));
      (draw-text (x +' w -' 1pt,y) ab);
      (draw-text (x +' aw *' 0.5 -' 2pt,y +' shift +' (d *' 2.0) +' 1pt) ib);
    ])
  in
  text-in-math MathInner make

enumitemi

箇条書きをいじくれるenumitemを使っています．デフォルトでは箇条書き中の改ページができなかったのでいじりました．

let enumitem-itemf ctx depth ib-label text = 
  let text-indent = (get-font-size ctx) *' ((EnumitemParam.get Enumitem.item-indent-ratio)*. (float depth)) in
  let decos = 
    let deco _ _ _ _ = [] in
    (deco,deco,deco,deco)
  in
  let index-width = get-natural-width ib-label in
  let pads = (text-indent +' index-width,0pt,0pt,0pt) in
  let ib = 
    let item-text-width = (get-text-width ctx) -' text-indent -' index-width in
    block-frame-breakable ctx pads decos (fun c ->
      line-break true true c (
        (inline-skip (index-width *' (0.0 -. 1.0))) ++
        ib-label ++ 
        (read-inline ctx text) ++
        inline-fil
      )
    )
  in
  ib

let-block ctx +enumerate ?:labelf item =
  let label = Option.from Enumitem.paren-arabic labelf in
  read-block ctx '<+genlisting(label)(enumitem-itemf)(item);>

let-inline ctx \enumerate ?:labelf item =
  let label = Option.from Enumitem.paren-arabic labelf in
  read-inline ctx {\listing-from-block<+enumerate?:(label)(item);>}

遅い

LaTeXに比べて遅いなぁという印象です．エラーが出るときは（組む前に出るので）早いけど．手元の現在93ページのをコンパイルするとこんな感じ．相互参照解決済みなので1パスだけです．Surface Pro 7 + WSL2．

$ time satysfi a.saty
real    0m27.221s
user    0m26.850s
sys     0m0.220s