From e06774421eb3b8f4438a6876cc1ab4262ef16f6e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 6 Jun 2016 15:39:21 +0000 Subject: [PATCH] MaTeX: - notational macros for constants - notational macro for quantification of propositions matex.sty: - support for math mode - improved rendering of basic constructions test style sheets - some notational macros for legacy_1 --- matita/components/binaries/matex/engine.ml | 39 ++++---- matita/components/binaries/matex/matex.ml | 4 +- matita/components/binaries/matex/options.ml | 9 +- matita/components/binaries/matex/options.mli | 4 +- matita/components/binaries/matex/test/Make | 2 +- .../binaries/matex/test/legacy_1.conf.xml | 29 +++--- .../binaries/matex/test/legacy_1.sty | 34 ++++++- .../components/binaries/matex/test/matex.sty | 90 ++++++++++++------- 8 files changed, 144 insertions(+), 67 deletions(-) diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml index e9ec76e86..5793ab38f 100644 --- a/matita/components/binaries/matex/engine.ml +++ b/matita/components/binaries/matex/engine.ml @@ -51,19 +51,22 @@ let missing s = let mk_ptr st name = if G.is_global_id name then P.sprintf "%s.%s" st.i name else "" -let get_macro s = +let get_macro s l = let rec aux = function - | [] -> "", G.nan - | (r, m, a) :: _ when r = s -> m, a - | _ :: tl -> aux tl + | [] -> "" + | (r, m, a) :: _ when r = s && a = l -> m + | _ :: tl -> aux tl in - aux !G.macro + aux !G.macro_gref let get_head = function | C.Const c :: ts -> let s, _ = K.resolve_reference c in - let macro, arity = get_macro s in - if arity = L.length ts then Some (macro, ts) else begin missing s; None end + let macro = get_macro s (L.length ts) in + if macro <> "" then Some (macro, s, ts) else begin + if !G.log_missing then missing s; + None + end | _ -> None let proc_sort st is = function @@ -80,16 +83,20 @@ let rec proc_term st is = function let name = K.resolve_lref st.c m in T.Macro "LREF" :: T.arg name :: T.free (mk_ptr st name) :: is | C.Appl ts -> - let macro, ts = match get_head ts with - | Some (macro, ts) -> macro, ts - | None -> "APPL", ts - in - let riss = L.rev_map (proc_term st []) ts in - T.Macro macro :: T.mk_rev_args riss is + begin match get_head ts with + | Some (macro, s, ts) -> + let riss = L.rev_map (proc_term st []) ts in + T.Macro macro :: T.free s :: T.mk_rev_args riss is + | None -> + let riss = L.rev_map (proc_term st []) ts in + T.Macro "APPL" :: T.mk_rev_args riss is + end | C.Prod (s, w, t) -> let is_w = proc_term st [] w in - let is_t = proc_term {st with c=K.add_dec s w st.c} is t in - T.Macro "PROD" :: T.arg s :: T.free (mk_ptr st s) :: T.Group is_w :: is_t + let c = K.add_dec s w st.c in + let is_t = proc_term {st with c=c} is t in + let macro = if K.not_prop1 c t then "PROD" else "FALL" in + T.Macro macro :: T.arg s :: T.free (mk_ptr st s) :: T.Group is_w :: is_t | C.Lambda (s, w, t) -> let is_w = proc_term st [] w in let is_t = proc_term {st with c=K.add_dec s w st.c} is t in @@ -149,7 +156,7 @@ let mk_open st ris = T.free (scope st) :: T.free (mk_ptr st st.n) :: T.arg st.n :: T.Macro "OPEN" :: ris let mk_dec st kind w s ris = - let w = if !G.no_types then [] else w in + let w = if !G.no_types then [T.Macro "NONE"] else w in T.Group w :: T.free (mk_ptr st s) :: T.arg s :: T.Macro kind :: ris let mk_inferred st t ris = diff --git a/matita/components/binaries/matex/matex.ml b/matita/components/binaries/matex/matex.ml index 24775c0a6..454c0463a 100644 --- a/matita/components/binaries/matex/matex.ml +++ b/matita/components/binaries/matex/matex.ml @@ -27,6 +27,7 @@ let help_X = " Clear configuration and options" let help_a = " Log alpha-unconverted identifiers (default: no)" let help_g = " Global alpha-conversion (default: no)" let help_l = " Output the list of generated files in this file" +let help_m = " Log missing notational macros (default: no)" let help_p = " Omit types (default: no)" let help_t = " Test term transformations (default: no)" @@ -46,7 +47,7 @@ let init registry = end; G.alpha_type := R.get_list alpha_decode "matex.alpha.type"; G.alpha_sort := R.get_list alpha_decode "matex.alpha.sort"; - G.macro := R.get_list macro_decode "matex.macro" + G.macro_gref := R.get_list macro_decode "matex.notation.const" let is_registry s = F.check_suffix s ".conf.xml" @@ -75,6 +76,7 @@ begin try "-a", A.Set G.log_alpha, help_a; "-g", A.Set G.global_alpha, help_g; "-l", A.String set_list, help_l; + "-m", A.Set G.log_missing, help_m; "-p", A.Set G.no_types, help_p; "-t", A.Set G.test, help_t; ] process help diff --git a/matita/components/binaries/matex/options.ml b/matita/components/binaries/matex/options.ml index 3b4c39d41..81cf705ba 100644 --- a/matita/components/binaries/matex/options.ml +++ b/matita/components/binaries/matex/options.ml @@ -30,6 +30,8 @@ let default_global_alpha = false let default_log_alpha = false +let default_log_missing = false + let default_list_och = None let default_alpha = [] @@ -58,13 +60,15 @@ let global_alpha = ref default_global_alpha (* log alpha-unconverted identifiers let log_alpha = ref default_log_alpha (* log alpha-unconverted identifiers *) +let log_missing = ref default_log_missing (* log missing notational macros *) + let list_och = ref default_list_och (* output stream for list file *) let alpha_type = ref default_alpha (* data for type-based alpha-conversion *) let alpha_sort = ref default_alpha (* data for sort-based alpha-conversion *) -let macro = ref default_macro (* data eta-conversion and macro rendering *) +let macro_gref = ref default_macro (* data eta-conversion and constant rendering *) let is_global_id s = !global_alpha && s <> dno_id @@ -82,7 +86,8 @@ let clear () = no_types := default_no_types; global_alpha := default_global_alpha; log_alpha := default_log_alpha; + log_missing := default_log_missing; list_och := default_list_och; alpha_type := default_alpha; alpha_sort := default_alpha; - macro := default_macro + macro_gref := default_macro diff --git a/matita/components/binaries/matex/options.mli b/matita/components/binaries/matex/options.mli index 8a7bbb8a2..ec4694e71 100644 --- a/matita/components/binaries/matex/options.mli +++ b/matita/components/binaries/matex/options.mli @@ -29,13 +29,15 @@ val global_alpha: bool ref val log_alpha: bool ref +val log_missing: bool ref + val list_och: out_channel option ref val alpha_type: (string * string * string) list ref val alpha_sort: (string * string * string) list ref -val macro: (string * string * int) list ref +val macro_gref: (string * string * int) list ref val clear: unit -> unit diff --git a/matita/components/binaries/matex/test/Make b/matita/components/binaries/matex/test/Make index 14c1cbe22..654490e0e 100644 --- a/matita/components/binaries/matex/test/Make +++ b/matita/components/binaries/matex/test/Make @@ -1,2 +1,2 @@ -matex.sty +matex.sty legacy_1.sty ground_1.sty basic_1.sty objs.tex diff --git a/matita/components/binaries/matex/test/legacy_1.conf.xml b/matita/components/binaries/matex/test/legacy_1.conf.xml index 056d1dc31..e215669f8 100644 --- a/matita/components/binaries/matex/test/legacy_1.conf.xml +++ b/matita/components/binaries/matex/test/legacy_1.conf.xml @@ -1,17 +1,18 @@ - +
+ matita.lambdadelta.legacy_1.coq.defs.ex.ex.type LExAA 2 + matita.lambdadelta.legacy_1.coq.defs.ex2.ex2.type LExBA 3 + matita.lambdadelta.legacy_1.coq.defs.land.land.type LAndB 2 + matita.lambdadelta.legacy_1.coq.defs.or.or.type LOrB 2 + + matita.lambdadelta.legacy_1.coq.defs.eq.eq.type EQ 3 + matita.lambdadelta.legacy_1.coq.defs.le.le.type LE 2 + matita.lambdadelta.legacy_1.coq.defs.lt.type LT 2 + matita.lambdadelta.legacy_1.coq.defs.minus.minus.type Minus 2 + matita.lambdadelta.legacy_1.coq.defs.nat.S.type Succ 1 + matita.lambdadelta.legacy_1.coq.defs.not.type LNot 1 + matita.lambdadelta.legacy_1.coq.defs.plus.plus.type Plus 2 + matita.lambdadelta.legacy_1.coq.defs.pred.type Pred 1 +
diff --git a/matita/components/binaries/matex/test/legacy_1.sty b/matita/components/binaries/matex/test/legacy_1.sty index d33196fb2..10edd9b62 100644 --- a/matita/components/binaries/matex/test/legacy_1.sty +++ b/matita/components/binaries/matex/test/legacy_1.sty @@ -1,10 +1,42 @@ \NeedsTeXFormat{LaTeX2e}[1995/12/01] -\ProvidesPackage{lambdadelta_1}[2016/05/23 Notation for "cic:/matita/lambdadelta/legacy_1/"] +\ProvidesPackage{legacy_1}[2016/06/06 Notation for "cic:/matita/lambdadelta/legacy_1/"] +\RequirePackage{matex} +\RequirePackage{fdsymbol} \ExecuteOptions{} \ProcessOptions* +\let\OldSucc=\Succ + \makeatletter +\newcommand*\ld@and[1]{\setbinlink{\&}{#1}} +\newcommand*\ld@lex[1]{\setordlink{\exists}{#1}} +\newcommand*\ld@land[1]{\setrellink{\land}{#1}} +\newcommand*\ld@lor[1]{\setrellink{\lor}{#1}} + +\newcommand*\ld@eq[1]{\setrellink{=}{#1}} +\newcommand*\ld@le[1]{\setrellink{\le}{#1}} +\newcommand*\ld@lt[1]{\setrellink{<}{#1}} +\newcommand*\ld@minus[1]{\setbinlink{+}{#1}} +\newcommand*\ld@lnot[1]{\setoplink{\lnot}{#1}} +\newcommand*\ld@plus[1]{\setbinlink{-}{#1}} +\newcommand*\ld@pred[1]{\setoplink{\downspoon}{#1}} +\newcommand*\ld@succ[1]{\setoplink{\upspoon}{#1}} + +\newcommand*\LAndB[3]{#2\ld@land{#1}#3} +\newcommand*\LOrB[3]{#2\ld@lor{#1}#3} +\newcommand*\LExAA[3]{\ld@lex{#1}#3} +\newcommand*\LExBA[4]{\ld@lex{#1}#3\ld@and{#1}#4} + +\newcommand*\EQ[4]{#3\ld@eq{#1}#4} +\newcommand*\LE[3]{#2\ld@le{#1}#3} +\newcommand*\LT[3]{#2\ld@lt{#1}#3} +\newcommand*\Minus[3]{#2\ld@minus{#1}#3} +\newcommand*\LNot[2]{\ld@lnot{#1}#2} +\newcommand*\Plus[3]{#2\ld@plus{#1}#3} +\newcommand*\Pred[2]{\ld@pred{#1}#2} +\renewcommand*\Succ[2]{\ld@succ{#1}#2} + \makeatother \endinput diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty index a25d051cb..119dffd26 100644 --- a/matita/components/binaries/matex/test/matex.sty +++ b/matita/components/binaries/matex/test/matex.sty @@ -1,11 +1,20 @@ \NeedsTeXFormat{LaTeX2e}[1995/12/01] -\ProvidesPackage{matex}[2016/05/22 MaTeX Package] +\ProvidesPackage{matex}[2016/06/05 MaTeX Package] \RequirePackage{xcolor} +\RequirePackage{stix} \ExecuteOptions{} \ProcessOptions* \makeatletter +\newcommand*\ma@cast{\mathbin:} +\newcommand*\ma@abbr{\mathrel\eqdef} +\newcommand*\ma@prod{\mathord\Pi} +\newcommand*\ma@arrw{\mathrel\Rightarrow} +\newcommand*\ma@fall{\mathord\forall} +\newcommand*\ma@impl{\mathrel\supset} +\newcommand*\ma@case{\mathrel\questeq} + \definecolor{ma@black}{HTML}{000000} \definecolor{ma@blue}{HTML}{00005F} \definecolor{ma@purple}{HTML}{3F005F} @@ -25,6 +34,17 @@ \newcommand*\ma@settarget[2]{\hypertarget{obj:#2}{#1}} \newcommand*\ma@setlink[2]{\hyperlink{obj:#2}{#1}} +\newcommand*\ma@setopttarget[2]{\def\ma@tmp{#2}% + \mathord{\ifx\ma@tmp\empty #1\else\ma@settarget{#1}{#2}\fi}% +} +\newcommand*\ma@setoptlink[2]{\def\ma@tmp{#2}% + \mathord{\ifx\ma@tmp\empty #1\else\ma@setlink{#1}{#2}\fi}% +} + +\newcommand*\setordlink[2]{\mathord{\ma@setlink{#1}{#2}}} +\newcommand*\setoplink[2]{\mathop{\ma@setlink{#1}{#2}}} +\newcommand*\setbinlink[2]{\mathbin{\ma@setlink{#1}{#2}}} +\newcommand*\setrellink[2]{\mathrel{\ma@setlink{#1}{#2}}} \newcommand*\ObjIncNode{} \newcommand*\ObjNode{} @@ -32,10 +52,10 @@ \newcommand*\ma@thehead[3]{\ObjIncNode\textbf{#1 \ObjNode(\ma@settarget{#2}{#3})}\neverindent\par} \newcommand*\ma@theneck[1]{\textsl{#1}\neverindent\par} -\newenvironment{axiom}[2]{\ma@thehead{Axiom}{#1}{#2}}{\par} -\newenvironment{declaration}[2]{\ma@thehead{Declaration}{#1}{#2}}{\par} -\newenvironment{definition}[2]{}{\par} -\newenvironment{proposition}[2]{\ma@thehead{Proposition}{#1}{#2}}{\par} +\newenvironment{axiom}[2]{\ma@thehead{Axiom}{#1}{#2}$}{$\par} +\newenvironment{declaration}[2]{\ma@thehead{Declaration}{#1}{#2}$}{$\par} +\newenvironment{definition}[2]{$}{$\par} +\newenvironment{proposition}[2]{\ma@thehead{Proposition}{#1}{#2}$}{$\par} \newenvironment{proof}[2]{\ma@theneck{Proof}}{\par} \newenvironment{ma@step}[1]{\color{#1}}{\par} @@ -45,44 +65,52 @@ \ifx\ma@tmp\empty #4\let\ma@tmp=\ma@skip\else #1#2{#5}\let\ma@tmp=\ma@next\fi \ma@tmp #3#2#3#4% } - -\newcommand*\ma@space{ } +\newcommand*\ma@thop[1]{\mathop{#1}\allowbreak} +\newcommand*\ma@cm{\ma@thop{,}} +\newcommand*\ma@or{\mathbin\vert} +\newcommand*\ma@cp{)\allowbreak} \newcommand*\ma@arg[1]{#1} - -\newcommand*\ma@setopttarget[2]{\def\ma@tmp{#2}% - \ifx\ma@tmp\empty #1\else\ma@settarget{#1}{#2}\fi +\newcommand*\ma@args{(\ma@next\relax\ma@arg\ma@cm\ma@cp} +\newcommand*\ma@cases{\ma@next\relax\ma@arg\ma@or\relax} +\newcommand*\ma@bind{\ma@thop{}} + +\newcommand*\PROP{\mathord\mathrm{PROP}} +\newcommand*\CROP[1]{\mathord\mathrm{CROP}} +\newcommand*\TYPE[1]{\mathord\mathrm{TYPE}} +\newcommand*\LREF[2]{\ma@setoptlink{#1}{#2}} +\newcommand*\GREF[2]{\ma@setoptlink{\mathrm{#1}}{#2}} +\newcommand*\ABBR[4]{(\ma@setopttarget{#1}{#2}\ma@abbr #4\ma@cast #3)\ma@bind} +\newcommand*\ABST[3]{(\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind} +\newcommand*\PROD[3]{\def\ma@tmp{#2}% + \ifx\ma@tmp\empty #3\ma@arrw\else + (\ma@prod\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind\fi } - -\newcommand*\PROP{PROP} -\newcommand*\CROP[1]{CROP} -\newcommand*\TYPE[1]{TYPE} -\newcommand*\LREF[2]{\def\ma@tmp{#2}% - \ifx\ma@tmp\empty #1\else\ma@setlink{#1}{#2}\fi +\newcommand*\FALL[3]{\def\ma@tmp{#2}% + \ifx\ma@tmp\empty #3\ma@impl\else + (\ma@fall\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind\fi } -\newcommand*\GREF[2]{\ma@setlink{#1}{#2}} -\newcommand*\ABBR[4]{(D \ma@setopttarget{#1}{#2} #3 #4) } -\newcommand*\ABST[3]{(I \ma@setopttarget{#1}{#2} #3) } -\newcommand*\PROD[3]{(P \ma@setopttarget{#1}{#2} #3) } -\newcommand*\APPL{(A)\ma@next\ma@space\ma@arg\ma@space\relax} -\newcommand*\CASE[3]{(C #1 #2 #3)\ma@next\ma@space\ma@arg\ma@space\relax} +\newcommand*\APPL[1]{#1\ma@args} +\newcommand*\CASE[3]{(#3\ma@cast #1)\ma@case\ma@cases} +\newcommand*\NONE{\mathrm{(omitted)}} +\newcommand*\ma@term[1]{$#1$} \newcommand*\ma@with{ with } \newcommand*\ma@comma{, } \newcommand*\ma@stop{.\end{ma@step}} \newcommand*\ma@head[6]{\def\ma@tmp{#5}% - \ifx\ma@tmp\empty\begin{ma@step}{#1}\textbf{\ma@setopttarget{#2}{#3}}% - \else\begin{ma@step}{#4}\textbf{\ma@setopttarget{#5}{#6}}% + \ifx\ma@tmp\empty\begin{ma@step}{#1}$\mathbf{\ma@setopttarget{#2}{#3}}$% + \else\begin{ma@step}{#4}$\mathbf{\ma@setopttarget{#5}{#6}}$% \fi } -\newcommand*\ma@tail{\ma@next\ma@with\ma@arg\ma@comma\ma@stop} +\newcommand*\ma@tail{\ma@next\ma@with\ma@term\ma@comma\ma@stop} -\newcommand*\EXIT[1]{\ma@head{}{}{}{\ma@exit}{end}{} of block #1\ma@stop} +\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 #3\ma@stop} -\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{}{\ma@fwd}{#1}{#2} has 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} +\newcommand*\PRIM[3]{\ma@head{}{}{}{\ma@prim}{#1}{#2} will have type $#3$\ma@stop} +\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{}{\ma@fwd}{#1}{#2} has 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} \makeatother -- 2.39.2