From 0e2836b432e8d1a10262836e160a5dd3cfb82c1e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 4 Jul 2016 17:30:45 +0000 Subject: [PATCH] - matex: notational macros for 0-ary constants - stylesheets and Makefiles: minor improvements --- matita/components/binaries/matex/Makefile | 7 +-- matita/components/binaries/matex/engine.ml | 14 ++++-- .../components/binaries/matex/test/Makefile | 2 +- .../binaries/matex/test/basic_1.conf.xml | 17 ++----- .../binaries/matex/test/macros_0.txt | 50 +++++++++++++++++++ .../components/binaries/matex/test/matex.sty | 6 +-- 6 files changed, 72 insertions(+), 24 deletions(-) create mode 100644 matita/components/binaries/matex/test/macros_0.txt diff --git a/matita/components/binaries/matex/Makefile b/matita/components/binaries/matex/Makefile index b3cc515d2..b437afb5b 100644 --- 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 c3d50d5e7..23e6f687a 100644 --- 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 cb19e9a6d..fe3b021c7 100644 --- 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 10095057b..3d6f14619 100644 --- a/matita/components/binaries/matex/test/basic_1.conf.xml +++ b/matita/components/binaries/matex/test/basic_1.conf.xml @@ -168,13 +168,12 @@ tlt_wf__q_ind q_ind_aux tslt_wf__q_ind q_ind_aux ty3_nf2_gen__ty3_nf2_inv_abst_aux ty3_nf2_inv_abst_aux + ty3_nf2_inv_abst_premise H_ty3_nf2_inv_abst
$(devel.basic1).A.defs.A.AHead.type To 2 0 $(devel.basic1).A.defs.A.ASort.type AtomB 2 0 - + $(devel.basic1).A.fwd.A_rect.A_rect.type APPL 4 0 $(devel.basic1).aplus.defs.aplus.aplus.type PlusA 3 0 $(devel.basic1).app.defs.app1.app1.type Shift 2 0 $(devel.basic1).app.defs.cbk.cbk.type Level 1 0 @@ -187,9 +186,7 @@ $(devel.basic1).A.fwd.A_rect.A_rect.type 0 $(devel.basic1).C.defs.clt.type LT 2 0 $(devel.basic1).C.defs.CTail.CTail.type THead 3 0 $(devel.basic1).C.defs.cweight.cweight.type WeightA 1 0 - + $(devel.basic1).C.fwd.C_rect.C_rect.type APPL 4 0 $(devel.basic1).cimp.defs.cimp.type SubEq 2 0 $(devel.basic1).clear.defs.clear.clear.type Drop 2 0 $(devel.basic1).clen.defs.clen.clen.type Length 1 0 @@ -247,9 +244,7 @@ $(devel.basic1).C.fwd.C_rect.C_rect.type 0 $(devel.basic1).T.defs.T.TLRef.type LRef 1 0 $(devel.basic1).T.defs.T.TSort.type AtomA 1 0 $(devel.basic1).T.defs.tweight.tweight.type WeightA 1 0 - + $(devel.basic1).T.fwd.T_rect.T_rect.type APPL 5 0 $(devel.basic1).tlist.defs.TApp.TApp.type CoConsA 2 0 $(devel.basic1).tlist.defs.THeads.THeads.type THead 3 0 $(devel.basic1).tlist.defs.TList.TCons.type ConsA 2 0 @@ -261,9 +256,7 @@ $(devel.basic1).T.fwd.T_rect.T_rect.type 0 $(devel.basic1).tlt.defs.weight.type CoWeightA 1 0 $(devel.basic1).ty3.defs.ty3.ty3.type Type 4 0 $(devel.basic1).ty3.defs.tys3.tys3.type Type 4 0 - + $(devel.basic1).ty3.nf2.ty3_nf2_inv_abst_premise.type APPL 3 0 $(devel.basic1).wcpr0.defs.wcpr0.wcpr0.type RStep 2 0 $(devel.basic1).wf3.defs.wf3.wf3.type Valid 3 0
diff --git a/matita/components/binaries/matex/test/macros_0.txt b/matita/components/binaries/matex/test/macros_0.txt new file mode 100644 index 000000000..87156f699 --- /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 7d6ae277e..eab676018 100644 --- 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} -- 2.39.2