From baa54e5db0fb93c4242dd1b67a5018ca63206cf6 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 24 Feb 2021 20:05:05 +0100 Subject: [PATCH] update in bin MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit + new application "recomm" for restyling comments in λδ source files + minor corrections in ground and apps_2 --- .../apps_2/functional/mf_vlift_exteq.ma | 1 - .../apps_2/functional/mf_vpush_exteq.ma | 1 - .../lambdadelta/apps_2/models/tm_vpush.ma | 1 - .../contribs/lambdadelta/bin/Makefile.common | 2 + .../contribs/lambdadelta/bin/recomm/Makefile | 21 ++++ .../bin/recomm/bGroundCounters.mrc | 5 + .../bin/recomm/dGroundCounters.mrc | 3 + .../contribs/lambdadelta/bin/recomm/mrc.ml | 20 ++++ .../contribs/lambdadelta/bin/recomm/mrc.mli | 0 .../lambdadelta/bin/recomm/mrcInput.ml | 71 ++++++++++++ .../lambdadelta/bin/recomm/mrcInput.mli | 5 + .../lambdadelta/bin/recomm/mrcOutput.ml | 51 ++++++++ .../lambdadelta/bin/recomm/mrcOutput.mli | 3 + .../lambdadelta/bin/recomm/mrcTypes.ml | 31 +++++ .../contribs/lambdadelta/bin/recomm/recomm.ml | 56 +++++++++ .../lambdadelta/bin/recomm/recomm.mli | 0 .../lambdadelta/bin/recomm/recommCheck.ml | 109 ++++++++++++++++++ .../lambdadelta/bin/recomm/recommCheck.mli | 17 +++ .../lambdadelta/bin/recomm/recommGc.ml | 5 + .../lambdadelta/bin/recomm/recommGc.mli | 0 .../bin/recomm/recommGcbGroundCounters.ml | 15 +++ .../bin/recomm/recommGcbGroundCounters.mli | 0 .../bin/recomm/recommGcdGroundCounters.ml | 11 ++ .../bin/recomm/recommGcdGroundCounters.mli | 0 .../lambdadelta/bin/recomm/recommGcsAttr.ml | 10 ++ .../lambdadelta/bin/recomm/recommGcsAttr.mli | 0 .../lambdadelta/bin/recomm/recommGcsMain.ml | 19 +++ .../lambdadelta/bin/recomm/recommGcsMain.mli | 0 .../lambdadelta/bin/recomm/recommGcsWith.ml | 10 ++ .../lambdadelta/bin/recomm/recommGcsWith.mli | 0 .../lambdadelta/bin/recomm/recommInput.ml | 9 ++ .../lambdadelta/bin/recomm/recommInput.mli | 1 + .../lambdadelta/bin/recomm/recommLexer.mll | 72 ++++++++++++ .../lambdadelta/bin/recomm/recommOutput.ml | 35 ++++++ .../lambdadelta/bin/recomm/recommOutput.mli | 3 + .../lambdadelta/bin/recomm/recommParser.mly | 84 ++++++++++++++ .../lambdadelta/bin/recomm/recommPccFor.ml | 32 +++++ .../lambdadelta/bin/recomm/recommPccFor.mli | 3 + .../lambdadelta/bin/recomm/recommPcsAnd.ml | 25 ++++ .../lambdadelta/bin/recomm/recommPcsAnd.mli | 1 + .../lambdadelta/bin/recomm/recommStep.ml | 5 + .../lambdadelta/bin/recomm/recommStep.mli | 4 + .../lambdadelta/bin/recomm/recommTypes.ml | 29 +++++ .../contribs/lambdadelta/bin/recomm/sAttr.mrc | 4 + .../contribs/lambdadelta/bin/recomm/sMain.mrc | 5 + .../contribs/lambdadelta/bin/recomm/sWith.mrc | 2 + .../lambdadelta/ground/steps/rtc_isrt.ma | 2 +- .../ground/steps/rtc_isrt_shift.ma | 4 +- 48 files changed, 781 insertions(+), 6 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/Makefile create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/bGroundCounters.mrc create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/dGroundCounters.mrc create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/mrc.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/mrc.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/mrcTypes.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recomm.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGc.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundCounters.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundCounters.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGcsAttr.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGcsAttr.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGcsMain.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGcsMain.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommInput.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommInput.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommParser.mly create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommStep.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommStep.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/sAttr.mrc create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/sMain.mrc create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma index fcb491078..d7d6211ec 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "ground/lib/functions.ma". -include "ground/lib/exteq.ma". include "apps_2/functional/flifts_flifts_basic.ma". include "apps_2/functional/mf_vlift.ma". diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma index e35fb1dfe..855934ca2 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "ground/lib/functions.ma". -include "ground/lib/exteq.ma". include "apps_2/functional/flifts_flifts_basic.ma". include "apps_2/functional/mf_vpush.ma". diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/tm_vpush.ma b/matita/matita/contribs/lambdadelta/apps_2/models/tm_vpush.ma index 35dfe7820..1eae07864 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/tm_vpush.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/tm_vpush.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "ground/lib/exteq.ma". include "apps_2/models/model_vpush.ma". include "apps_2/models/tm.ma". diff --git a/matita/matita/contribs/lambdadelta/bin/Makefile.common b/matita/matita/contribs/lambdadelta/bin/Makefile.common index 7f95f4a23..ad41f216c 100644 --- a/matita/matita/contribs/lambdadelta/bin/Makefile.common +++ b/matita/matita/contribs/lambdadelta/bin/Makefile.common @@ -32,5 +32,7 @@ clean:: .PHONY: all clean +.SUFFIXES: + %.ml: %.aml $(H)$(ALPHA) < $< > $@ diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/Makefile b/matita/matita/contribs/lambdadelta/bin/recomm/Makefile new file mode 100644 index 000000000..fdee8f321 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/Makefile @@ -0,0 +1,21 @@ +EXECS = mrc recomm + +REQUIRES = + +include ../Makefile.common + +clean:: + @$(RM) recommGc*.ml* + +test: + @./recomm.native $(O) -C ../../ground/steps . | sort | uniq > log.txt + +MRCS = $(wildcard *.mrc) + +mrc: $(MRCS:%.mrc=recommGc%.ml) + @./mrc.native . + +recommGc%.ml recommGc%.mli: %.mrc mrc.ml + @./mrc.native $< + +.PHONY: test mrc diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/bGroundCounters.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/bGroundCounters.mrc new file mode 100644 index 000000000..bd88c9d60 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/bGroundCounters.mrc @@ -0,0 +1,5 @@ +PcsAnd b "" true false +rtc_max, max +rtc_shift, shift +rtc_ism, test for constrained rt-transition counter +rtc_ist, test for t-transition counter diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/dGroundCounters.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/dGroundCounters.mrc new file mode 100644 index 000000000..f78834d6a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/dGroundCounters.mrc @@ -0,0 +1,3 @@ +PccFor d "" true false +T-BOUND RT-TRANSITION COUNTERS, RT-TRANSITION COUNTER +T-TRANSITION COUNTERS, T-TRANSITION COUNTER diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/mrc.ml b/matita/matita/contribs/lambdadelta/bin/recomm/mrc.ml new file mode 100644 index 000000000..1e04132c5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/mrc.ml @@ -0,0 +1,20 @@ +module EI = MrcInput +module EO = MrcOutput + +let process file = + if Sys.is_directory file then begin + let st = EI.read_dir file in + if st <> EI.read_index file then begin + Printf.eprintf "indexing: %S\n" file; + EO.write_index st + end + end else if Filename.extension file = ".mrc" then begin + Printf.eprintf "processing: %S\n" file; + EO.write_component (EI.read_file file) + end else begin + Printf.eprintf "skipping: %S\n" file + end + +let main = + Arg.parse [ + ] process "" diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/mrc.mli b/matita/matita/contribs/lambdadelta/bin/recomm/mrc.mli new file mode 100644 index 000000000..e69de29bb diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml new file mode 100644 index 000000000..c5d7f5857 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml @@ -0,0 +1,71 @@ +module ET = MrcTypes + +let read_substs substs ich = + let map subst = + let words = String.split_on_char ' ' subst in + List.filter ((<>) "") words + in + while true do + let line = input_line ich in + let subst = String.split_on_char ',' line in + substs := List.map map subst :: !substs + done + +let read_file file = + let ich = open_in file in + let line = input_line ich in + let scan r f d p o = r, f, d, p, o in + let rmod, rfun, dmod, para, optn = + Scanf.sscanf line "%s %s %S %b %b" scan + in + let substs = ref [] in + begin + try read_substs substs ich with + | End_of_file -> close_in ich + end; + { + ET.cmod = Filename.remove_extension file; + rmod; rfun; dmod; para; optn; + substs = !substs; + } + +let list_rev_filter_map filter map l = + let rec aux r = function + | [] -> r + | hd :: tl -> if filter hd then aux (map hd :: r) tl else aux r tl + in + aux [] l + +let read_dir file = + let filter name = + Filename.extension name = ".mrc" + in + let map name = + Filename.remove_extension name + in + let dir = Array.to_list (Sys.readdir file) in + let mods = List.fast_sort Pervasives.compare (list_rev_filter_map filter map dir) in + { + ET.cdir = file; mods; + } + +let rec read_mods mods ich = + let line = input_line ich in + let scan _ m = + mods := m :: !mods + in + Scanf.sscanf line "module %s = RecommGc%s" scan; + read_mods mods ich + +let read_index dir = + let file = Filename.concat dir "recommGc.ml" in + let mods = ref [] in + if Sys.file_exists file then begin + let ich = open_in file in + try read_mods mods ich with + | End_of_file -> close_in ich + end; + let mods = List.fast_sort Pervasives.compare !mods in + { + ET.cdir = dir; mods; + } diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.mli b/matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.mli new file mode 100644 index 000000000..9bbde0d05 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.mli @@ -0,0 +1,5 @@ +val read_file: string -> MrcTypes.mrc_status + +val read_dir: string -> MrcTypes.idx_status + +val read_index: string -> MrcTypes.idx_status diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml new file mode 100644 index 000000000..abece29bb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml @@ -0,0 +1,51 @@ +module ET = MrcTypes + +let cap = String.capitalize_ascii + +let ok b = + if b then "true" else "ok" + +let write_mli name = + let file = name ^ ".mli" in + if Sys.file_exists file then () + else begin + let och = open_out file in + close_out och + end + +let write_subst st och subst = + let iter hd words = + let lhs = List.map (Printf.sprintf "%S :: ") words in + let rhs = List.map (Printf.sprintf "%S :: ") hd in + Printf.fprintf och " | %stl -> k %s (%souts) tl\n" + (String.concat "" lhs) (ok st.ET.para) (String.concat "" rhs) + in + match subst with + | [] -> () + | hd :: _ -> List.iter (iter (List.rev hd)) subst + +let write_component st = + let cmod = "recommGc" ^ st.ET.cmod in + let och = open_out (cmod ^ ".ml") in + if st.ET.dmod <> "" then begin + Printf.fprintf och "module D = Recomm%s\n\n" (cap st.ET.dmod) + end; + Printf.fprintf och "let step k ok outs ins =\n"; + Printf.fprintf och " if ok then k ok outs ins else\n"; + Printf.fprintf och " match ins with\n"; + List.iter (write_subst st och) st.ET.substs; + Printf.fprintf och " | _ -> k %s outs ins\n\n" (ok st.ET.optn); + Printf.fprintf och "let main =\n"; + Printf.fprintf och " Recomm%s.register_%s step\n" (cap st.ET.rmod) st.ET.rfun; + close_out och; + write_mli cmod + +let write_index st = + let cmod = Filename.concat st.ET.cdir "recommGc" in + let och = open_out (cmod ^ ".ml") in + let iter i name = + Printf.fprintf och "module G%u = RecommGc%s\n" (succ i) name + in + List.iteri iter st.ET.mods; + close_out och; + write_mli cmod diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.mli b/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.mli new file mode 100644 index 000000000..52248c2f1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.mli @@ -0,0 +1,3 @@ +val write_component: MrcTypes.mrc_status -> unit + +val write_index: MrcTypes.idx_status -> unit diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/mrcTypes.ml b/matita/matita/contribs/lambdadelta/bin/recomm/mrcTypes.ml new file mode 100644 index 000000000..1ff1b9096 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/mrcTypes.ml @@ -0,0 +1,31 @@ +type word = string + +type words = word list + +type subst = words list + +type substs = subst list + +type mrc_status = { +(* component module *) + cmod : string; +(* register module *) + rmod : string; +(* register function *) + rfun : string; +(* optional depend module *) + dmod : string; +(* parallel component *) + para : bool; +(* optional component *) + optn : bool; +(* substitutions *) + substs : substs; +} + +type idx_status = { +(* indexed directory *) + cdir: string; +(* indexed modules *) + mods: string list; +} diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml new file mode 100644 index 000000000..a2336ad9c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml @@ -0,0 +1,56 @@ +module EC = RecommCheck +module EL = RecommLexer +module EI = RecommInput +module EO = RecommOutput + +module P1 = RecommPccFor +module P2 = RecommPcsAnd + +module G = RecommGc + +let write = ref false + +let chdir path = + Sys.chdir path + +let rec process path name = + let file = Filename.concat path name in + if Sys.is_directory file then begin + let dir = Sys.readdir file in + Array.iter (process file) dir + end else + if Filename.extension file = ".ma" then begin + Printf.eprintf "processing: %S\n" file; + let orig = EI.read_srcs file in + let lint = EC.recomm_srcs orig in + if !write && lint <> orig then EO.write_srcs file lint + end else begin + Printf.eprintf "skipping: %S\n" file + end + +let msg_C = " Set this working directory (default: .)" +let msg_L = " Log lexer tokens (default: no)" +let msg_c = " Set these output columns (default: 78)" +let msg_d = " Log with dark colors (default: no)" +let msg_k = " Log key comments (default: no)" +let msg_m = " Log mark comments (default: no)" +let msg_n = " Log with no colors (default: yes)" +let msg_o = " Log other comments (default: no)" +let msg_s = " Log section comments (default: no)" +let msg_t = " Log title comments (default: no)" +let msg_w = " Write the output files (default: no)" + +let main = + Arg.parse [ + "-C", Arg.String chdir, msg_C; + "-L", Arg.Set EL.debug, msg_m; + "-c", Arg.Int ((:=) EO.width), msg_c; + "-d", Arg.Clear EC.bw, msg_d; + "-k", Arg.Set EC.log_k, msg_k; + "-m", Arg.Set EC.log_m, msg_m; + "-n", Arg.Set EC.bw, msg_n; + "-o", Arg.Set EC.log_o, msg_o; + "-s", Arg.Set EC.log_s, msg_s; + "-t", Arg.Set EC.log_t, msg_t; + "-w", Arg.Set write, msg_w; + ] (process "") "" diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recomm.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recomm.mli new file mode 100644 index 000000000..e69de29bb diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml new file mode 100644 index 000000000..93d1d0316 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml @@ -0,0 +1,109 @@ +module ES = RecommStep +module ET = RecommTypes + +let c_line = ref ES.id + +let s_line = ref ES.id + +let k_final b ws1 ws2 = b, ws1, ws2 + +type status = + { + r: ET.srcs; (* reversed result *) + } + +let init () = + { + r = []; + } + +let add src st = + { + r = src :: st.r; + } + +let middle st = + match st.r with + | [] + | ET.Line _ :: _ -> false + | _ -> true + +let mute_o = [| + "___ "; + "||M|| "; + "||A|| A project by Andrea Asperti "; + "||T|| "; + "||I|| Developers: "; + "||T|| The HELM team. "; + "||A|| http://helm.cs.unibo.it "; + "\\ / "; + "\\ / This file is distributed under the terms of the "; + "v GNU General Public License Version 2 "; + ""; +|] + +let bw = ref false + +let log_k = ref false +let log_m = ref false +let log_o = ref false +let log_s = ref false +let log_t = ref false + +let no_color = "\x1B[0m" +let black = "\x1B[30m" +let sky = "\x1B[38;2;0;96;128m" +let blue = "\x1B[34m" +let prune = "\x1B[38;2;96;0;128m" +let red = "\x1B[31m" + +let log color s = + if !bw then Printf.printf "%S\n" s else + Printf.printf "%s%S%s\n" color s no_color + +let rec recomm srcs st = + match srcs with + | [] -> + st + | ET.Line _ as hd :: tl -> + recomm tl @@ add hd @@ st + | ET.Text _ as hd :: tl -> + recomm tl @@ add hd @@ st + | ET.Mark s as hd :: tl -> + if !log_m then log red s; + recomm tl @@ add hd @@ st + | ET.Key (s1, s2) as hd :: tl -> + if middle st then Printf.eprintf "middle: %S\n" s1; + if !log_k then log prune (s1^s2); + recomm tl @@ add hd @@ st + | ET.Title ss as hd :: tl -> + if middle st then Printf.eprintf "middle: TITLE\n"; + let b, ss1, ss2 = !c_line k_final false [] ss in + let ss2 = + if ss2 = [] then ss2 else "*" :: ss2 + in + let ss = List.rev_append ss1 ss2 in + let s = String.concat " " ss in + if !log_t then log blue s; + recomm tl @@ add hd @@ st + | ET.Slice ss as hd :: tl -> + if middle st then Printf.eprintf "middle: Section\n"; + let b, ss1, ss2 = !s_line k_final false [] ss in + let ss2 = + if ss2 = [] then ss2 else "*" :: ss2 + in + let ss = List.rev_append ss1 ss2 in + let s = String.capitalize_ascii (String.concat " " ss) in + if !log_s then log sky s; + recomm tl @@ add hd @@ st + | ET.Other (_, s, _) as hd :: tl -> + if !log_o && not (Array.mem s mute_o) then log black s; + recomm tl @@ add hd @@ st + +let recomm_srcs srcs = + let st = recomm srcs @@ init () in + List.rev st.r + +let register_c = ES.register c_line + +let register_s = ES.register s_line diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.mli new file mode 100644 index 000000000..971386007 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.mli @@ -0,0 +1,17 @@ +val log_k: bool ref + +val log_m: bool ref + +val log_o: bool ref + +val log_s: bool ref + +val log_t: bool ref + +val bw: bool ref + +val register_c: RecommTypes.step -> unit + +val register_s: RecommTypes.step -> unit + +val recomm_srcs: RecommTypes.srcs -> RecommTypes.srcs diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml new file mode 100644 index 000000000..6ffe876a7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml @@ -0,0 +1,5 @@ +module G1 = RecommGcbGroundCounters +module G2 = RecommGcdGroundCounters +module G3 = RecommGcsAttr +module G4 = RecommGcsMain +module G5 = RecommGcsWith diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.mli new file mode 100644 index 000000000..e69de29bb diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.ml new file mode 100644 index 000000000..da14eabe1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.ml @@ -0,0 +1,15 @@ +let step k ok outs ins = + if ok then k ok outs ins else + match ins with + | "rtc_ist" :: tl -> k true ("rtc_ist" :: outs) tl + | "test" :: "for" :: "t-transition" :: "counter" :: tl -> k true ("rtc_ist" :: outs) tl + | "rtc_ism" :: tl -> k true ("rtc_ism" :: outs) tl + | "test" :: "for" :: "constrained" :: "rt-transition" :: "counter" :: tl -> k true ("rtc_ism" :: outs) tl + | "rtc_shift" :: tl -> k true ("rtc_shift" :: outs) tl + | "shift" :: tl -> k true ("rtc_shift" :: outs) tl + | "rtc_max" :: tl -> k true ("rtc_max" :: outs) tl + | "max" :: tl -> k true ("rtc_max" :: outs) tl + | _ -> k ok outs ins + +let main = + RecommPcsAnd.register_b step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.mli new file mode 100644 index 000000000..e69de29bb diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundCounters.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundCounters.ml new file mode 100644 index 000000000..5f86d75fe --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundCounters.ml @@ -0,0 +1,11 @@ +let step k ok outs ins = + if ok then k ok outs ins else + match ins with + | "T-TRANSITION" :: "COUNTERS" :: tl -> k true ("COUNTERS" :: "T-TRANSITION" :: outs) tl + | "T-TRANSITION" :: "COUNTER" :: tl -> k true ("COUNTERS" :: "T-TRANSITION" :: outs) tl + | "T-BOUND" :: "RT-TRANSITION" :: "COUNTERS" :: tl -> k true ("COUNTERS" :: "RT-TRANSITION" :: "T-BOUND" :: outs) tl + | "RT-TRANSITION" :: "COUNTER" :: tl -> k true ("COUNTERS" :: "RT-TRANSITION" :: "T-BOUND" :: outs) tl + | _ -> k ok outs ins + +let main = + RecommPccFor.register_d step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundCounters.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundCounters.mli new file mode 100644 index 000000000..e69de29bb diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsAttr.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsAttr.ml new file mode 100644 index 000000000..cb7037f67 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsAttr.ml @@ -0,0 +1,10 @@ +let step k ok outs ins = + if ok then k ok outs ins else + match ins with + | "main" :: tl -> k ok ("main" :: outs) tl + | "basic" :: tl -> k ok ("basic" :: outs) tl + | "advanced" :: tl -> k ok ("advanced" :: outs) tl + | _ -> k ok outs ins + +let main = + RecommCheck.register_s step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsAttr.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsAttr.mli new file mode 100644 index 000000000..e69de29bb diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsMain.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsMain.ml new file mode 100644 index 000000000..82905b840 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsMain.ml @@ -0,0 +1,19 @@ +module D = RecommGcsAttr + +let step k ok outs ins = + if ok then k ok outs ins else + match ins with + | "eliminations" :: tl -> k ok ("eliminations" :: outs) tl + | "eliminators" :: tl -> k ok ("eliminations" :: outs) tl + | "destructions" :: tl -> k ok ("destructions" :: outs) tl + | "forward" :: "properties" :: tl -> k ok ("destructions" :: outs) tl + | "forward" :: "lemmas" :: tl -> k ok ("destructions" :: outs) tl + | "inversions" :: tl -> k ok ("inversions" :: outs) tl + | "inversion" :: "properties" :: tl -> k ok ("inversions" :: outs) tl + | "inversion" :: "lemmas" :: tl -> k ok ("inversions" :: outs) tl + | "constructions" :: tl -> k ok ("constructions" :: outs) tl + | "properties" :: tl -> k ok ("constructions" :: outs) tl + | _ -> k true outs ins + +let main = + RecommCheck.register_s step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsMain.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsMain.mli new file mode 100644 index 000000000..e69de29bb diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml new file mode 100644 index 000000000..8e1d810a2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml @@ -0,0 +1,10 @@ +module D = RecommGcsMain + +let step k ok outs ins = + if ok then k ok outs ins else + match ins with + | "with" :: tl -> k ok ("with" :: outs) tl + | _ -> k true outs ins + +let main = + RecommCheck.register_s step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.mli new file mode 100644 index 000000000..e69de29bb diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommInput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommInput.ml new file mode 100644 index 000000000..78777b1ca --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommInput.ml @@ -0,0 +1,9 @@ +module EL = RecommLexer +module EP = RecommParser + +let read_srcs file = + let ich = open_in file in + let lexbuf = Lexing.from_channel ich in + let srcs = EP.srcs EL.src_token lexbuf in + close_in ich; + srcs diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommInput.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommInput.mli new file mode 100644 index 000000000..5e8295c18 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommInput.mli @@ -0,0 +1 @@ +val read_srcs: string -> RecommTypes.srcs diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll b/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll new file mode 100644 index 000000000..0f66fc44b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll @@ -0,0 +1,72 @@ +{ + module EP = RecommParser + + let debug = ref false + + let keys = [| + "Note"; + |] + + let heads = [| + "Advanved"; + "Basic"; + "Forward"; + "Destructions"; + "Eliminations"; + "Eliminators"; + "Inversion"; + "Inversions"; + "Main"; + "Properties"; + |] + + let str c = String.make 1 c + + let nl lexbuf = Lexing.new_line lexbuf + + let is_uppercase_ascii s = + let rec aux i = + if i < 0 then true else + if 'a' <= s.[i] && s.[i] <= 'z' then false else + aux (pred i) + in + aux (String.length s - 1) + + let disambiguate_word s = + if is_uppercase_ascii s then EP.CW s else + if Array.mem s keys then EP.KW s else + if Array.mem s heads then EP.HW s else + EP.SW s + + let log s = + if !debug then Printf.eprintf "lezer: %s\n" s + + let log_s s = + if !debug then Printf.eprintf "lexer: %S\n" s + + let log_c c = + if !debug then Printf.eprintf "lexer: %C\n" c +} + +let CR = "\r" +let SP = " " +let NL = "\n" +let SR = "*" +let OP = "(*" SP* +let CP = SR* "*)" +let PP = CP SP* OP +let WF = ['A'-'Z' 'a'-'z'] +let WB = ['A'-'Z' 'a'-'z' '_' '-']* +let WD = WF WB + +rule src_token = parse + | CR { src_token lexbuf } + | NL as c { log "NL"; nl lexbuf; EP.NL (str c) } + | SP+ as s { log "SP"; EP.SP s } + | PP as s { log "PP"; EP.PP s } + | OP as s { log "OP"; EP.OP s } + | CP as s { log "CP"; EP.CP s } + | SR as c { log "SR"; EP.SR (str c) } + | WD as s { log_s s ; disambiguate_word s } + | _ as c { log_c c ; EP.OT (str c) } + | eof { log "EF"; EP.EF } diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml new file mode 100644 index 000000000..5189c7f77 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml @@ -0,0 +1,35 @@ +module ET = RecommTypes + +let width = ref 78 + +let complete s = + let l = !width - String.length s - 6 in + if l < 0 then begin + Printf.eprintf "overfull: %S\n" s; + "" + end else begin + String.make l '*' + end + +let out_src och = function + | ET.Line s -> + Printf.fprintf och "%s" s + | ET.Text s -> + Printf.fprintf och "%s" s + | ET.Mark s -> + Printf.fprintf och "(* %s**)" s + | ET.Key (s1, s2) -> + Printf.fprintf och "(* %s1%s2*)" s1 s2 + | ET.Title ss -> + let s = String.concat " " ss in + Printf.fprintf och "(* %s %s*)" s (complete s) + | ET.Slice ss -> + let s = String.capitalize_ascii (String.concat " " ss) in + Printf.fprintf och "(* %s %s*)" s (complete s) + | ET.Other (s1, s2, s3) -> + Printf.fprintf och "%s%s%s" s1 s2 s3 + +let write_srcs file srcs = + let och = open_out (file ^ ".new") in + List.iter (out_src och) srcs; + close_out och diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.mli new file mode 100644 index 000000000..e1e856296 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.mli @@ -0,0 +1,3 @@ +val width: int ref + +val write_srcs: string -> RecommTypes.srcs -> unit diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommParser.mly b/matita/matita/contribs/lambdadelta/bin/recomm/recommParser.mly new file mode 100644 index 000000000..5686e747e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommParser.mly @@ -0,0 +1,84 @@ +%{ + + module ET = RecommTypes + + let lc = String.lowercase_ascii + +%} + +%token SP NL OP CP PP SR KW CW HW SW OT +%token EF + +%start srcs +%type srcs + +%% + +inn_r: + | SP { $1 } + | NL { $1 } + | SW { $1 } + | OT { $1 } + +inn: + | inn_r { $1 } + | KW { $1 } + | CW { $1 } + | HW { $1 } + +inns_r: + | inn_r { $1 } + | inn_r inns { $1 ^ $2 } + +inns: + | inn { $1 } + | inn inns { $1 ^ $2 } + +out: + | SP { $1 } + | SR { $1 } + | KW { $1 } + | CW { $1 } + | HW { $1 } + | SW { $1 } + | OT { $1 } + +outs: + | out { $1 } + | out outs { $1 ^ $2 } + +sw: + | HW { lc $1 } + | SW { lc $1 } + +cws: + | { [] } + | SP { [] } + | SP CW cws { $2 :: $3 } + +sws: + | { [] } + | SP { [] } + | SP sw sws { $2 :: $3 } + +src_l: + | NL { ET.Line $1 } + | OP PP inns CP { ET.Mark $3 } + | OP KW inns CP { ET.Key ($2, $3) } + | OP CW cws CP { ET.Title ($2 :: $3) } + | OP HW sws CP { ET.Slice (lc $2 :: $3) } + | OP CP { ET.Other ($1, "", $2) } + | OP inns_r CP { ET.Other ($1, $2, $3) } + | OP SR inns CP { ET.Other ($1, $2 ^ $3, $4) } + | OP SR SR inns CP { ET.Other ($1, $2 ^ $3 ^ $4, $5) } + +src: + | outs { ET.Text $1 } + +srcs_l: + | EF { [] } + | src_l srcs { $1 :: $2 } + +srcs: + | srcs_l { $1 } + | src srcs_l { $1 :: $2 } diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml new file mode 100644 index 000000000..5d08261c8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml @@ -0,0 +1,32 @@ +module EC = RecommCheck +module ES = RecommStep + +let d_line = ref ES.id + +let r_line = ref ES.id + +let k_for k ok outs ins = + if ok then begin + match ins with + | "for" :: tl -> !d_line k false ("for" :: outs) tl + | _ -> k true outs ins + end else begin + k true outs ins + end + +let k_or k ok outs ins = + if ok then k ok outs ins else + !r_line (k_for k) ok outs ins + +let step k ok outs ins = + if ok then k ok outs ins else + !d_line (k_or k) ok outs ins + +let register_d = + ES.register d_line + +let register_r = + ES.register r_line + +let main = + EC.register_c step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.mli new file mode 100644 index 000000000..ee07f8147 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.mli @@ -0,0 +1,3 @@ +val register_d: RecommTypes.step -> unit + +val register_r: RecommTypes.step -> unit diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml new file mode 100644 index 000000000..de05255a5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml @@ -0,0 +1,25 @@ +module EC = RecommCheck +module ES = RecommStep + +module D = RecommGcsWith + +let b_line = ref ES.id + +let rec k_and k ok outs ins = + if ok then begin + match ins with + | "and" :: tl -> step k false ("and" :: outs) tl + | _ -> k true outs ins + end else begin + k true outs ins + end + +and step k ok outs ins = + if ok then k ok outs ins else + !b_line (k_and k) ok outs ins + +let register_b = + ES.register b_line + +let main = + EC.register_s step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.mli new file mode 100644 index 000000000..9d815c44a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.mli @@ -0,0 +1 @@ +val register_b: RecommTypes.step -> unit diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommStep.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommStep.ml new file mode 100644 index 000000000..a9b26c22d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommStep.ml @@ -0,0 +1,5 @@ +let id p = p + +let register line next = + let first = !line in + line := fun k -> first @@ next @@ k diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommStep.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommStep.mli new file mode 100644 index 000000000..df91cd169 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommStep.mli @@ -0,0 +1,4 @@ +val id: ('s, 't) RecommTypes.astep + +val register: ('s, 't) RecommTypes.astep ref -> ('s, 't) RecommTypes.astep -> unit + diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml new file mode 100644 index 000000000..f2f8e87a9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml @@ -0,0 +1,29 @@ +type text = string + +type word = string + +type words = word list + +type src = +(* end of line *) + | Line of text +(* other text *) + | Text of text +(* mark *) + | Mark of text +(* Key *) + | Key of word * text +(* title *) + | Title of words +(* section *) + | Slice of words +(* other comment *) + | Other of text * text * text + +type srcs = src list + +type ('s, 't) aproc = 's -> words -> words -> 't + +type ('s, 't) astep = ('s, 't) aproc -> ('s, 't) aproc + +type step = (bool, bool * words * words) astep diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/sAttr.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/sAttr.mrc new file mode 100644 index 000000000..4daa8ba06 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/sAttr.mrc @@ -0,0 +1,4 @@ +check s "" false false +advanced +basic +main diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/sMain.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/sMain.mrc new file mode 100644 index 000000000..8ed0ff28d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/sMain.mrc @@ -0,0 +1,5 @@ +check s "GcsAttr" false true +constructions, properties +inversions, inversion properties, inversion lemmas +destructions, forward properties, forward lemmas +eliminations, eliminators diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc new file mode 100644 index 000000000..1a7d1fbfb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc @@ -0,0 +1,2 @@ +check s "GcsMain" false true +with diff --git a/matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt.ma b/matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt.ma index 7f9f2f74a..667172096 100644 --- a/matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt.ma +++ b/matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt.ma @@ -20,7 +20,7 @@ include "ground/steps/rtc.ma". definition isrt: relation2 nat rtc ≝ λts,c. ∃∃ri,rs. 〈ri,rs,0,ts〉 = c. -interpretation "test for costrained rt-transition counter (rtc)" +interpretation "test for constrained rt-transition counter (rtc)" 'IsRedType ts c = (isrt ts c). (* Basic properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt_shift.ma b/matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt_shift.ma index b9f14a958..0e0b73f4a 100644 --- a/matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt_shift.ma +++ b/matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt_shift.ma @@ -17,13 +17,13 @@ include "ground/steps/rtc_isrt.ma". (* RT-TRANSITION COUNTER ****************************************************) -(* Properties with test for costrained rt-transition counter ****************) +(* Properties with test for constrained rt-transition counter ***************) lemma isr_shift: ∀c. 𝐑𝐓❪0,c❫ → 𝐑𝐓❪0,↕*c❫. #c * #ri #rs #H destruct /2 width=3 by ex1_2_intro/ qed. -(* Inversion properties with test for costrained rt-counter *****************) +(* Inversion properties with test for constrained rt-transition counter *****) lemma isrt_inv_shift: ∀n,c. 𝐑𝐓❪n,↕*c❫ → 𝐑𝐓❪0,c❫ ∧ 0 = n. #n #c * #ri #rs #H -- 2.39.2