From 28e8954fbe2e28f01ae918c8d0e0ef34bd84b48f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 22 Jun 2016 19:46:32 +0000 Subject: [PATCH] - matex: minor improvements - latex stylesheets: more notation for basic_1 now we use just the stix fonts --- matita/components/binaries/matex/Makefile | 2 +- matita/components/binaries/matex/alpha.ml | 2 +- .../components/binaries/matex/anticipate.ml | 2 +- matita/components/binaries/matex/engine.ml | 22 ++-- matita/components/binaries/matex/matex.ml | 10 +- matita/components/binaries/matex/options.ml | 11 +- matita/components/binaries/matex/options.mli | 4 +- .../binaries/matex/test/basic_1.conf.xml | 104 +++++++++++------- .../binaries/matex/test/basic_1.sty | 69 ++++++++++-- .../binaries/matex/test/ground_1.conf.xml | 2 +- .../binaries/matex/test/ground_1.sty | 14 +-- .../binaries/matex/test/legacy_1.sty | 26 ++--- .../components/binaries/matex/test/matex.sty | 10 +- .../components/binaries/matex/test/test.tex | 6 +- 14 files changed, 183 insertions(+), 101 deletions(-) diff --git a/matita/components/binaries/matex/Makefile b/matita/components/binaries/matex/Makefile index c9a7b58ed..b3cc515d2 100644 --- a/matita/components/binaries/matex/Makefile +++ b/matita/components/binaries/matex/Makefile @@ -21,6 +21,6 @@ test/$(OBJS): $(REGISTRY) test/$(SRCS): test/$(OBJS) $(REGISTRY) ./matex.native @echo MaTeX: processing $< - $(H)./matex.native -O test -l $(SRCS) -p -g -a $(REGISTRY) `cat $<` + $(H)./matex.native -O test -l $(SRCS) -a -g -p $(REGISTRY) `cat $<` .PHONY: test diff --git a/matita/components/binaries/matex/alpha.ml b/matita/components/binaries/matex/alpha.ml index 4c4eccef7..6420d20c6 100644 --- a/matita/components/binaries/matex/alpha.ml +++ b/matita/components/binaries/matex/alpha.ml @@ -165,7 +165,7 @@ and proc_terms st ts = let proc_named_term s st t = try let tt = proc_term st t in - if !G.test then begin + if !G.check then begin let _ = K.typeof st.c tt in ok s end; diff --git a/matita/components/binaries/matex/anticipate.ml b/matita/components/binaries/matex/anticipate.ml index e6f51e554..645d7b417 100644 --- a/matita/components/binaries/matex/anticipate.ml +++ b/matita/components/binaries/matex/anticipate.ml @@ -104,7 +104,7 @@ let shift_named_term s c t = try fresh := 0; let tt = shift_term c t in - if !G.test then begin + if !G.check then begin let _ = K.typeof c tt in ok s end; diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml index 2fffd264c..83de453f7 100644 --- a/matita/components/binaries/matex/engine.ml +++ b/matita/components/binaries/matex/engine.ml @@ -43,8 +43,8 @@ let internal s = let malformed s = X.error ("engine: malformed term: " ^ s) -let missing s = - X.log ("engine: missing macro for " ^ s) +let missing s l = + X.log (P.sprintf "engine: missing macro for %s (%u)" s l) (* generic term processing *) @@ -72,13 +72,16 @@ let get_macro s l = let get_head = function | C.Const c :: ts -> let s, _ = K.resolve_reference c in - let macro, x = get_macro s (L.length ts) in - if macro <> "" then - let ts1, ts2 = X.split_at x ts in - Some (macro, s, ts1, ts2) - else begin - if !G.log_missing then missing s; - None + 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 + Some (macro, s, ts1, ts2) end | _ -> None @@ -243,6 +246,7 @@ let proc_item item s ss t = 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 = + if !G.no_proofs then [] else 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 *) diff --git a/matita/components/binaries/matex/matex.ml b/matita/components/binaries/matex/matex.ml index 88ae85436..ddd413049 100644 --- a/matita/components/binaries/matex/matex.ml +++ b/matita/components/binaries/matex/matex.ml @@ -25,11 +25,12 @@ module K = Kernel let help_O = " Set this output directory" let help_X = " Clear configuration and options" let help_a = " Log alpha-unconverted identifiers (default: no)" +let help_c = " Check term transformations (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)" +let help_p = " Omit proofs (default: no)" +let help_t = " Omit types (default: no)" let help = "" @@ -77,11 +78,12 @@ begin try "-O", A.String ((:=) G.out_dir), help_O; "-X", A.Unit G.clear, help_X; "-a", A.Set G.log_alpha, help_a; + "-c", A.Set G.check, help_c; "-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; + "-p", A.Set G.no_proofs, help_p; + "-t", A.Set G.no_types, help_t; ] process help with | X.Error s -> X.log s diff --git a/matita/components/binaries/matex/options.ml b/matita/components/binaries/matex/options.ml index b361841c6..165b2d978 100644 --- a/matita/components/binaries/matex/options.ml +++ b/matita/components/binaries/matex/options.ml @@ -22,10 +22,12 @@ let default_out_dir = F.current_dir_name let default_proc_id = "H" -let default_test = false +let default_check = false let default_no_types = false +let default_no_proofs = false + let default_global_alpha = false let default_log_alpha = false @@ -52,10 +54,12 @@ let out_dir = ref default_out_dir (* directory of generated files *) let proc_id = ref default_proc_id (* identifer for anticipations *) -let test = ref default_test (* test anticipation *) +let check = ref default_check (* check transformations *) let no_types = ref default_no_types (* omit types *) +let no_proofs = ref default_no_proofs (* omit proofs *) + let global_alpha = ref default_global_alpha (* log alpha-unconverted identifiers *) let log_alpha = ref default_log_alpha (* log alpha-unconverted identifiers *) @@ -84,8 +88,9 @@ let clear () = no_init := default_no_init; out_dir := default_out_dir; proc_id := default_proc_id; - test := default_test; + check := default_check; no_types := default_no_types; + no_proofs := default_no_proofs; global_alpha := default_global_alpha; log_alpha := default_log_alpha; log_missing := default_log_missing; diff --git a/matita/components/binaries/matex/options.mli b/matita/components/binaries/matex/options.mli index 3801a8d19..1c6aef077 100644 --- a/matita/components/binaries/matex/options.mli +++ b/matita/components/binaries/matex/options.mli @@ -21,10 +21,12 @@ val out_dir: string ref val proc_id: string ref -val test: bool ref +val check: bool ref val no_types: bool ref +val no_proofs: bool ref + val global_alpha: bool ref val log_alpha: bool ref diff --git a/matita/components/binaries/matex/test/basic_1.conf.xml b/matita/components/binaries/matex/test/basic_1.conf.xml index 5056ebfbc..162425ddd 100644 --- a/matita/components/binaries/matex/test/basic_1.conf.xml +++ b/matita/components/binaries/matex/test/basic_1.conf.xml @@ -170,50 +170,60 @@ ty3_nf2_gen__ty3_nf2_inv_abst_aux ty3_nf2_inv_abst_aux
+ $(devel.basic1).A.defs.A.AHead.type To 2 0 + $(devel.basic1).A.defs.A.ASort.type AtomB 2 0 + $(devel.basic1).app.defs.app1.app1.type Shift 2 0 + $(devel.basic1).app.defs.cbk.cbk.type Level 1 0 + + $(devel.basic1).C.defs.C.CSort.type AtomA 1 0 + $(devel.basic1).C.defs.cle.type LE 2 0 + $(devel.basic1).C.defs.clt.type LT 2 0 + + $(devel.basic1).C.defs.cweight.cweight.type WeightA 1 0 + + $(devel.basic1).clear.defs.clear.clear.type Drop 2 0 + $(devel.basic1).clen.defs.clen.clen.type Length 1 0 + $(devel.basic1).cnt.defs.cnt.cnt.type LEnv 1 0 + + $(devel.basic1).csubst0.defs.csubst0.csubst0.type Subst 4 0 + $(devel.basic1).csubst1.defs.csubst1.csubst1.type SubstS 4 0 + - $(devel.basic1).drop1.defs.drop1.drop1.type DropS 2 0 + $(devel.basic1).drop1.defs.drop1.drop1.type DropS 3 0 - $(devel.basic1).drop.defs.drop.drop.type Drop 3 0 + $(devel.basic1).drop.defs.drop.drop.type DropB 4 0 + $(devel.basic1).ex0.defs.leqz.leqz.type Equiv 2 0 + $(devel.basic1).flt.defs.flt.type LTB 4 0 + $(devel.basic1).flt.defs.fweight.type WeightB 2 0 + $(devel.basic1).fsubst0.defs.fsubst0.fsubst0.type SubstB 6 0 + $(devel.basic1).G.defs.next.next.type Next 2 0 + $(devel.basic1).getl.defs.getl.getl.type DropA 3 0 + $(devel.basic1).iso.defs.iso.iso.type SameTop 2 0 + $(devel.basic1).leq.defs.leq.leq.type EquivA 3 0 $(devel.basic1).lift1.defs.lift1.lift1.type FunLiftS 2 0 $(devel.basic1).lift1.defs.lifts1.lifts1.type FunLiftS 2 0 $(devel.basic1).lift.defs.lifts.lifts.type FunLift 3 0 $(devel.basic1).lift.defs.lift.type FunLift 3 0 + $(devel.basic1).lift.defs.lref_map.lref_map.type FunLift 3 0 + $(devel.basic1).llt.defs.llt.type LT 2 0 + $(devel.basic1).llt.defs.lweight.lweight.type WeightA 1 0 + $(devel.basic1).r.defs.r.type FunW 2 0 + + $(devel.basic1).s.defs.s.type FunV 2 0 + + $(devel.basic1).subst0.defs.subst0.subst0.type Subst 4 0 + $(devel.basic1).subst1.defs.subst1.subst1.type SubstS 4 0 + $(devel.basic1).subst.defs.subst.subst.type FunSubstS 3 0 + + $(devel.basic1).T.defs.tle.type LE 2 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).tlist.defs.TApp.TApp.type RevConsA 2 0 + $(devel.basic1).tlist.defs.TApp.TApp.type CoConsA 2 0 $(devel.basic1).tlist.defs.TList.TCons.type ConsA 2 0 + $(devel.basic1).tlist.defs.tslen.tslen.type Length 1 0 + $(devel.basic1).tlist.defs.tslt.type LT 2 0 + $(devel.basic1).tlt.defs.tlt.type LT 2 0 + $(devel.basic1).tlt.defs.wadd.type CoConsA 2 0 + $(devel.basic1).tlt.defs.weight_map.weight_map.type CoWeightB 2 0 + $(devel.basic1).tlt.defs.weight.type CoWeightA 1 0