From: Ferruccio Guidi Date: Mon, 3 Oct 2011 17:59:46 +0000 (+0000) Subject: - first version of xhtbl X-Git-Tag: make_still_working~2239 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2b58d92062882492dd024a1196b6f8b788ffe5c6;p=helm.git - first version of xhtbl - first version of ld_basic_2.html (generated) --- diff --git a/helm/www/lambda_delta/bin/a.ml b/helm/www/lambda_delta/bin/a.ml new file mode 100644 index 000000000..4f310c873 --- /dev/null +++ b/helm/www/lambda_delta/bin/a.ml @@ -0,0 +1,17 @@ +let f = "0123456789abcdef" + +let r, g, b = 1.0, 0.5, 0.0 + +let h = 1. /. 2. + +let mk_h x = x +. (1. -. x) *. h + +let rr, gg, bb = mk_h r, mk_h g, mk_h b + +let mk_f x = + let x = int_of_float x in + print_char f.[x / 16]; print_char f.[x mod 16] + +let _ = + mk_f (rr *. 255.); mk_f (gg *. 255.); mk_f (bb *. 255.); + print_newline () diff --git a/helm/www/lambda_delta/bin/xhtbl/Makefile b/helm/www/lambda_delta/bin/xhtbl/Makefile new file mode 100644 index 000000000..289c0cecd --- /dev/null +++ b/helm/www/lambda_delta/bin/xhtbl/Makefile @@ -0,0 +1,31 @@ +EXEC = xhtbl +VERSION=0.1.0 + +REQUIRES = str + +YACCFLAGS = -v + +include Makefile.common + +XSLT = xsltproc +XHTBL = ./xhtbl.native + +XSLS = xhtbl.xsl ld_basic_2.xsl +LDWEB = ld_web.xsl ld_web_root.xsl ld_web_library.xsl + +LDURL = http://lambda-delta.info/ +XSLDIR = ../../xslt/ +SRCDIR = ../../web/home/ +HOMEDIR = ../../ + +%.html: BASEURL = --stringparam baseurl $(LDURL) + +test: $(HOMEDIR)ld_basic_2.html + +$(XSLS:%=$(XSLDIR)%): $(SRCDIR)ld_basic_2.tbl $(XHTBL) + @echo " XHTBL $<" + $(H)$(XHTBL) -O $(XSLDIR) $< + +$(HOMEDIR)ld_basic_2.html: $(SRCDIR)ld_basic_2.ldw.xml $(XSLS:%=$(XSLDIR)%) $(LDWEB:%=$(XSLDIR)%) + @echo " XSLT $<" + $(H)$(XSLT) -o $@ $(BASEURL) $(XSLDIR)ld_web.xsl $< diff --git a/helm/www/lambda_delta/bin/xhtbl/Makefile.common b/helm/www/lambda_delta/bin/xhtbl/Makefile.common new file mode 100644 index 000000000..96c564336 --- /dev/null +++ b/helm/www/lambda_delta/bin/xhtbl/Makefile.common @@ -0,0 +1,27 @@ +H=@ + +include ../../../claudio/Makefile.defs + +DIST=$(EXEC)---$(VERSION) +DATE=$(shell date +%y%m%d) + +OCAMLOPTIONS = -linkpkg -thread -rectypes -package \"$(REQUIRES)\" +OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) +OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) + +all: $(EXEC).native + +$(EXEC).native: $(wildcard *.ml) $(wildcard *.mli) $(wildcard *.mly) $(wildcard *.mll) + @echo " OCAMLBUILD $(EXEC).native" + $(H)ocamlbuild -ocamlc "$(OCAMLC)" -ocamlopt "$(OCAMLOPT)" -yaccflags "$(YACCFLAGS)" $(EXEC).native + +clean: + ocamlbuild -clean + rm -rf $(DIST) $(DIST).tgz + +dist: + mkdir -p $(DIST)/Sources + cp ReadMe $(DIST) + cp *.ml *.mli *.mll *.mly Makefile _tags $(DIST)/Sources + cd $(DIST); ln -s Sources/$(EXEC).native $(EXEC) + tar -cvzf $(DIST).tgz $(DIST) diff --git a/helm/www/lambda_delta/bin/xhtbl/css.ml b/helm/www/lambda_delta/bin/xhtbl/css.ml new file mode 100644 index 000000000..82a41e91c --- /dev/null +++ b/helm/www/lambda_delta/bin/xhtbl/css.ml @@ -0,0 +1,20 @@ +module L = List + +module T = Table + +(* true for a row specification *) +type atom = T.css * bool * int option * int option + +type atoms = atom list + +let get_css a y x = + let map y x (c, b, x1, x2) = match b, x1, x2 with + | _ , None, None -> c + | false, None, Some c2 -> if x <= c2 then c else [] + | false, Some c1, None -> if x >= c1 then c else [] + | false, Some c1, Some c2 -> if x >= c1 && x <= c2 then c else [] + | true , None, Some r2 -> if y <= r2 then c else [] + | true , Some r1, None -> if y >= r1 then c else [] + | true , Some r1, Some r2 -> if y >= r1 && y <= r2 then c else [] + in + L.concat (L.map (map y x) a) diff --git a/helm/www/lambda_delta/bin/xhtbl/fold.ml b/helm/www/lambda_delta/bin/xhtbl/fold.ml new file mode 100644 index 000000000..752b06d77 --- /dev/null +++ b/helm/www/lambda_delta/bin/xhtbl/fold.ml @@ -0,0 +1,25 @@ +module T = Table + +type 'a fold_cb = { + open_table : 'a -> T.table -> 'a; + close_table: 'a -> T.table -> 'a; + map_key : 'a -> T.key -> 'a; + open_line : bool -> 'a -> 'a; + close_line : bool -> 'a -> 'a; + open_entry : bool -> 'a -> 'a; + close_entry: bool -> 'a -> 'a -> 'a; +} + +let map h g f a b = h a (g (f a) b) + +let rec fold_table cb a t = + let a = cb.open_table a t in + let a = fold_entry cb a t.T.te in + cb.close_table a t + +and fold_entry cb a = function + | T.Key k -> cb.map_key a k + | T.Line (r, ts) -> + let a = cb.open_line r a in + let a = List.fold_left (map (cb.close_entry r) (fold_table cb) (cb.open_entry r)) a ts in + cb.close_line r a diff --git a/helm/www/lambda_delta/bin/xhtbl/matrix.ml b/helm/www/lambda_delta/bin/xhtbl/matrix.ml new file mode 100644 index 000000000..9b3bb9443 --- /dev/null +++ b/helm/www/lambda_delta/bin/xhtbl/matrix.ml @@ -0,0 +1,52 @@ +module A = Array + +module T = Table + +type cell = { + ck: string; (* contents *) + cc: T.css; (* css classes *) + cb: T.border; (* border *) +} + +type matrix = { + r: int; (* rows *) + c: int; (* columns *) + m: cell array array; (* matrix *) +} + +let empty = { + ck = ""; cc = []; cb = T.border false; +} + +let make ts = { + r = ts.T.rf; c = ts.T.cf; + m = A.make_matrix ts.T.rf ts.T.cf empty; +} + +let set_key m y x k = + m.m.(y).(x) <- {m.m.(y).(x) with ck = k} + +let set_css m y x c = + m.m.(y).(x) <- {m.m.(y).(x) with cc = c @ m.m.(y).(x).cc} + +let set_west m y x b = + let c = m.m.(y).(x) in + let cb = {c.cb with T.w = c.cb.T.w || b.T.w} in + m.m.(y).(x) <- {c with cb = cb} + +let set_north m y x b = + let c = m.m.(y).(x) in + let cb = {c.cb with T.n = c.cb.T.n || b.T.n} in + m.m.(y).(x) <- {c with cb = cb} + +let set_east m y x b = + if x < pred m.c then set_west m y (succ x) {b with T.w = b.T.e} else + let c = m.m.(y).(x) in + let cb = {c.cb with T.e = c.cb.T.e || b.T.e} in + m.m.(y).(x) <- {c with cb = cb} + +let set_south m y x b = + if y < pred m.r then set_north m (succ y) x {b with T.n = b.T.s} else + let c = m.m.(y).(x) in + let cb = {c.cb with T.s = c.cb.T.s || b.T.s} in + m.m.(y).(x) <- {c with cb = cb} diff --git a/helm/www/lambda_delta/bin/xhtbl/options.ml b/helm/www/lambda_delta/bin/xhtbl/options.ml new file mode 100644 index 000000000..ce1c88867 --- /dev/null +++ b/helm/www/lambda_delta/bin/xhtbl/options.ml @@ -0,0 +1,34 @@ +let output_dir_default = "" + +let debug_lexer_default = false + +let debug_pass_default = false + +let pass_default = false + +let output_dir = ref output_dir_default + +let debug_lexer = ref debug_lexer_default + +let d0 = ref debug_pass_default + +let d1 = ref debug_pass_default + +let d2 = ref debug_pass_default + +let e1 = ref debug_pass_default + +let e2 = ref debug_pass_default + +let p0 = ref pass_default + +let p1 = ref pass_default + +let p2 = ref pass_default + +let clear () = + output_dir := output_dir_default; + debug_lexer := debug_lexer_default; + d0 := debug_pass_default; d1 := debug_pass_default; d2 := debug_pass_default; + e1 := debug_pass_default; e2 := debug_pass_default; + p0 := pass_default; p1 := pass_default; p2 := pass_default diff --git a/helm/www/lambda_delta/bin/xhtbl/pass1.ml b/helm/www/lambda_delta/bin/xhtbl/pass1.ml new file mode 100644 index 000000000..1c53e7d6f --- /dev/null +++ b/helm/www/lambda_delta/bin/xhtbl/pass1.ml @@ -0,0 +1,86 @@ +module L = List + +module T = Table +module F = Fold + +type status = { + ts: T.size; (* current dimensions *) + tc: T.css; (* current class *) +} + +let empty = { + ts = T.no_size; tc = []; +} + +let init b ts = + if b then + {ts with T.ri = max_int; T.ci = 0} + else + {ts with T.ri = 0; T.ci = max_int} + +let combine b ts1 ts2 = + if b then + {ts1 with + T.rf = max ts1.T.rf ts2.T.rf; T.ri = min ts1.T.ri ts2.T.ri; + T.cf = ts1.T.cf + ts2.T.cf; T.ci = ts1.T.ci + ts2.T.ci; + } + else + {ts1 with + T.cf = max ts1.T.cf ts2.T.cf; T.ci = min ts1.T.ci ts2.T.ci; + T.rf = ts1.T.rf + ts2.T.rf; T.ri = ts1.T.ri + ts2.T.ri; + } + +let deinit ts = {ts with + T.ri = if ts.T.ri = max_int then 0 else ts.T.ri; + T.ci = if ts.T.ci = max_int then 0 else ts.T.ci; +} + +(****************************************************************************) + +let open_table st t = + t.T.tc <- t.T.tc @ st.tc; + {st with tc = t.T.tc} + +let close_table st t = + t.T.ts <- st.ts; st + +let map_key st k = + let ts = match k, st.ts.T.p with + | T.Text _ , _ -> + {st.ts with T.rf = 1; T.cf = 1; T.ri = 0; T.ci = 0} + | T.Glue None , _ -> + {st.ts with T.rf = 0; T.cf = 0; T.ri = 1; T.ci = 1} + | T.Glue Some g, Some false -> + {st.ts with T.rf = g; T.cf = 0; T.ri = 0; T.ci = 1} + | T.Glue Some g, Some true -> + {st.ts with T.rf = 0; T.cf = g; T.ri = 1; T.ci = 0} + | T.Glue Some g, None -> + {st.ts with T.rf = g; T.cf = g; T.ri = 0; T.ci = 0} + in + {st with ts = ts} + +let open_line b st = + let ts = init b st.ts in + let ts = {ts with T.rf = 0; T.cf = 0} in + {st with ts = ts} + +let open_entry b st = + let ts = {st.ts with T.p = Some b} in + {st with ts = ts} + +let close_entry b st sst = + {st with ts = combine b st.ts sst.ts} + +let close_line b st = + {st with ts = deinit st.ts} + +let cb = { + F.open_table = open_table; F.close_table = close_table; + F.open_line = open_line; F.close_line = close_line; + F.open_entry = open_entry; F.close_entry = close_entry; + F.map_key = map_key; +} + +let process t = + let st = F.fold_table cb empty t in + st.ts diff --git a/helm/www/lambda_delta/bin/xhtbl/pass2.ml b/helm/www/lambda_delta/bin/xhtbl/pass2.ml new file mode 100644 index 000000000..8ec358123 --- /dev/null +++ b/helm/www/lambda_delta/bin/xhtbl/pass2.ml @@ -0,0 +1,139 @@ +module O = Options +module T = Table +module M = Matrix +module F = Fold + +type status = { + ts: T.size; (* current dimensions *) + tm: M.matrix; (* current matrix *) +} + +let initial t m = { + ts = {t.T.ts with T.ri = 0; T.ci = 0}; + tm = m; +} + +let resize b sts tts = + if b then begin (* parent is a row *) + if tts.T.rf < sts.T.rf && tts.T.ri = 0 then + failwith "underful column"; + {tts with T.rf = sts.T.rf; T.cf = tts.T.cf + sts.T.ci * tts.T.ci} + end else begin (* parent is a column *) + if tts.T.cf < sts.T.cf && tts.T.ci = 0 then + failwith "underful row"; + {tts with T.cf = sts.T.cf; T.rf = tts.T.rf + sts.T.ri * tts.T.ri} + end + +let fill b sts tts = + if b then (* parent is a row *) + {sts with T.ri = + let rf, ri = sts.T.rf - tts.T.rf, tts.T.ri in + if ri = 0 then 0 else + if rf mod ri = 0 then rf / ri else + failwith "fracted column" + } + else (* parent is a column *) + {sts with T.ci = + let cf, ci = sts.T.cf - tts.T.cf, tts.T.ci in + if ci = 0 then 0 else + if cf mod ci = 0 then cf / ci else + failwith "fracted row" + } + +let place b sts tts = + if b then (* parent is a row *) + {sts with T.x = sts.T.x + tts.T.cf} + else (* parent is a column *) + {sts with T.y = sts.T.y + tts.T.rf} + +let set_key st t = match t.T.te with + | T.Key (T.Text s) -> M.set_key st.tm t.T.ts.T.y t.T.ts.T.x s + | _ -> () + +let set_css st t = + let rec aux y x = + if y >= t.T.ts.T.rf then () else + if x >= t.T.ts.T.cf then aux (succ y) 0 else begin + M.set_css st.tm (t.T.ts.T.y + y) (t.T.ts.T.x + x) t.T.tc; + aux y (succ x) + end + in + match t.T.te with + | T.Key _ -> aux 0 0 + | _ -> () + +let set_borders st t = + let rec aux_we y = + if y >= t.T.ts.T.rf then () else begin + M.set_west st.tm (t.T.ts.T.y + y) t.T.ts.T.x t.T.tb; + if t.T.ts.T.cf > 0 then + M.set_east st.tm (t.T.ts.T.y + y) (t.T.ts.T.x + pred t.T.ts.T.cf) t.T.tb; + aux_we (succ y) + end + in + let rec aux_ns x = + if x >= t.T.ts.T.cf then () else begin + M.set_north st.tm t.T.ts.T.y (t.T.ts.T.x + x) t.T.tb; + if t.T.ts.T.rf > 0 then + M.set_south st.tm (t.T.ts.T.y + pred t.T.ts.T.rf) (t.T.ts.T.x + x) t.T.tb; + aux_ns (succ x) + end + in + match t.T.te with + | T.Line (true, _) -> aux_we 0; aux_ns 0 + | _ -> () + +let print st t = + if !O.e2 then + Printf.printf "#%u: (%u+%u, %u+%u) - (%u+%u, %u+%u)\n" + t.T.ti + t.T.ts.T.rf t.T.ts.T.ri + t.T.ts.T.cf t.T.ts.T.ci + st.ts.T.rf st.ts.T.ri + st.ts.T.cf st.ts.T.ci + +(****************************************************************************) + +let open_table st t = + print st t; + let ts = match t.T.ts.T.p with + | None -> + let ts = fill false st.ts t.T.ts in + let ts = fill true ts t.T.ts in + t.T.ts <- resize false st.ts t.T.ts; + t.T.ts <- resize true st.ts t.T.ts; + ts + | Some b -> + let ts = fill b st.ts t.T.ts in + t.T.ts <- resize b st.ts t.T.ts; + ts + in + t.T.ts <- {t.T.ts with T.ri = 0; T.ci = 0; T.x = st.ts.T.x; T.y = st.ts.T.y}; + let ts = {ts with T.rf = t.T.ts.T.rf; T.cf = t.T.ts.T.cf} in + let st = {st with ts = ts} in + print st t; st + +let close_table st t = + set_key st t; set_css st t; set_borders st t; st + +let map_key st k = st + +let open_line b st = st + +let open_entry b st = st + +let close_entry b st sst = + let ts = place b st.ts sst.ts in + {st with ts = ts} + +let close_line b st = st + +let cb = { + F.open_table = open_table; F.close_table = close_table; + F.open_line = open_line; F.close_line = close_line; + F.open_entry = open_entry; F.close_entry = close_entry; + F.map_key = map_key; +} + +let process t m = + let _ = F.fold_table cb (initial t m) t in () diff --git a/helm/www/lambda_delta/bin/xhtbl/pass3.ml b/helm/www/lambda_delta/bin/xhtbl/pass3.ml new file mode 100644 index 000000000..4513828b5 --- /dev/null +++ b/helm/www/lambda_delta/bin/xhtbl/pass3.ml @@ -0,0 +1,23 @@ +module A = Array + +module M = Matrix +module C = Css + +type status = { + m: M.matrix; + a: C.atoms; +} + +let initial a m = { + m = m; a = a; +} + +let process_cell st y x c = + M.set_css st.m y x (C.get_css st.a y x) + +let process_row st y row = + A.iteri (process_cell st y) row + +let process css matrix = + let st = initial css matrix in + A.iteri (process_row st) matrix.M.m diff --git a/helm/www/lambda_delta/bin/xhtbl/table.ml b/helm/www/lambda_delta/bin/xhtbl/table.ml new file mode 100644 index 000000000..a7fdf19fa --- /dev/null +++ b/helm/www/lambda_delta/bin/xhtbl/table.ml @@ -0,0 +1,54 @@ +type css = string list + +type size = { + y : int; (* first row *) + x : int; (* first column *) + rf: int; (* finite rows *) + cf: int; (* finite columns *) + ri: int; (* infinite rows *) + ci: int; (* infinite columns *) + p : bool option; (* parent kind *) +} + +type border = { + n: bool; (* north *) + s: bool; (* south *) + e: bool; (* east *) + w: bool; (* west *) +} + +type key = Text of string + | Glue of int option + +type table = { + mutable tc: css; (* css classes *) + mutable ts: size; (* dimension *) + tb: border; (* border *) + te: entry; (* contents *) + ti: int; (* table identifier *) +} + +and entry = Key of key + | Line of bool * table list (* true for a row *) + +let id = + let current = ref 0 in + fun () -> incr current; !current + +let no_size = { + y = 0; x = 0; rf = 0; cf = 0; ri = 0; ci = 0; p = None; +} + +let border b = { + n = b; s = b; e = b; w = b; +} + +let mk_key k tc = { + ts = no_size; tb = border false; te = Key k; tc = tc; + ti = id (); +} + +let mk_line b tl tc = { + ts = no_size; tb = border b; te = Line (b, tl); tc = tc; + ti = id (); +} diff --git a/helm/www/lambda_delta/bin/xhtbl/textLexer.mll b/helm/www/lambda_delta/bin/xhtbl/textLexer.mll new file mode 100644 index 000000000..f1ea9a61a --- /dev/null +++ b/helm/www/lambda_delta/bin/xhtbl/textLexer.mll @@ -0,0 +1,28 @@ +{ + module S = String + module O = Options + module TP = TextParser + + let trim s = S.sub s 1 (S.length s - 2) + + let out s = if !O.debug_lexer then prerr_endline s +} + +let SPC = ['\r' '\n' '\t' ' ']+ +let QT = '"' +let STR = QT [^'"']* QT +let NUM = ['0'-'9']+ + +rule token = parse + | SPC { token lexbuf } + | STR as s { out s; TP.TEXT (trim s) } + | NUM as s { out s; TP.NUM (int_of_string s) } + | "{" { out "{"; TP.OC } + | "}" { out "}"; TP.CC } + | "[" { out "["; TP.OB } + | "]" { out "]"; TP.CB } + | "*" { out "*"; TP.SR } + | "name" { out "name"; TP.NAME } + | "table" { out "table"; TP.TABLE } + | "class" { out "class"; TP.CSS } + | eof { TP.EOF } diff --git a/helm/www/lambda_delta/bin/xhtbl/textParser.mly b/helm/www/lambda_delta/bin/xhtbl/textParser.mly new file mode 100644 index 000000000..6be439813 --- /dev/null +++ b/helm/www/lambda_delta/bin/xhtbl/textParser.mly @@ -0,0 +1,87 @@ +%{ + +module S = Str +module L = List +module T = Table + +let split s = + S.split (S.regexp "[ \r\n\t]+") s + +let mk_atom s rs = + let map c (b, (x1, x2)) = c, b, x1, x2 in + L.map (map (split s)) rs + +%} + +%token NUM +%token TEXT +%token NAME TABLE CSS SR OC CC OB CB EOF + +%start script +%type <(string * Table.table * Css.atoms) list> script + +%% + +key: + | TEXT { T.Text $1 } + | SR { T.Glue None } + | NUM { T.Glue (Some $1) } +; + +css: + | { [] } + | CSS TEXT { split $2 } +; + +table: + | css key { T.mk_key $2 $1 } + | css OC tables CC { T.mk_line false $3 $1 } + | css OB tables CB { T.mk_line true $3 $1 } +; + +tables: + | { [] } + | table tables { $1 :: $2 } +; + +name: + | { "" } + | NAME TEXT { $2 } +; + +interval: + | NUM { Some $1, Some $1 } + | SR { None, None } + | NUM NUM { Some $1, Some $2 } + | NUM SR { Some $1, None } + | SR NUM { None, Some $2 } + | SR SR { None, None } +; + +range: + | OB interval CB { true, $2 } + | OC interval CC { false, $2 } +; + +ranges: + | { [] } + | range ranges { $1 :: $2 } +; + +atom: + | CSS TEXT ranges { mk_atom $2 $3 } +; + +atoms: + | { [] } + | atom atoms { $1 @ $2 } +; + +directive: + | name TABLE table atoms { $1, $3, $4 } +; + +script: + | EOF { [] } + | directive script { $1 :: $2 } +; diff --git a/helm/www/lambda_delta/bin/xhtbl/textUnparser.ml b/helm/www/lambda_delta/bin/xhtbl/textUnparser.ml new file mode 100644 index 000000000..969713aac --- /dev/null +++ b/helm/www/lambda_delta/bin/xhtbl/textUnparser.ml @@ -0,0 +1,88 @@ +module P = Printf +module S = String + +module T = Table +module F = Fold + +type status = { + i: int; (* indentation *) + out: string -> unit; (* output function *) +} + +let home = { + i = 0; out = print_string +} + +let indent st = + S.make st.i ' ' + +let add st = {st with i = st.i + 3} + +let sub st = {st with i = st.i - 3} + +let parent = function + | None -> "key" + | Some false -> "col" + | Some true -> "row" + +let size ts = + P.sprintf "(%u, %u); (%u+%u, %u+%u); %s" + ts.T.y ts.T.x ts.T.rf ts.T.ri ts.T.cf ts.T.ci (parent ts.T.p) + +let border tb = + let str = S.make 4 ' ' in + if tb.T.w then str.[0] <- 'W'; + if tb.T.n then str.[1] <- 'N'; + if tb.T.e then str.[2] <- 'E'; + if tb.T.s then str.[3] <- 'S'; + str + +let css tc = + P.sprintf "\"%s\"" (S.concat " " tc) + +let key = function + | T.Text s -> P.sprintf "\"%s\"" s + | T.Glue None -> "*" + | T.Glue (Some i) -> P.sprintf "%u" i + +let entry = function + | false -> "column" + | true -> "row" + +(****************************************************************************) + +let open_table st t = + let str = + P.sprintf "%s[{#%u: %s; %s; %s}\n" + (indent st) t.T.ti (size t.T.ts) (border t.T.tb) (css t.T.tc) + in + st.out str; add st + +let close_table st t = + let st = sub st in + let str = P.sprintf "%s]\n" (indent st) in + st.out str; st + +let map_key st k = + let str = P.sprintf "%s%s\n" (indent st) (key k) in + st.out str; st + +let open_line b st = + let str = P.sprintf "%s%s\n" (indent st) (entry b) in + st.out str; st + +let close_line b st = st + +let open_entry b st = st + +let close_entry b st sst = st + +let cb = { + F.open_table = open_table; F.close_table = close_table; + F.open_line = open_line; F.close_line = close_line; + F.open_entry = open_entry; F.close_entry = close_entry; + F.map_key = map_key; +} + +let debug t = + let _ = F.fold_table cb home t in () diff --git a/helm/www/lambda_delta/bin/xhtbl/xhtbl.ml b/helm/www/lambda_delta/bin/xhtbl/xhtbl.ml new file mode 100644 index 000000000..cf4d818b6 --- /dev/null +++ b/helm/www/lambda_delta/bin/xhtbl/xhtbl.ml @@ -0,0 +1,76 @@ +module A = Arg +module F = Filename +module L = List + +module O = Options +module TP = TextParser +module TL = TextLexer +module TU = TextUnparser +module P1 = Pass1 +module P2 = Pass2 +module P3 = Pass3 +module M = Matrix +module XU = XmlUnparser + +let help = "" +let help_L = "" +let help_O = "" +let help_X = "" +let help_d0 = "" +let help_d1 = "" +let help_d2 = "" +let help_e1 = "" +let help_e2 = "" +let help_p0 = "" +let help_p1 = "" +let help_p2 = "" + +let hook = "xhtbl" + +let includes, tables = ref [], ref [] + +let set_output_dir s = O.output_dir := s + +let process_directive och bname (name, table, css) = + tables := name :: !tables; + if !O.d0 then TU.debug table; + if not !O.p0 then begin + let size = P1.process table in + if !O.d1 then TU.debug table; + if not !O.p1 then begin + let matrix = M.make size in + let _ = P2.process table matrix in + if !O.d2 then TU.debug table; + if not !O.p2 then P3.process css matrix; + let name = if name = "" then bname else name in + XU.output och name matrix + end + end + +let process_file fname = + let bname = F.chop_extension (F.basename fname) in + let ich = open_in fname in + let lexbuf = Lexing.from_channel ich in + let ds = TP.script TL.token lexbuf in + close_in ich; includes := bname :: !includes; + let och = XU.open_out true bname in + L.iter (process_directive och bname) ds; + XU.close_out och + +let main () = + A.parse [ + "-L", A.Set O.debug_lexer, help_L; + "-O", A.String set_output_dir, help_O; + "-X", A.Unit O.clear, help_X; + "-d0", A.Set O.d0, help_d0; + "-d1", A.Set O.d1, help_d1; + "-d2", A.Set O.d2, help_d2; + "-e1", A.Set O.e1, help_e1; + "-e2", A.Set O.e2, help_e2; + "-p0", A.Set O.p0, help_p0; + "-p1", A.Set O.p1, help_p1; + "-p2", A.Set O.p2, help_p2; + ] process_file help; + XU.write_hook hook !includes !tables + +let _ = main () diff --git a/helm/www/lambda_delta/bin/xhtbl/xmlUnparser.ml b/helm/www/lambda_delta/bin/xhtbl/xmlUnparser.ml new file mode 100644 index 000000000..17f24671c --- /dev/null +++ b/helm/www/lambda_delta/bin/xhtbl/xmlUnparser.ml @@ -0,0 +1,82 @@ +module A = Array +module F = Filename +module L = List +module P = Printf +module S = String + +module O = Options +module T = Table +module M = Matrix + +let i = 0 + +let myself = F.basename (Sys.argv.(0)) + +let msg = P.sprintf "This file was generated by %s, do not edit" myself + +let border cell = + let str = S.make 4 'n' in + if cell.M.cb.T.n then str.[0] <- 's'; + if cell.M.cb.T.e then str.[1] <- 's'; + if cell.M.cb.T.s then str.[2] <- 's'; + if cell.M.cb.T.w then str.[3] <- 's'; + str :: cell.M.cc + +let key cell = + if cell.M.ck = "" then "
" else cell.M.ck + +let ind i = S.make (2 * i) ' ' + +let out_cell och cell = + let cc = border cell in + P.fprintf och "%s%s\n" + (ind (i+4)) (S.concat " " cc) (key cell) + +let out_row och row = + P.fprintf och "%s\n" (ind (i+3)); + A.iter (out_cell och) row; + P.fprintf och "%s\n" (ind (i+3)) + +(****************************************************************************) + +let open_out html name = + let fname = F.concat !O.output_dir (P.sprintf "%s.xsl" name) in + let och = open_out fname in + P.fprintf och "\n\n"; + P.fprintf och "\n\n" msg; + P.fprintf och "\n\n"; + och + +let output och name matrix = + P.fprintf och "\n" name; + P.fprintf och "%s\n" (ind (i+1)); + P.fprintf och "%s\n" (ind (i+2)); + A.iter (out_row och) matrix.M.m; + P.fprintf och "%s\n" (ind (i+2)); + P.fprintf och "%s
\n" (ind (i+1)); + P.fprintf och "\n\n" + +let close_out och = + P.fprintf och "\n"; + close_out och + +let map_incs och name = + P.fprintf och "\n" name + +let map_tbls och name = + P.fprintf och "%s\n" (ind (i+2)) name; + P.fprintf och "%s\n" (ind (i+3)) name; + P.fprintf och "%s\n" (ind (i+2)) + +let write_hook name incs tbls = + let och = open_out false name in + L.iter (map_incs och) incs; + P.fprintf och "\n\n" name; + P.fprintf och "%s\n" (ind (i+1)); + L.iter (map_tbls och) tbls; + P.fprintf och "%s\n" (ind (i+1)); + P.fprintf och "\n\n"; + close_out och diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html new file mode 100644 index 000000000..1110c7060 --- /dev/null +++ b/helm/www/lambda_delta/ld_basic_2.html @@ -0,0 +1,24 @@ + + + + + + + + + + lambda_delta version 2 + + + + + +
[lambda_delta home]
cic:/matita/lambda_delta/Basic_2/ (λδ version 2)
[Spacer]
+
Logical structure of the contribution
+
The source files are grouped in planes and components according to the following table.
+
componentplanefiles


native typing
nty


conversioncontext-sensitivecpcs


computationstrongly normalizingcsn



context-sensitivecprs


reductioncontext-sensitivelcpr




cprcpr_liftcpr_tpsscpr_cpr

context-freeltprltpr_drop



tprtpr_lifttpr_tpsstpr_tpr
static typingatomic arity ass.aaaaaa_liftaaa_aaa

static type ass.stysty_liftsty_sty
unfoldpartialltpssltpss_dropltpss_tpsltpss_ltpss


tpsstpss_lifttpss_tpsstpss_ltps
substitutionparallelltpsltps_dropltps_tpsltps_ltps


tpstps_lifttps_tps

local env. droppingdropdrop_drop


term relocationliftlift_lift

grammarlocal env. equivalenceleqleq_leq


term hom.thomthom_thom


closurescl_shiftcl_weight


internal syntaxlenvlenv_weightlenv_length


termterm_weightterm_simple


item



external syntaxaarity



parameterssh


+
Physical structure of the contribution
+
The source files are grouped in directories, one for each component.
+
[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]
+ + diff --git a/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml b/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml new file mode 100644 index 000000000..080d62ea1 --- /dev/null +++ b/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml @@ -0,0 +1,14 @@ + + + + Logical structure of the contribution + The source files are grouped in planes and components according to the following table. + + Physical structure of the contribution + The source files are grouped in directories, one for each component. + + diff --git a/helm/www/lambda_delta/web/home/ld_basic_2.tbl b/helm/www/lambda_delta/web/home/ld_basic_2.tbl new file mode 100644 index 000000000..5ba11a277 --- /dev/null +++ b/helm/www/lambda_delta/web/home/ld_basic_2.tbl @@ -0,0 +1,128 @@ +name "ld_basic_2_src" + +table { + class "grey" + [ { "component" * } { + [ { "plane" * } { + [ "files" * ] + } + ] + } + ] + class "sky" + [ { "native typing" * } { + [ { "" * } { + [ "nty" * ] + } + ] + } + ] + class "cyan" + [ { "conversion" * } { + [ { "context-sensitive" * } { + [ "cpcs" * ] + } + ] + } + ] + class "water" + [ { "computation" * } { + [ { "strongly normalizing" * } { + [ "csn" * ] + } + ] + [ { "context-sensitive" * } { + [ "cprs" * ] + } + ] + } + ] + class "green" + [ { "reduction" * } { + [ { "context-sensitive" * } { + [ "lcpr" * ] + [ "cpr" "cpr_lift" "cpr_tpss" "cpr_cpr" * ] + } + ] + [ { "context-free" * } { + [ "ltpr" "ltpr_drop" * ] + [ "tpr" "tpr_lift" "tpr_tpss" "tpr_tpr" * ] + } + ] + } + ] + class "grass" + [ { "static typing" * } { + [ { "atomic arity ass." * } { + [ "aaa" "aaa_lift" "aaa_aaa" * ] + } + ] + [ { "static type ass." * } { + [ "sty" "sty_lift" "sty_sty" * ] + } + ] + } + ] + class "yellow" + [ { "unfold" * } { + [ { "partial" * } { + [ "ltpss" "ltpss_drop" "ltpss_tps" "ltpss_ltpss" * ] + [ "tpss" "tpss_lift" "tpss_tpss" "tpss_ltps" * ] + } + ] + } + ] + class "orange" + [ { "substitution" * } { + [ { "parallel" * } { + [ "ltps" "ltps_drop" "ltps_tps" "ltps_ltps" * ] + [ "tps" "tps_lift" "tps_tps" * ] + } + ] + [ { "local env. dropping" * } { + [ "drop" "drop_drop" * ] + } + ] + [ { "term relocation" * } { + [ "lift" "lift_lift" * ] + } + ] + } + ] + class "red" + [ { "grammar" * } { + [ { "local env. equivalence" * } { + [ "leq" "leq_leq" * ] + } + ] + [ { "term hom." * } { + [ "thom" "thom_thom" * ] + } + ] + [ { "closures" * } { + [ "cl_shift" "cl_weight" * ] + } + ] + [ { "internal syntax" * } { + [ "lenv" "lenv_weight" "lenv_length" * ] + [ "term" "term_weight" "term_simple" * ] + [ "item" * ] + } + ] + [ { "external syntax" * } { + [ "aarity" * ] + } + ] + [ { "parameters" * } { + [ "sh" * ] + } + ] + } + ] +} + +class "component" { 0 } + +class "plane" { 1 } + +class "file" { 2 * }