(* generic term processing *)
+let rec rename s = function
+ | [] -> s
+ | (s1, s2) :: _ when s1 = s -> s2
+ | _ :: tl -> rename s tl
+
+let mk_lname s = s
+
+let mk_gname s =
+ rename s !G.alpha_gref
+
let mk_ptr st name =
if G.is_global_id name then P.sprintf "%s.%s" st.i name else ""
| C.Meta _
| C.Implicit _ -> malformed "T2"
| C.Rel m ->
- let name = K.resolve_lref st.c m in
- T.Macro "LREF" :: T.arg name :: T.free (mk_ptr st name) :: is
+ let s = K.resolve_lref st.c m in
+ T.Macro "LREF" :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: is
| C.Appl ts ->
begin match get_head ts with
| Some (macro, s, ts) ->
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
+ T.Macro macro :: T.arg (mk_lname 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.Macro "ABST" :: T.arg s :: T.free (mk_ptr st s) :: T.Group is_w :: is_t
+ T.Macro "ABST" :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: T.Group is_w :: is_t
| C.LetIn (s, w, v, t) ->
let is_w = proc_term st [] w in
let is_v = proc_term st [] v in
let is_t = proc_term {st with c=K.add_def s w v st.c} is t in
- T.Macro "ABBR" :: T.arg s :: T.free (mk_ptr st s) :: T.Group is_w :: T.Group is_v :: is_t
+ T.Macro "ABBR" :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: T.Group is_w :: T.Group is_v :: is_t
| C.Sort s ->
proc_sort st is s
| C.Const c ->
let s, name = K.resolve_reference c in
- T.Macro "GREF" :: T.arg name :: T.free s :: is
+ T.Macro "GREF" :: T.arg (mk_gname name) :: 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
let is_v = proc_term st [] v in
- let riss = L.rev_map (proc_term st []) ts in
- T.Macro "CASE" :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss is
+ let riss = X.rev_mapi (proc_case st [] w) K.fst_con ts in
+ let macro = if ts = [] then "CAZE" else "CASE" in
+ T.Macro macro :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss is
+
+and proc_case st is w i t =
+ let v = R.mk_constructor i w in
+ let is_v = proc_term st [] (C.Const v) in
+ let is_t = proc_term st [] t in
+ T.Macro "PAIR" :: T.Group is_v :: T.Group is_t :: is
let proc_term st is t = try proc_term st is t with
| E.ObjectNotFound _
let mk_open st ris =
if st.n = "" then ris else
- T.free (scope st) :: T.free (mk_ptr st st.n) :: T.arg st.n :: T.Macro "OPEN" :: ris
+ T.free (scope st) :: T.free (mk_ptr st st.n) :: T.arg (mk_lname st.n) :: T.Macro "OPEN" :: ris
let mk_dec st kind w s ris =
- 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 w = if !G.no_types then [] else w in
+ T.Group w :: T.free (mk_ptr st s) :: T.arg (mk_lname s) :: T.Macro kind :: ris
let mk_inferred st t ris =
let u = typeof st t in
let st = init ss in
let tt = N.process_top_term s t in (* alpha-conversion *)
let is = [T.Macro "end"; T.arg item] in
- note :: T.Macro "begin" :: T.arg item :: T.arg s :: T.free ss :: proc_term st is tt
+ note :: T.Macro "begin" :: T.arg item :: T.arg (mk_gname s) :: T.free ss :: proc_term st is tt
let proc_top_proof s ss t =
let st = init ss in
let t0 = A.process_top_term s t in (* anticipation *)
let tt = N.process_top_term s t0 in (* alpha-conversion *)
- let ris = [T.free ss; T.arg s; T.arg "proof"; T.Macro "begin"; note] in
+ let ris = [T.free ss; T.arg (mk_gname s); T.arg "proof"; T.Macro "begin"; note] in
L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof st ris tt)
let open_out_tex s =
| [] -> a
| hd :: tl -> foldi_left mapi (succ i) (mapi i a hd) tl
+let rec rev_mapi mapi i l =
+ let map i a hd = mapi i hd :: a in
+ foldi_left map i [] l
+
let rec rev_map_append map l r = match l with
| [] -> r
| hd :: tl -> rev_map_append map tl (map hd :: r)
val foldi_left: (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
+val rev_mapi: (int -> 'b -> 'a) -> int -> 'b list -> 'a list
+
val rev_map_append: ('a -> 'b) -> 'a list -> 'b list -> 'b list
let u1 = mk_type_universe "1" in
E.add_lt_constraint ~acyclic:true u0 u1
-let fst_var = 1
+let fst_var = 1 (* first variable *)
-let snd_var = 2
+let snd_var = 2 (* second variable *)
+
+let fst_con = 1 (* first constructor *)
let appl ts = C.Appl ts
let alpha_decode = R.triple R.string R.string R.string
+let const_decode = R.pair R.string R.string
+
let macro_decode = R.triple R.string R.string R.int
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.alpha_gref := R.get_list const_decode "matex.alpha.gref";
G.macro_gref := R.get_list macro_decode "matex.notation.const"
let is_registry s =
let alpha_sort = ref default_alpha (* data for sort-based alpha-conversion *)
+let alpha_gref = ref default_alpha (* data for constant renaming *)
+
let macro_gref = ref default_macro (* data eta-conversion and constant rendering *)
let is_global_id s =
list_och := default_list_och;
alpha_type := default_alpha;
alpha_sort := default_alpha;
+ alpha_gref := default_alpha;
macro_gref := default_macro
val alpha_sort: (string * string * string) list ref
+val alpha_gref: (string * string) list ref
+
val macro_gref: (string * string * int) list ref
val clear: unit -> unit
<key name="sort">Prop x H</key>
<key name="sort">Type[cic:/matita/pts/Type0.univ] f a</key>
+
+ <key name="gref">clt_wf__q_ind q_ind_aux</key>
+
+ <key name="gref">ex1__leq_sort_SS leq_sort_SS_aux</key>
+
+ <key name="gref">flt_wf__q_ind q_ind_aux</key>
+
+ <key name="gref">llt_wf__q_ind q_ind_aux</key>
+
+ <key name="gref">nf2_gen__nf2_gen_aux nf2_gen_aux</key>
+
+ <key name="gref">pc3_ind_left__pc3_left_pc3 pc3_left_pc3_aux</key>
+ <key name="gref">pc3_ind_left__pc3_left_pr3 pc3_left_pr3_aux</key>
+ <key name="gref">pc3_ind_left__pc3_left_sym pc3_left_sym_aux</key>
+ <key name="gref">pc3_ind_left__pc3_left_trans pc3_left_trans_aux</key>
+ <key name="gref">pc3_ind_left__pc3_pc3_left pc3_pc3_left_aux</key>
+ <key name="gref">pc3_wcpr0__pc3_wcpr0_t_aux pc3_wcpr0_t_aux</key>
+
+ <key name="gref">pr0_confluence__pr0_cong_delta pr0_cong_delta_aux</key>
+ <key name="gref">pr0_confluence__pr0_cong_upsilon_cong pr0_cong_upsilon_cong_aux</key>
+ <key name="gref">pr0_confluence__pr0_cong_upsilon_delta pr0_cong_upsilon_delta_aux</key>
+ <key name="gref">pr0_confluence__pr0_cong_upsilon_refl pr0_cong_upsilon_refl_aux</key>
+ <key name="gref">pr0_confluence__pr0_cong_upsilon_zeta pr0_cong_upsilon_zeta_aux</key>
+ <key name="gref">pr0_confluence__pr0_delta_delta pr0_delta_delta_aux</key>
+ <key name="gref">pr0_confluence__pr0_delta_tau pr0_delta_tau_aux</key>
+ <key name="gref">pr0_confluence__pr0_upsilon_upsilon pr0_upsilon_upsilon_aux</key>
+
+ <key name="gref">pr2_confluence__pr2_delta_delta pr2_delta_delta_aux</key>
+ <key name="gref">pr2_confluence__pr2_free_delta pr2_free_delta_aux</key>
+ <key name="gref">pr2_confluence__pr2_free_free pr2_free_free_aux</key>
+
+ <key name="gref">sc3_props__sc3_sn3_abst sc3_sn3_abst_aux</key>
+
+ <key name="gref">terms_props__bind_dec bind_dec_aux</key>
+ <key name="gref">terms_props__flat_dec flat_dec_aux</key>
+ <key name="gref">terms_props__kind_dec kind_dec_aux</key>
+
+ <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>
+
</section>
<!--
matita.lambdadelta.basic_1.A.defs.A.AHead.type
<?xml version="1.0" encoding="utf-8"?>
<helm_registry>
<!--
-matita.lambdadelta.ground_1.blt.defs.blt.blt.type
-matita.lambdadelta.ground_1.plist.defs.papp.papp.type
-matita.lambdadelta.ground_1.plist.defs.PConsTail.PConsTail.type
-matita.lambdadelta.ground_1.plist.defs.PList.PCons.type
-matita.lambdadelta.ground_1.plist.defs.Ss.Ss.type
-matita.lambdadelta.ground_1.types.defs.and3.and3.type
matita.lambdadelta.ground_1.types.defs.ex2_2.ex2_2.type
matita.lambdadelta.ground_1.types.defs.ex2_3.ex2_3.type
matita.lambdadelta.ground_1.types.defs.ex_2.ex_2.type
matita.lambdadelta.ground_1.types.defs.ex6_6.ex6_6.type
matita.lambdadelta.ground_1.types.defs.or3.or3.type
matita.lambdadelta.ground_1.types.defs.or4.or4.type
+matita.lambdadelta.ground_1.types.defs.and3.and3.type
+
+matita.lambdadelta.ground_1.blt.defs.blt.blt.type
+matita.lambdadelta.ground_1.plist.defs.papp.papp.type
+matita.lambdadelta.ground_1.plist.defs.PConsTail.PConsTail.type
+matita.lambdadelta.ground_1.plist.defs.PList.PCons.type
+matita.lambdadelta.ground_1.plist.defs.Ss.Ss.type
-->
</helm_registry>
\NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{matex}[2016/06/05 MaTeX Package]
+\ProvidesPackage{matex}[2016/06/12 MaTeX Package]
\RequirePackage{xcolor}
\RequirePackage{stix}
\ExecuteOptions{}
\newcommand*\ma@fall{\mathord\forall}
\newcommand*\ma@impl{\mathrel\supset}
\newcommand*\ma@case{\mathrel\questeq}
+\newcommand*\ma@caze{\mathrel\mapsto}
+\newcommand*\ma@pair{\mathbin\mapsto}
\definecolor{ma@black}{HTML}{000000}
\definecolor{ma@blue}{HTML}{00005F}
\newcommand*\ma@cm{\ma@thop{,}}
\newcommand*\ma@or{\mathbin\vert}
\newcommand*\ma@cp{)\allowbreak}
+\newcommand*\ma@qm{\mathord{?}}
\newcommand*\ma@arg[1]{#1}
\newcommand*\ma@args{(\ma@next\relax\ma@arg\ma@cm\ma@cp}
\newcommand*\ma@cases{\ma@next\relax\ma@arg\ma@or\relax}
(\ma@fall\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind\fi
}
\newcommand*\APPL[1]{#1\ma@args}
-\newcommand*\CASE[3]{(#3\ma@cast #1)\ma@case\ma@cases}
-\newcommand*\NONE{\mathrm{(omitted)}}
+\newcommand*\CASE[3]{#3\ma@case\ma@cases}
+\newcommand*\CAZE[3]{#3\ma@caze(\ma@qm\ma@cast #2)\ma@cases}
+\newcommand*\PAIR[2]{#1\ma@pair #2}
\newcommand*\ma@term[1]{$#1$}
\newcommand*\ma@with{ with }
\fi
}
\newcommand*\ma@tail{\ma@next\ma@with\ma@term\ma@comma\ma@stop}
+\newcommand*\ma@type[1]{\def\ma@tmp{#1}%
+ \ifx\ma@tmp\empty\mathrm{(omitted)}\else #1\fi
+}
\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*\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}
projects / helm.git / commitdiff