X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Fxhtbl%2Ffold.ml;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Fxhtbl%2Ffold.ml;h=752b06d77c5ce84eb3fc59f3da91f5358d02c970;hb=d2545ffd201b1aa49887313791386add78fa8603;hp=0000000000000000000000000000000000000000;hpb=57ae1762497a5f3ea75740e2908e04adb8642cc2;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/bin/xhtbl/fold.ml b/matita/matita/contribs/lambdadelta/bin/xhtbl/fold.ml new file mode 100644 index 000000000..752b06d77 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/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