From: Ferruccio Guidi Date: Sat, 27 Feb 2021 21:54:36 +0000 (+0100) Subject: update in ground X-Git-Tag: make_still_working~156 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=4d232392091ee233afc26ecf3120dd5f5c6a33c8 update in ground + arith restyled + recomm updated --- diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/Makefile b/matita/matita/contribs/lambdadelta/bin/recomm/Makefile index cb3deebf6..6fdc32c44 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/Makefile +++ b/matita/matita/contribs/lambdadelta/bin/recomm/Makefile @@ -15,7 +15,7 @@ MRCS = $(wildcard *.mrc) mrc: $(MRCS:%.mrc=recommGc%.ml) @./mrc.native . -recommGc%.ml recommGc%.mli: %.mrc mrc.ml +recommGc%.ml recommGc%.mli: %.mrc mrc*.ml mrc*.mli @./mrc.native $< .PHONY: test mrc diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/bGroundArith.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/bGroundArith.mrc new file mode 100644 index 000000000..561d9f957 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/bGroundArith.mrc @@ -0,0 +1,16 @@ +PcsAnd b "" true false +niter +ntri +nsucc +npred +nplus +nminus +nmax +nle +nlt +ysucc +ypred +yplus +ylminus, yminus +yle +ylt diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/dGroundArith.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/dGroundArith.mrc new file mode 100644 index 000000000..2a721cf63 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/dGroundArith.mrc @@ -0,0 +1,7 @@ +PccFor d "" true false +POSITIVE INTEGERS +NON-NEGATIVE INTEGERS +NON-NEGATIVE INTEGERS WITH INFINITY +WELL-FOUNDED INDUCTION +λδ-2A +λδ-2B diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml index abece29bb..19128fb63 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml @@ -2,8 +2,8 @@ module ET = MrcTypes let cap = String.capitalize_ascii -let ok b = - if b then "true" else "ok" +let ko b = + if b then "KO" else "OO" let write_mli name = let file = name ^ ".mli" in @@ -17,8 +17,8 @@ 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) + Printf.fprintf och " | %stl -> k T.OK (%souts) tl\n" + (String.concat "" lhs) (String.concat "" rhs) in match subst with | [] -> () @@ -27,16 +27,23 @@ let write_subst st och subst = let write_component st = let cmod = "recommGc" ^ st.ET.cmod in let och = open_out (cmod ^ ".ml") in + Printf.fprintf och "module T = RecommTypes\n"; + Printf.fprintf och "module R = Recomm%s\n" (cap st.ET.rmod); if st.ET.dmod <> "" then begin - Printf.fprintf och "module D = Recomm%s\n\n" (cap st.ET.dmod) + Printf.fprintf och "module D = Recomm%s\n" (cap st.ET.dmod) + end; + Printf.fprintf och "\n"; + Printf.fprintf och "let step k st outs ins =\n"; + if st.ET.para then begin + Printf.fprintf och " if st <> T.OO then k st outs ins else\n" + end else begin + Printf.fprintf och " if st = T.KO then k st outs ins else\n" 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 " | _ -> k T.%s outs ins\n\n" (ko 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; + Printf.fprintf och " R.register_%s step\n" st.ET.rfun; close_out och; write_mli cmod @@ -44,7 +51,7 @@ 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 + Printf.fprintf och "module G%03u = RecommGc%s\n" (succ i) name in List.iteri iter st.ET.mods; close_out och; diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/pGroundArith.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/pGroundArith.mrc new file mode 100644 index 000000000..226e772f3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/pGroundArith.mrc @@ -0,0 +1,2 @@ +PcsPar p "" true false +(semigroup properties) diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/rGroundArith.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundArith.mrc new file mode 100644 index 000000000..bfc2730fc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundArith.mrc @@ -0,0 +1,14 @@ +PccFor r "" true false +DISCRIMINATOR +ITERATED FUNCTION +TRICHOTOMY OPERATOR +NAT-INJECTION +SUCCESSOR +PREDECESSOR +ADDITION +SUBTRACTION +LEFT SUBTRACTION +MAXIMUM, MAXIMUN +ORDER +STRICT ORDER +ARITHMETICAL PROPERTIES diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/rGroundCounters.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundCounters.mrc index 72b071350..35503a9f3 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/rGroundCounters.mrc +++ b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundCounters.mrc @@ -1,4 +1,2 @@ PccFor r "" true false -ADDITION -MAXIMUM, MAXIMUN SHIFT diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml index bac315438..ce971dd45 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml @@ -5,6 +5,7 @@ module EO = RecommOutput module P1 = RecommPccFor module P2 = RecommPcsAnd +module P3 = RecommPcsPar module G = RecommGc diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml index e5629ccc8..655ff8095 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml @@ -5,7 +5,7 @@ let c_line = ref ES.id let s_line = ref ES.id -let k_final b ws1 ws2 = b, ws1, ws2 +let k_final r ws1 ws2 = r, ws1, ws2 type status = { @@ -29,16 +29,17 @@ let middle st = | _ -> 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 "; + " "; + " ___ "; + " ||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 "; ""; |] @@ -78,9 +79,9 @@ let rec recomm srcs st = recomm tl @@ add hd @@ st | ET.Title ss :: tl -> if middle st then Printf.eprintf "middle: TITLE\n"; - let b, ss1, ss2 = !c_line k_final false [] ss in + let r, ss1, ss2 = !c_line k_final ET.OO [] ss in let ss2 = - if ss2 = [] then ss2 else "*" :: ss2 + if r <> ET.KO && ss2 = [] then ss2 else "*" :: ss2 in let ss = List.rev_append ss1 ss2 in let s = String.concat " " ss in @@ -88,9 +89,9 @@ let rec recomm srcs st = recomm tl @@ add (ET.Title ss) @@ st | ET.Slice ss :: tl -> if middle st then Printf.eprintf "middle: Section\n"; - let b, ss1, ss2 = !s_line k_final false [] ss in + let r, ss1, ss2 = !s_line k_final ET.OO [] ss in let ss2 = - if ss2 = [] then ss2 else "*" :: ss2 + if r <> ET.KO && ss2 = [] then ss2 else "*" :: ss2 in let ss = List.rev_append ss1 ss2 in let s = String.capitalize_ascii (String.concat " " ss) in diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml index 12a3ec664..b3fd0b550 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml @@ -1,6 +1,10 @@ -module G1 = RecommGcbGroundCounters -module G2 = RecommGcdGroundCounters -module G3 = RecommGcrGroundCounters -module G4 = RecommGcsAttr -module G5 = RecommGcsMain -module G6 = RecommGcsWith +module G001 = RecommGcbGroundArith +module G002 = RecommGcbGroundCounters +module G003 = RecommGcdGroundArith +module G004 = RecommGcdGroundCounters +module G005 = RecommGcpGroundArith +module G006 = RecommGcrGroundArith +module G007 = RecommGcrGroundCounters +module G008 = RecommGcsAttr +module G009 = RecommGcsMain +module G010 = RecommGcsWith diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml new file mode 100644 index 000000000..1528eb2b1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml @@ -0,0 +1,26 @@ +module T = RecommTypes +module R = RecommPcsAnd + +let step k st outs ins = + if st <> T.OO then k st outs ins else + match ins with + | "ylt" :: tl -> k T.OK ("ylt" :: outs) tl + | "yle" :: tl -> k T.OK ("yle" :: outs) tl + | "ylminus" :: tl -> k T.OK ("ylminus" :: outs) tl + | "yminus" :: tl -> k T.OK ("ylminus" :: outs) tl + | "yplus" :: tl -> k T.OK ("yplus" :: outs) tl + | "ypred" :: tl -> k T.OK ("ypred" :: outs) tl + | "ysucc" :: tl -> k T.OK ("ysucc" :: outs) tl + | "nlt" :: tl -> k T.OK ("nlt" :: outs) tl + | "nle" :: tl -> k T.OK ("nle" :: outs) tl + | "nmax" :: tl -> k T.OK ("nmax" :: outs) tl + | "nminus" :: tl -> k T.OK ("nminus" :: outs) tl + | "nplus" :: tl -> k T.OK ("nplus" :: outs) tl + | "npred" :: tl -> k T.OK ("npred" :: outs) tl + | "nsucc" :: tl -> k T.OK ("nsucc" :: outs) tl + | "ntri" :: tl -> k T.OK ("ntri" :: outs) tl + | "niter" :: tl -> k T.OK ("niter" :: outs) tl + | _ -> k T.OO outs ins + +let main = + R.register_b step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.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 index 53a98c92e..8391c7da9 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.ml @@ -1,10 +1,13 @@ -let step k ok outs ins = - if ok then k ok outs ins else +module T = RecommTypes +module R = RecommPcsAnd + +let step k st outs ins = + if st <> T.OO then k st outs ins else match ins with - | "rtc_plus" :: tl -> k true ("rtc_plus" :: outs) tl - | "rtc_max" :: tl -> k true ("rtc_max" :: outs) tl - | "rtc_shift" :: tl -> k true ("rtc_shift" :: outs) tl - | _ -> k ok outs ins + | "rtc_plus" :: tl -> k T.OK ("rtc_plus" :: outs) tl + | "rtc_max" :: tl -> k T.OK ("rtc_max" :: outs) tl + | "rtc_shift" :: tl -> k T.OK ("rtc_shift" :: outs) tl + | _ -> k T.OO outs ins let main = - RecommPcsAnd.register_b step + R.register_b step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundArith.ml new file mode 100644 index 000000000..b3ed0f29e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundArith.ml @@ -0,0 +1,16 @@ +module T = RecommTypes +module R = RecommPccFor + +let step k st outs ins = + if st <> T.OO then k st outs ins else + match ins with + | "\206\187\206\180-2B" :: tl -> k T.OK ("\206\187\206\180-2B" :: outs) tl + | "\206\187\206\180-2A" :: tl -> k T.OK ("\206\187\206\180-2A" :: outs) tl + | "WELL-FOUNDED" :: "INDUCTION" :: tl -> k T.OK ("INDUCTION" :: "WELL-FOUNDED" :: outs) tl + | "NON-NEGATIVE" :: "INTEGERS" :: "WITH" :: "INFINITY" :: tl -> k T.OK ("INFINITY" :: "WITH" :: "INTEGERS" :: "NON-NEGATIVE" :: outs) tl + | "NON-NEGATIVE" :: "INTEGERS" :: tl -> k T.OK ("INTEGERS" :: "NON-NEGATIVE" :: outs) tl + | "POSITIVE" :: "INTEGERS" :: tl -> k T.OK ("INTEGERS" :: "POSITIVE" :: outs) tl + | _ -> k T.OO outs ins + +let main = + R.register_d step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundArith.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundArith.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 index 796c21168..bcbbc7102 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundCounters.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundCounters.ml @@ -1,10 +1,13 @@ -let step k ok outs ins = - if ok then k ok outs ins else +module T = RecommTypes +module R = RecommPccFor + +let step k st outs ins = + if st <> T.OO then k st outs ins else match ins with - | "T-TRANSITION" :: "COUNTERS" :: 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" :: "COUNTERS" :: tl -> k true ("COUNTERS" :: "RT-TRANSITION" :: outs) tl - | _ -> k ok outs ins + | "T-TRANSITION" :: "COUNTERS" :: tl -> k T.OK ("COUNTERS" :: "T-TRANSITION" :: outs) tl + | "T-BOUND" :: "RT-TRANSITION" :: "COUNTERS" :: tl -> k T.OK ("COUNTERS" :: "RT-TRANSITION" :: "T-BOUND" :: outs) tl + | "RT-TRANSITION" :: "COUNTERS" :: tl -> k T.OK ("COUNTERS" :: "RT-TRANSITION" :: outs) tl + | _ -> k T.OO outs ins let main = - RecommPccFor.register_d step + R.register_d step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.ml new file mode 100644 index 000000000..7005e5c20 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.ml @@ -0,0 +1,11 @@ +module T = RecommTypes +module R = RecommPcsPar + +let step k st outs ins = + if st <> T.OO then k st outs ins else + match ins with + | "(semigroup" :: "properties)" :: tl -> k T.OK ("properties)" :: "(semigroup" :: outs) tl + | _ -> k T.OO outs ins + +let main = + R.register_p step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.mli new file mode 100644 index 000000000..e69de29bb diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml new file mode 100644 index 000000000..091cc7f5f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml @@ -0,0 +1,24 @@ +module T = RecommTypes +module R = RecommPccFor + +let step k st outs ins = + if st <> T.OO then k st outs ins else + match ins with + | "ARITHMETICAL" :: "PROPERTIES" :: tl -> k T.OK ("PROPERTIES" :: "ARITHMETICAL" :: outs) tl + | "STRICT" :: "ORDER" :: tl -> k T.OK ("ORDER" :: "STRICT" :: outs) tl + | "ORDER" :: tl -> k T.OK ("ORDER" :: outs) tl + | "MAXIMUM" :: tl -> k T.OK ("MAXIMUM" :: outs) tl + | "MAXIMUN" :: tl -> k T.OK ("MAXIMUM" :: outs) tl + | "LEFT" :: "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: "LEFT" :: outs) tl + | "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: outs) tl + | "ADDITION" :: tl -> k T.OK ("ADDITION" :: outs) tl + | "PREDECESSOR" :: tl -> k T.OK ("PREDECESSOR" :: outs) tl + | "SUCCESSOR" :: tl -> k T.OK ("SUCCESSOR" :: outs) tl + | "NAT-INJECTION" :: tl -> k T.OK ("NAT-INJECTION" :: outs) tl + | "TRICHOTOMY" :: "OPERATOR" :: tl -> k T.OK ("OPERATOR" :: "TRICHOTOMY" :: outs) tl + | "ITERATED" :: "FUNCTION" :: tl -> k T.OK ("FUNCTION" :: "ITERATED" :: outs) tl + | "DISCRIMINATOR" :: tl -> k T.OK ("DISCRIMINATOR" :: outs) tl + | _ -> k T.OO outs ins + +let main = + R.register_r step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.mli new file mode 100644 index 000000000..e69de29bb diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundCounters.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundCounters.ml index d85161fa4..4defad66e 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundCounters.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundCounters.ml @@ -1,11 +1,11 @@ -let step k ok outs ins = - if ok then k ok outs ins else +module T = RecommTypes +module R = RecommPccFor + +let step k st outs ins = + if st <> T.OO then k st outs ins else match ins with - | "SHIFT" :: tl -> k true ("SHIFT" :: outs) tl - | "MAXIMUM" :: tl -> k true ("MAXIMUM" :: outs) tl - | "MAXIMUN" :: tl -> k true ("MAXIMUM" :: outs) tl - | "ADDITION" :: tl -> k true ("ADDITION" :: outs) tl - | _ -> k ok outs ins + | "SHIFT" :: tl -> k T.OK ("SHIFT" :: outs) tl + | _ -> k T.OO outs ins let main = - RecommPccFor.register_r step + R.register_r step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsAttr.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsAttr.ml index cb7037f67..83c402ebb 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsAttr.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsAttr.ml @@ -1,10 +1,14 @@ -let step k ok outs ins = - if ok then k ok outs ins else +module T = RecommTypes +module R = RecommCheck + +let step k st outs ins = + if st = T.KO then k st 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 + | "main" :: tl -> k T.OK ("main" :: outs) tl + | "helper" :: tl -> k T.OK ("helper" :: outs) tl + | "basic" :: tl -> k T.OK ("basic" :: outs) tl + | "advanced" :: tl -> k T.OK ("advanced" :: outs) tl + | _ -> k T.OO outs ins let main = - RecommCheck.register_s step + R.register_s step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsMain.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsMain.ml index 82905b840..d308df8db 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsMain.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsMain.ml @@ -1,19 +1,24 @@ +module T = RecommTypes +module R = RecommCheck module D = RecommGcsAttr -let step k ok outs ins = - if ok then k ok outs ins else +let step k st outs ins = + if st = T.KO then k st 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 + | "iterators" :: tl -> k T.OK ("iterators" :: outs) tl + | "eliminations" :: tl -> k T.OK ("eliminations" :: outs) tl + | "eliminators" :: tl -> k T.OK ("eliminations" :: outs) tl + | "equalities" :: tl -> k T.OK ("equalities" :: outs) tl + | "destructions" :: tl -> k T.OK ("destructions" :: outs) tl + | "forward" :: "properties" :: tl -> k T.OK ("destructions" :: outs) tl + | "forward" :: "lemmas" :: tl -> k T.OK ("destructions" :: outs) tl + | "inversions" :: tl -> k T.OK ("inversions" :: outs) tl + | "inversion" :: "properties" :: tl -> k T.OK ("inversions" :: outs) tl + | "inversion" :: "lemmas" :: tl -> k T.OK ("inversions" :: outs) tl + | "inversion" :: tl -> k T.OK ("inversions" :: outs) tl + | "constructions" :: tl -> k T.OK ("constructions" :: outs) tl + | "properties" :: tl -> k T.OK ("constructions" :: outs) tl + | _ -> k T.KO outs ins let main = - RecommCheck.register_s step + R.register_s step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml index 8e1d810a2..091bb2d12 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml @@ -1,10 +1,12 @@ +module T = RecommTypes +module R = RecommCheck module D = RecommGcsMain -let step k ok outs ins = - if ok then k ok outs ins else +let step k st outs ins = + if st = T.KO then k st outs ins else match ins with - | "with" :: tl -> k ok ("with" :: outs) tl - | _ -> k true outs ins + | "with" :: tl -> k T.OK ("with" :: outs) tl + | _ -> k T.OO outs ins let main = - RecommCheck.register_s step + R.register_s step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll b/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll index 21cca9c6c..99ff840af 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll @@ -8,15 +8,18 @@ |] let heads = [| - "Advanved"; + "Advanced"; "Basic"; "Constructions"; "Forward"; "Destructions"; "Eliminations"; "Eliminators"; + "Equalities"; + "Helper"; "Inversion"; "Inversions"; + "Iterators"; "Main"; "Properties"; |] @@ -53,7 +56,7 @@ let CR = "\r" let SP = " " let NL = "\n" let SR = "*" -let OP = "(*" SP* +let OP = "(*" let CP = SR* "*)" let PP = CP SP* OP let WF = ['A'-'Z' 'a'-'z'] diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml index fe8bebe94..e0f3f1d70 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml @@ -4,8 +4,17 @@ let width = ref 78 let replace = ref false +let string_length_utf8 s = + let l = String.length s in + let rec aux r i = + if i >= l then r else + if '\x80' <= s.[i] && s.[i] <= '\xBF' + then aux (succ r) (succ i) else aux r (succ i) + in + l - aux 0 0 + let complete s = - let l = !width - String.length s - 6 in + let l = !width - string_length_utf8 s - 6 in if l < 0 then begin Printf.eprintf "overfull: %S\n" s; "" @@ -19,7 +28,7 @@ let out_src och = function | ET.Text s -> Printf.fprintf och "%s" s | ET.Mark s -> - Printf.fprintf och "(* %s**)" s + Printf.fprintf och "(* *%s*)" s | ET.Key (s1, s2) -> Printf.fprintf och "(* %s%s*)" s1 s2 | ET.Title ss -> diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommParser.mly b/matita/matita/contribs/lambdadelta/bin/recomm/recommParser.mly index 5686e747e..79512c7c4 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommParser.mly +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommParser.mly @@ -14,17 +14,21 @@ %% -inn_r: +sp: + | { "" } | SP { $1 } + +inn_r: | NL { $1 } | SW { $1 } | OT { $1 } inn: | inn_r { $1 } - | KW { $1 } - | CW { $1 } - | HW { $1 } + | SP { $1 } + | KW { $1 } + | CW { $1 } + | HW { $1 } inns_r: | inn_r { $1 } @@ -47,14 +51,27 @@ outs: | out { $1 } | out outs { $1 ^ $2 } -sw: - | HW { lc $1 } - | SW { lc $1 } +cc: + | CW { $1 } + | OT { $1 } + +cw: + | cc { $1 } + | cc cw { $1 ^ $2 } cws: | { [] } | SP { [] } - | SP CW cws { $2 :: $3 } + | SP cw cws { $2 :: $3 } + +sc: + | HW { lc $1 } + | SW { lc $1 } + | OT { $1 } + +sw: + | sc { $1 } + | sc sw { $1 ^ $2 } sws: | { [] } @@ -63,14 +80,15 @@ sws: 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 sp PP inns CP { ET.Mark $4 } + | OP sp KW inns CP { ET.Key ($3, $4) } + | OP sp CW cws CP { ET.Title ($3 :: $4) } + | OP sp HW sws CP { ET.Slice (lc $3 :: $4) } + | OP sp CP { ET.Other ($1, $2, $3) } + | OP sp inns_r CP { ET.Other ($1, $2 ^ $3, $4) } | OP SR inns CP { ET.Other ($1, $2 ^ $3, $4) } | OP SR SR inns CP { ET.Other ($1, $2 ^ $3 ^ $4, $5) } + | OP SP SR inns CP { ET.Mark $4 } src: | outs { ET.Text $1 } diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml index cdad8df55..41a787dbd 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml @@ -1,26 +1,28 @@ module EC = RecommCheck module ES = RecommStep +module ET = RecommTypes 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 k_exit k st out ins = + if st <> ET.OK then k ET.KO out ins else + k st out ins + +let k_for k st outs ins = + if st <> ET.OK then k ET.KO outs ins else + match ins with + | "FOR" :: tl -> !d_line (k_exit k) ET.OO ("FOR" :: outs) tl + | _ -> k ET.KO outs ins + +let k_or k st outs ins = + if st <> ET.OO then k st outs ins else + !r_line (k_for k) st outs ins + +let step k st outs ins = + if st = ET.KO then k st outs ins else + !d_line (k_or k) ET.OO outs ins let register_d = ES.register d_line diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml index de05255a5..cf09e52ce 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml @@ -1,22 +1,20 @@ module EC = RecommCheck module ES = RecommStep +module ET = RecommTypes 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 +let rec k_and k st outs ins = + if st <> ET.OK then k ET.KO outs ins else + match ins with + | "and" :: tl -> step k ET.OK ("and" :: outs) tl + | _ -> k ET.OK outs ins -and step k ok outs ins = - if ok then k ok outs ins else - !b_line (k_and k) ok outs ins +and step k st outs ins = + if st <> ET.OK then k st outs ins else + !b_line (k_and k) ET.OO outs ins let register_b = ES.register b_line diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsPar.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsPar.ml new file mode 100644 index 000000000..52a1c00f9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsPar.ml @@ -0,0 +1,17 @@ +module EC = RecommCheck +module ES = RecommStep +module ET = RecommTypes + +module D = RecommPcsAnd + +let p_line = ref ES.id + +let step k st outs ins = + if st = ET.KO then k st outs ins else + !p_line k ET.OO outs ins + +let register_p = + ES.register p_line + +let main = + EC.register_s step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsPar.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsPar.mli new file mode 100644 index 000000000..451e24226 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsPar.mli @@ -0,0 +1 @@ +val register_p: RecommTypes.step -> unit diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommStep.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommStep.mli index df91cd169..76003832a 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommStep.mli +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommStep.mli @@ -1,4 +1,3 @@ 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 index f2f8e87a9..7225e916e 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml @@ -26,4 +26,8 @@ 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 +type return = KO + | OK + | OO + +type step = (return, return * words * words) astep diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/sAttr.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/sAttr.mrc index 4daa8ba06..7d8aadcff 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/sAttr.mrc +++ b/matita/matita/contribs/lambdadelta/bin/recomm/sAttr.mrc @@ -1,4 +1,5 @@ check s "" false false advanced basic +helper main diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/sMain.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/sMain.mrc index 8ed0ff28d..fbb9e2dc5 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/sMain.mrc +++ b/matita/matita/contribs/lambdadelta/bin/recomm/sMain.mrc @@ -1,5 +1,7 @@ check s "GcsAttr" false true constructions, properties -inversions, inversion properties, inversion lemmas +inversions, inversion properties, inversion lemmas, inversion destructions, forward properties, forward lemmas +equalities eliminations, eliminators +iterators diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc index 1a7d1fbfb..ecd022556 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc +++ b/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc @@ -1,2 +1,2 @@ -check s "GcsMain" false true +check s "GcsMain" false false with diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma index 5e131af37..d54738f25 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma @@ -15,9 +15,9 @@ include "ground/arith/nat_plus.ma". include "ground/arith/nat_le.ma". -(* ORDER FOR NON-NEGATIVE INTEGERS ****************************************************) +(* ORDER FOR NON-NEGATIVE INTEGERS ******************************************) -(* Constructions with nplus ***********************************************************) +(* Constructions with nplus *************************************************) (*** monotonic_le_plus_l *) lemma nle_plus_bi_dx (m) (n1) (n2): n1 ≤ n2 → n1 + m ≤ n2 + m. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma index 44c3539b9..cb902736e 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma @@ -39,7 +39,7 @@ qed. (*** max_SS *) lemma nmax_succ_bi (n1) (n2): ↑(n1 ∨ n2) = (↑n1 ∨ ↑n2). #n1 #n2 -@trans_eq [3: @ntri_succ_bi | skip ] (**) (* rewrite fails because δ-expansion gets in the way *) +@trans_eq [3: @ntri_succ_bi | skip ] (* * rewrite fails because δ-expansion gets in the way *) H12 #H lapply (yle_inv_plus_bi_sn_inj … H) -H #Hmy2 -generalize in match H12; -H12 (**) (* rewrite in hyp *) +generalize in match H12; -H12 (* * rewrite in hyp *) >(yplus_lminus_sn_refl_sn … Hmy2) in ⊢ (%→?); (yplus_lminus_dx_refl_sn … Hnx1) in ⊢ (%→?); -Hnx1 #H diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma index 15e58fd55..04cd607c9 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma @@ -61,7 +61,7 @@ qed. (* Advanced constructions ***************************************************) -(* yminus_O1 *) +(*** yminus_O1 *) lemma ylminus_zero_sn (n): 𝟎 = 𝟎 - n. // qed. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt.ma index a76ccd946..e9531df33 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt.ma @@ -29,7 +29,7 @@ interpretation (* Basic destructions *******************************************************) -(* ylt_fwd_gen ylt_inv_Y2 *) +(*** ylt_fwd_gen ylt_inv_Y2 *) lemma ylt_des_gen_sn (x) (y): x < y → ∃m. x = yinj_nat m. #x #y * -x -y diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le.ma index 84edec50f..9c4939f47 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le.ma @@ -67,7 +67,7 @@ lemma nle_ylt_trans (m) (n) (z): (* Inversions with yle ******************************************************) -(* ylt_yle_false *) +(*** ylt_yle_false *) lemma ylt_ge_false (x) (y): x < y → y ≤ x → ⊥. /3 width=4 by yle_ylt_trans, ylt_inv_refl/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus.ma index 04e0c4c3c..7c7b64f1a 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus.ma @@ -19,7 +19,7 @@ include "ground/arith/ynat_lt.ma". (* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************) -(* Cobstructions with yle and ylminus **************************************) +(* Constructions with yle and ylminus ***************************************) (*** monotonic_ylt_minus_dx *) lemma ylt_lminus_bi_dx (o) (x) (y): diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus_plus.ma index 6a66bded3..c39589b99 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus_plus.ma @@ -17,7 +17,7 @@ include "ground/arith/ynat_lt_le_lminus.ma". (* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************) -(* Constructions with yle and ylminus and yplus ****************************) +(* Constructions with yle and ylminus and yplus *****************************) (*** ylt_plus2_to_minus_inj2 *) lemma ylt_plus_dx_dx_lminus_sn (o) (x) (y): diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_succ.ma index 73e38daeb..56a6dadc9 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_succ.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_succ.ma @@ -24,7 +24,7 @@ lemma ylt_le_succ_sn (x) (y): x < ∞ → ↑x ≤ y → x < y. /3 width=3 by ylt_yle_trans, ylt_succ_dx_refl/ qed. -(* Inversions and destructions on yle ***************************************) +(* Inversions with yle and ysucc ********************************************) (*** ylt_inv_le *) lemma ylt_inv_le_succ_sn (x) (y): diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_plus.ma index 8f8ecd3aa..06e7d0813 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_plus.ma @@ -88,7 +88,7 @@ lemma yplus_inv_plus_bi_23 (z) (x1) (x2) (y1) (y2): z < ∞ → x1 + z + y1 = x2 + z + y2 → x1 + y1 = x2 + y2. #z #x1 #x2 #y1 #y2 #Hz ysucc_inj >ysucc_inj