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
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
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 =
let help_a = " Log alpha-unconverted identifiers (default: no)"
let help_g = " Global alpha-conversion (default: no)"
let help_l = "<file> 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)"
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"
"-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
let default_log_alpha = false
+let default_log_missing = false
+
let default_list_och = None
let default_alpha = []
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
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
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
-matex.sty
+matex.sty legacy_1.sty ground_1.sty basic_1.sty
objs.tex
<?xml version="1.0" encoding="utf-8"?>
<helm_registry>
-<!--
-matita.lambdadelta.legacy_1.coq.defs.eq.eq.type
-matita.lambdadelta.legacy_1.coq.defs.ex2.ex2.type
-matita.lambdadelta.legacy_1.coq.defs.ex.ex.type
-matita.lambdadelta.legacy_1.coq.defs.land.land.type
-matita.lambdadelta.legacy_1.coq.defs.le.le.type
-matita.lambdadelta.legacy_1.coq.defs.lt.type
-matita.lambdadelta.legacy_1.coq.defs.minus.minus.type
-matita.lambdadelta.legacy_1.coq.defs.nat.S.type
-matita.lambdadelta.legacy_1.coq.defs.not.type
-matita.lambdadelta.legacy_1.coq.defs.or.or.type
-matita.lambdadelta.legacy_1.coq.defs.plus.plus.type
-matita.lambdadelta.legacy_1.coq.defs.pred.type
--->
+ <section name="matex.notation">
+ <key name="const">matita.lambdadelta.legacy_1.coq.defs.ex.ex.type LExAA 2</key>
+ <key name="const">matita.lambdadelta.legacy_1.coq.defs.ex2.ex2.type LExBA 3</key>
+ <key name="const">matita.lambdadelta.legacy_1.coq.defs.land.land.type LAndB 2</key>
+ <key name="const">matita.lambdadelta.legacy_1.coq.defs.or.or.type LOrB 2</key>
+
+ <key name="const">matita.lambdadelta.legacy_1.coq.defs.eq.eq.type EQ 3</key>
+ <key name="const">matita.lambdadelta.legacy_1.coq.defs.le.le.type LE 2</key>
+ <key name="const">matita.lambdadelta.legacy_1.coq.defs.lt.type LT 2</key>
+ <key name="const">matita.lambdadelta.legacy_1.coq.defs.minus.minus.type Minus 2</key>
+ <key name="const">matita.lambdadelta.legacy_1.coq.defs.nat.S.type Succ 1</key>
+ <key name="const">matita.lambdadelta.legacy_1.coq.defs.not.type LNot 1</key>
+ <key name="const">matita.lambdadelta.legacy_1.coq.defs.plus.plus.type Plus 2</key>
+ <key name="const">matita.lambdadelta.legacy_1.coq.defs.pred.type Pred 1</key>
+ </section>
</helm_registry>
\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
\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}
\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{}
\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}
\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
projects / helm.git / commitdiff