- matex: notational macros for 0-ary constants

- stylesheets and Makefiles: minor improvements

diff --git a/matita/components/binaries/matex/Makefile b/matita/components/binaries/matex/Makefile
index b3cc515d2ef748a01192eedb789efdb38fad7816..b437afb5b00925671ed2fc3420343e49d847b067 100644 (file)
--- a/matita/components/binaries/matex/Makefile
+++ b/matita/components/binaries/matex/Makefile
@@ -5,6 +5,7 @@ REQUIRES = helm-ng_library
 
 include ../Makefile.common
 
+MATEX    = ./$(EXEC).native
 PROBE    = ../probe/probe.native
 REGISTRY = $(RT_BASE_DIR)/matita.conf.xml \
            test/legacy_1.conf.xml test/ground_1.conf.xml test/basic_1.conf.xml
@@ -15,12 +16,12 @@ DEVEL = ../../../matita/contribs/lambdadelta/basic_1/
 
 test: test/$(SRCS)
 
-test/$(OBJS): $(REGISTRY)
+test/$(OBJS): $(REGISTRY) Makefile
        @echo probe: $(DEVEL)
        $(H)$(PROBE) $(REGISTRY) -g $(DEVEL) -os > $@
 
-test/$(SRCS): test/$(OBJS) $(REGISTRY) ./matex.native
+test/$(SRCS): test/$(OBJS) $(REGISTRY) $(MATEX) Makefile
        @echo MaTeX: processing $<
-       $(H)./matex.native -O test -l $(SRCS) -a -g -p $(REGISTRY) `cat $<`
+       $(H)$(MATEX) -O test -l $(SRCS) -a -g -p $(REGISTRY) `cat $<`
 
 .PHONY: test

diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml
index c3d50d5e74fdd4bf2c8a5e481b11d3f50a08e67d..23e6f687acab2b104029e6f4e7bb8341342371eb 100644 (file)
--- a/matita/components/binaries/matex/engine.ml
+++ b/matita/components/binaries/matex/engine.ml
@@ -63,7 +63,9 @@ let mk_ptr st name =
 
 let get_macro s l =
    let rec aux = function
-      | []                                    -> "", 0
+      | []                                    -> 
+         if !G.log_missing then missing s l;
+         "", 0
       | (r, m, a, x) :: _ when r = s && a = l -> m, x
       | _ :: tl                               -> aux tl
    in
@@ -75,9 +77,7 @@ let get_head = function
       let l = L.length ts in
       let macro, x = get_macro s l in
       begin match macro with      
-         | ""     -> 
-            if !G.log_missing then missing s l;
-            None
+         | ""
          | "APPL" -> None
          | _      -> 
             let ts1, ts2 = X.split_at x ts in
@@ -131,7 +131,11 @@ let rec proc_term st is = function
       proc_sort st is s
    | C.Const c              ->
       let s, name = K.resolve_reference c in
-      T.Macro "GREF" :: T.arg (mk_gname name) :: T.free s :: is
+      let macro, _ = get_macro s 0 in
+      if macro = "" || macro = "APPL" then
+         T.Macro "GREF" :: T.arg (mk_gname name) :: T.free s :: is
+      else
+         T.Macro macro :: T.free s :: is
    | C.Match (w, u, v, ts)  ->
       let is_w = proc_term st [] (C.Const w) in
       let is_u = proc_term st [] u in

diff --git a/matita/components/binaries/matex/test/Makefile b/matita/components/binaries/matex/test/Makefile
index cb19e9a6d290e9797dd69eac37180229341202f0..fe3b021c7e5d0130e2a776b439d24ef32614d315 100644 (file)
--- a/matita/components/binaries/matex/test/Makefile
+++ b/matita/components/binaries/matex/test/Makefile
@@ -6,7 +6,7 @@ UNLOG  = ./unlog.pl
 
 MAIN = test
 
-SOURCES = $(shell cat Make) $(shell cat Make.srcs)
+SOURCES = $(shell cat Make) $(shell cat Make.srcs) Makefile
 
 all: $(MAIN).dvi 
 

diff --git a/matita/components/binaries/matex/test/basic_1.conf.xml b/matita/components/binaries/matex/test/basic_1.conf.xml
index 10095057bb45b09ad21802e6bacd81fb6afc1aa2..3d6f14619e3be90231c5695f773ddceb62fd1352 100644 (file)
--- a/matita/components/binaries/matex/test/basic_1.conf.xml
+++ b/matita/components/binaries/matex/test/basic_1.conf.xml
@@ -168,13 +168,12 @@
     <key name="gref">tlt_wf__q_ind q_ind_aux</key>
     <key name="gref">tslt_wf__q_ind q_ind_aux</key>
     <key name="gref">ty3_nf2_gen__ty3_nf2_inv_abst_aux ty3_nf2_inv_abst_aux</key>
+    <key name="gref">ty3_nf2_inv_abst_premise H_ty3_nf2_inv_abst</key>
   </section>
   <section name="matex.notation">
     <key name="const">$(devel.basic1).A.defs.A.AHead.type To 2 0</key>
     <key name="const">$(devel.basic1).A.defs.A.ASort.type AtomB 2 0</key>
-<!--
-$(devel.basic1).A.fwd.A_rect.A_rect.type 0</key>
--->
+    <key name="const">$(devel.basic1).A.fwd.A_rect.A_rect.type APPL 4 0</key>
     <key name="const">$(devel.basic1).aplus.defs.aplus.aplus.type PlusA 3 0</key>
     <key name="const">$(devel.basic1).app.defs.app1.app1.type Shift 2 0</key>
     <key name="const">$(devel.basic1).app.defs.cbk.cbk.type Level 1 0</key>
@@ -187,9 +186,7 @@ $(devel.basic1).A.fwd.A_rect.A_rect.type 0</key>
     <key name="const">$(devel.basic1).C.defs.clt.type LT 2 0</key>
     <key name="const">$(devel.basic1).C.defs.CTail.CTail.type THead 3 0</key>
     <key name="const">$(devel.basic1).C.defs.cweight.cweight.type WeightA 1 0</key>
-<!--
-$(devel.basic1).C.fwd.C_rect.C_rect.type 0</key>
--->
+    <key name="const">$(devel.basic1).C.fwd.C_rect.C_rect.type APPL 4 0</key>
     <key name="const">$(devel.basic1).cimp.defs.cimp.type SubEq 2 0</key>
     <key name="const">$(devel.basic1).clear.defs.clear.clear.type Drop 2 0</key>
     <key name="const">$(devel.basic1).clen.defs.clen.clen.type Length 1 0</key>
@@ -247,9 +244,7 @@ $(devel.basic1).C.fwd.C_rect.C_rect.type 0</key>
     <key name="const">$(devel.basic1).T.defs.T.TLRef.type LRef 1 0</key>
     <key name="const">$(devel.basic1).T.defs.T.TSort.type AtomA 1 0</key>
     <key name="const">$(devel.basic1).T.defs.tweight.tweight.type WeightA 1 0</key>
-<!--
-$(devel.basic1).T.fwd.T_rect.T_rect.type 0</key>
--->
+    <key name="const">$(devel.basic1).T.fwd.T_rect.T_rect.type APPL 5 0</key>
     <key name="const">$(devel.basic1).tlist.defs.TApp.TApp.type CoConsA 2 0</key>
     <key name="const">$(devel.basic1).tlist.defs.THeads.THeads.type THead 3 0</key>
     <key name="const">$(devel.basic1).tlist.defs.TList.TCons.type ConsA 2 0</key>
@@ -261,9 +256,7 @@ $(devel.basic1).T.fwd.T_rect.T_rect.type 0</key>
     <key name="const">$(devel.basic1).tlt.defs.weight.type CoWeightA 1 0</key>
     <key name="const">$(devel.basic1).ty3.defs.ty3.ty3.type Type 4 0</key>
     <key name="const">$(devel.basic1).ty3.defs.tys3.tys3.type Type 4 0</key>
-<!--
-$(devel.basic1).ty3.nf2.ty3_nf2_inv_abst_premise.type 0</key>
--->
+    <key name="const">$(devel.basic1).ty3.nf2.ty3_nf2_inv_abst_premise.type APPL 3 0</key>
     <key name="const">$(devel.basic1).wcpr0.defs.wcpr0.wcpr0.type RStep 2 0</key>
     <key name="const">$(devel.basic1).wf3.defs.wf3.wf3.type Valid 3 0</key>
   </section>

diff --git a/matita/components/binaries/matex/test/macros_0.txt b/matita/components/binaries/matex/test/macros_0.txt
new file mode 100644 (file)
index 0000000..87156f6
--- /dev/null
+++ b/matita/components/binaries/matex/test/macros_0.txt
@@ -0,0 +1,50 @@
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.A.defs.A.AHead.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.A.defs.A.ASort.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.A.defs.A.A.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.A.fwd.A_rect.A_rect.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.C.defs.C.CHead.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.C.defs.C.CSort.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.C.defs.C.C.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.C.fwd.C_rect.C_rect.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.ex0.defs.gz.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.ex1.defs.ex1_c.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.ex1.defs.ex1_t.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.ex2.defs.ex2_c.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.ex2.defs.ex2_t.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.G.defs.G.G.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.T.defs.B.Abbr.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.T.defs.B.Abst.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.T.defs.B.B.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.T.defs.B.Void.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.T.defs.F.Appl.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.T.defs.F.Cast.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.T.defs.F.F.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.T.defs.K.Bind.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.T.defs.K.Flat.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.T.defs.K.K.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.T.defs.T.THead.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.T.defs.T.TLRef.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.T.defs.T.TSort.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.T.defs.T.T.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.T.fwd.T_rect.T_rect.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.tlist.defs.TList.TCons.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.tlist.defs.TList.TList.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.tlist.defs.TList.TNil.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.tlt.defs.wadd.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.tlt.defs.wadd.type (3)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.tlt.defs.weight_map.weight_map.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.tlt.defs.weight_map.weight_map.type (1)
+MaTeX: engine: missing macro for matita.lambdadelta.basic_1.ty3.nf2.ty3_nf2_inv_abst_premise.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.ground_1.plist.defs.PList.PCons.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.ground_1.plist.defs.PList.PList.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.ground_1.plist.defs.PList.PNil.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.legacy_1.coq.defs.bool.bool.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.legacy_1.coq.defs.bool.false.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.legacy_1.coq.defs.bool.true.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.legacy_1.coq.defs.nat.nat.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.legacy_1.coq.defs.nat.O.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.legacy_1.coq.defs.nat.S.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.legacy_1.coq.defs.True.True.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.legacy_1.coq.props.lt_n_Sn.type (0)
+MaTeX: engine: missing macro for matita.lambdadelta.legacy_1.preamble.False.False.type (0)
+MaTeX: processing test/Make.objs

diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty
index 7d6ae277e8b678f41181428b31e309b2ab5a6a1e..eab67601843ba804c6b4110a74d114d15b7cbaa1 100644 (file)
--- a/matita/components/binaries/matex/test/matex.sty
+++ b/matita/components/binaries/matex/test/matex.sty
@@ -73,7 +73,7 @@
 \newenvironment{assumption}[2]{\ma@thehead{Assumption}{has type}{#1}{#2}$}{$\par}
 \newenvironment{axiom}[2]{\ma@thehead{Axiom}{states}{#1}{#2}$}{$\par}
 \newenvironment{declaration}[2]{\ma@thehead{Definition}{of type}{#1}{#2}$}{$\par}
-\newenvironment{definition}[2]{\ma@theneck{is defined as}$}{$\par}
+\newenvironment{definition}[2]{\ma@theneck{is defined as}$}{$.\par}
 \newenvironment{proposition}[2]{\ma@thehead{Proposition}{stating}{#1}{#2}$}{$\par}
 \newenvironment{proof}[2]{\ma@theneck{is proved by}}{\par}
 \newenvironment{ma@step}[1]{\color{#1}}{\par}
@@ -126,8 +126,8 @@
 
 \newcommand*\EXIT[1]{\ma@head{\ma@exit}{end}{}{}{}{} of block #1\ma@stop}
 \newcommand*\OPEN[3]{\ma@head{}{}{}{\ma@open}{#1}{#2} is this block #3\ma@stop}
-\newcommand*\PRIM[3]{\ma@head{}{}{}{\ma@prim}{#1}{#2} will have type $\ma@type{#3}$\ma@stop}
-\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{}{\ma@fwd}{#1}{#2} has type $\ma@type{#3}$\par}
+\newcommand*\PRIM[3]{\ma@head{}{}{}{\ma@prim}{#1}{#2} will have type: $\ma@type{#3}$\ma@stop}
+\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{}{\ma@fwd}{#1}{#2} has type: $\ma@type{#3}$\par}
 \newcommand*\BODY[1]{being $#1$\ma@stop}
 \newcommand*\STEP[1]{by $#1$\ma@tail}
 \newcommand*\DEST[1]{by cases on $#1$\ma@tail}