From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 24 Feb 2021 19:05:05 +0000 (+0100)
Subject: update in bin
X-Git-Tag: make_still_working~160
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=baa54e5db0fb93c4242dd1b67a5018ca63206cf6;p=helm.git

update in bin

+ new application "recomm"
  for restyling comments in λδ source files
+ minor corrections in ground and apps_2
---

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 = "<dir>  Set this working directory (default: .)"
+let msg_L = " Log lexer tokens (default: no)"
+let msg_c = "<int>  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 <string> SP NL OP CP PP SR KW CW HW SW OT
+%token EF
+
+%start srcs
+%type <RecommTypes.srcs> 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