■

中目のブックセンターはマンガが多くてありがたいが、技術書が少ないのが不満。
西遊妖猿伝 西域編 4
夜の経済学

Imp_Jを読んだことにする。

証明がさっぱり歯が立たなくなってきた。そもそも何書いてあんのかまるで理解していない・・・

ImpParser_J

あんまりこのへんのことをやったことがない。ちゃんとした字句解析とかコンパイラとか。もちろん自分が「ちゃんとやったことある」分野など存在しないのだが。

(*
 cls : 直前の文字種
 acc: それまでの蓄積 ascii文字リスト
 xs : 解析対象文字列

-同じ種類の文字を読み込んだら accに貯めこんで次に行く。
-カッコ、空白、文字種変更があればそれまでの溜め込んだascii列を出力にpush
-空白は捨てる。
みたいな感じの関数かな。
*)
Fixpoint tokenize_helper (cls : chartype) (acc xs : list ascii)
                       : list (list ascii) :=
  let tk := match acc with [] => [] | _::_ => [rev acc] end in
  match xs with
  | [] => tk
  | (x::xs') =>
    match cls, classifyChar x, x with
    | _, _, "(" => tk ++ ["("]::(tokenize_helper other [] xs')
    | _, _, ")" => tk ++ [")"]::(tokenize_helper other [] xs')
    | _, white, _ => tk ++ (tokenize_helper white [] xs')
    | alpha,alpha,x => tokenize_helper alpha (x::acc) xs'
    | digit,digit,x => tokenize_helper digit (x::acc) xs'
    | other,other,x => tokenize_helper other (x::acc) xs'
    | _,tp,x => tk ++ (tokenize_helper tp [x] xs')
    end
  end %char.

最後の%char は、なんですの？

Definition ll : list (list ascii) := [].
Definition el : list ascii := ["a","b","c"] %char.

Eval simpl in  [el] ++ (["("] :: ll) %char.
(*  = el :: ["("%char] :: ll
     : list (list ascii)
*)
Eval compute in  [el] ++ (["("] :: ll) %char.
(*  = [["a"%char, "b"%char, "c"%char], ["("%char]]
     : list (list ascii)
*)

charactorリテラルがない？そいで文字列リテラルとを区別してる？
Manual見てもさっぱり。