From f462726eaf4edb5852851ec5d265cdafe9d3a78d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 12 Jun 2016 17:36:44 +0000 Subject: [PATCH] - improved support for case - support for renaming constants --- matita/components/binaries/matex/engine.ml | 43 +++++++++++++------ matita/components/binaries/matex/ground.ml | 4 ++ matita/components/binaries/matex/ground.mli | 2 + matita/components/binaries/matex/kernel.ml | 6 ++- matita/components/binaries/matex/matex.ml | 3 ++ matita/components/binaries/matex/options.ml | 3 ++ matita/components/binaries/matex/options.mli | 2 + .../binaries/matex/test/basic_1.conf.xml | 41 ++++++++++++++++++ .../binaries/matex/test/ground_1.conf.xml | 13 +++--- .../components/binaries/matex/test/matex.sty | 17 +++++--- 10 files changed, 108 insertions(+), 26 deletions(-) diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml index 5793ab38f..8ed2a3d57 100644 --- a/matita/components/binaries/matex/engine.ml +++ b/matita/components/binaries/matex/engine.ml @@ -48,6 +48,16 @@ let missing s = (* 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 "" @@ -80,8 +90,8 @@ let rec proc_term st is = function | 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) -> @@ -96,27 +106,34 @@ let rec proc_term st is = function 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 _ @@ -153,11 +170,11 @@ let mk_exit st ris = 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 @@ -215,13 +232,13 @@ let proc_item item s ss t = 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 = diff --git a/matita/components/binaries/matex/ground.ml b/matita/components/binaries/matex/ground.ml index 0e9f28c55..91d85bc36 100644 --- a/matita/components/binaries/matex/ground.ml +++ b/matita/components/binaries/matex/ground.ml @@ -48,6 +48,10 @@ let rec foldi_left mapi i a = function | [] -> 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) diff --git a/matita/components/binaries/matex/ground.mli b/matita/components/binaries/matex/ground.mli index 90ef8ddd5..9cc32beda 100644 --- a/matita/components/binaries/matex/ground.mli +++ b/matita/components/binaries/matex/ground.mli @@ -29,4 +29,6 @@ val rev_neg_filter : ('a -> bool) -> 'a list -> 'a list -> 'a list 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 diff --git a/matita/components/binaries/matex/kernel.ml b/matita/components/binaries/matex/kernel.ml index 8b6a81a3e..818ad07d9 100644 --- a/matita/components/binaries/matex/kernel.ml +++ b/matita/components/binaries/matex/kernel.ml @@ -46,9 +46,11 @@ let init () = 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 diff --git a/matita/components/binaries/matex/matex.ml b/matita/components/binaries/matex/matex.ml index 454c0463a..30f96287a 100644 --- a/matita/components/binaries/matex/matex.ml +++ b/matita/components/binaries/matex/matex.ml @@ -37,6 +37,8 @@ let help = "" 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 = @@ -47,6 +49,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.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 = diff --git a/matita/components/binaries/matex/options.ml b/matita/components/binaries/matex/options.ml index 81cf705ba..1a2522142 100644 --- a/matita/components/binaries/matex/options.ml +++ b/matita/components/binaries/matex/options.ml @@ -68,6 +68,8 @@ let alpha_type = ref default_alpha (* data for type-based alpha-convers 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 = @@ -90,4 +92,5 @@ let clear () = list_och := default_list_och; alpha_type := default_alpha; alpha_sort := default_alpha; + alpha_gref := default_alpha; macro_gref := default_macro diff --git a/matita/components/binaries/matex/options.mli b/matita/components/binaries/matex/options.mli index ec4694e71..da4f7a46d 100644 --- a/matita/components/binaries/matex/options.mli +++ b/matita/components/binaries/matex/options.mli @@ -37,6 +37,8 @@ val alpha_type: (string * string * string) list ref 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 diff --git a/matita/components/binaries/matex/test/basic_1.conf.xml b/matita/components/binaries/matex/test/basic_1.conf.xml index 6292ed4ce..701b0c84f 100644 --- a/matita/components/binaries/matex/test/basic_1.conf.xml +++ b/matita/components/binaries/matex/test/basic_1.conf.xml @@ -125,6 +125,47 @@ Prop x H Type[cic:/matita/pts/Type0.univ] f a + + clt_wf__q_ind q_ind_aux + + ex1__leq_sort_SS leq_sort_SS_aux + + flt_wf__q_ind q_ind_aux + + llt_wf__q_ind q_ind_aux + + nf2_gen__nf2_gen_aux nf2_gen_aux + + pc3_ind_left__pc3_left_pc3 pc3_left_pc3_aux + pc3_ind_left__pc3_left_pr3 pc3_left_pr3_aux + pc3_ind_left__pc3_left_sym pc3_left_sym_aux + pc3_ind_left__pc3_left_trans pc3_left_trans_aux + pc3_ind_left__pc3_pc3_left pc3_pc3_left_aux + pc3_wcpr0__pc3_wcpr0_t_aux pc3_wcpr0_t_aux + + pr0_confluence__pr0_cong_delta pr0_cong_delta_aux + pr0_confluence__pr0_cong_upsilon_cong pr0_cong_upsilon_cong_aux + pr0_confluence__pr0_cong_upsilon_delta pr0_cong_upsilon_delta_aux + pr0_confluence__pr0_cong_upsilon_refl pr0_cong_upsilon_refl_aux + pr0_confluence__pr0_cong_upsilon_zeta pr0_cong_upsilon_zeta_aux + pr0_confluence__pr0_delta_delta pr0_delta_delta_aux + pr0_confluence__pr0_delta_tau pr0_delta_tau_aux + pr0_confluence__pr0_upsilon_upsilon pr0_upsilon_upsilon_aux + + pr2_confluence__pr2_delta_delta pr2_delta_delta_aux + pr2_confluence__pr2_free_delta pr2_free_delta_aux + pr2_confluence__pr2_free_free pr2_free_free_aux + + sc3_props__sc3_sn3_abst sc3_sn3_abst_aux + + terms_props__bind_dec bind_dec_aux + terms_props__flat_dec flat_dec_aux + terms_props__kind_dec kind_dec_aux + + 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 + diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty index 119dffd26..9b2e412c7 100644 --- a/matita/components/binaries/matex/test/matex.sty +++ b/matita/components/binaries/matex/test/matex.sty @@ -1,5 +1,5 @@ \NeedsTeXFormat{LaTeX2e}[1995/12/01] -\ProvidesPackage{matex}[2016/06/05 MaTeX Package] +\ProvidesPackage{matex}[2016/06/12 MaTeX Package] \RequirePackage{xcolor} \RequirePackage{stix} \ExecuteOptions{} @@ -14,6 +14,8 @@ \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} @@ -69,6 +71,7 @@ \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} @@ -90,8 +93,9 @@ (\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 } @@ -103,11 +107,14 @@ \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} -- 2.39.2