From c992745a40b4ac8b6c5285bf9c5eff26c423f236 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 19 Jun 2016 12:59:00 +0000 Subject: [PATCH] - matex: minor corrections to handle applications with many arguments - matex test stylesheets: some improvements, notation for ground_1 completed --- matita/components/binaries/matex/engine.ml | 26 ++++++---- matita/components/binaries/matex/ground.ml | 7 +++ matita/components/binaries/matex/ground.mli | 2 + matita/components/binaries/matex/matex.ml | 2 +- matita/components/binaries/matex/options.ml | 2 +- matita/components/binaries/matex/options.mli | 2 +- .../binaries/matex/test/ground_1.conf.xml | 50 +++++++++---------- .../binaries/matex/test/ground_1.sty | 18 ++++++- .../binaries/matex/test/legacy_1.conf.xml | 24 ++++----- .../binaries/matex/test/legacy_1.sty | 15 +++--- .../components/binaries/matex/test/matex.sty | 22 ++++---- matita/components/registry/helm_registry.ml | 11 ++++ matita/components/registry/helm_registry.mli | 4 ++ 13 files changed, 119 insertions(+), 66 deletions(-) diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml index 8ed2a3d57..2fffd264c 100644 --- a/matita/components/binaries/matex/engine.ml +++ b/matita/components/binaries/matex/engine.ml @@ -63,17 +63,20 @@ let mk_ptr st name = let get_macro s l = let rec aux = function - | [] -> "" - | (r, m, a) :: _ when r = s && a = l -> m - | _ :: tl -> aux tl + | [] -> "", 0 + | (r, m, a, x) :: _ when r = s && a = l -> m, x + | _ :: tl -> aux tl in aux !G.macro_gref let get_head = function | C.Const c :: ts -> let s, _ = K.resolve_reference c in - let macro = get_macro s (L.length ts) in - if macro <> "" then Some (macro, s, ts) else begin + 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 end @@ -94,12 +97,17 @@ let rec proc_term st is = function 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 riss = L.rev_map (proc_term st []) ts in - T.Macro macro :: T.free s :: T.mk_rev_args riss is - | None -> + | None -> let riss = L.rev_map (proc_term st []) ts in T.Macro "APPL" :: T.mk_rev_args riss is + | Some (macro, s, [], ts) + | 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 + | Some (macro, s, ts1, ts2) -> + let riss1 = L.rev_map (proc_term st []) ts1 in + let riss2 = L.rev_map (proc_term st []) ts2 in + T.Macro macro :: T.free s :: T.mk_rev_args riss1 (T.mk_rev_args riss2 is) end | C.Prod (s, w, t) -> let is_w = proc_term st [] w in diff --git a/matita/components/binaries/matex/ground.ml b/matita/components/binaries/matex/ground.ml index 91d85bc36..7eebedb7d 100644 --- a/matita/components/binaries/matex/ground.ml +++ b/matita/components/binaries/matex/ground.ml @@ -56,6 +56,13 @@ let rec rev_map_append map l r = match l with | [] -> r | hd :: tl -> rev_map_append map tl (map hd :: r) +let rec split_at x = function + | l when x <= 0 -> [], l + | [] -> [], [] + | hd :: tl -> + let l1, l2 = split_at (pred x) tl in + hd :: l1, l2 + let error s = raise (Error s) let log s = P.eprintf "MaTeX: %s\n%!" s diff --git a/matita/components/binaries/matex/ground.mli b/matita/components/binaries/matex/ground.mli index 9cc32beda..923ec58b7 100644 --- a/matita/components/binaries/matex/ground.mli +++ b/matita/components/binaries/matex/ground.mli @@ -32,3 +32,5 @@ 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 + +val split_at: int -> 'a list -> 'a list * 'a list diff --git a/matita/components/binaries/matex/matex.ml b/matita/components/binaries/matex/matex.ml index 30f96287a..88ae85436 100644 --- a/matita/components/binaries/matex/matex.ml +++ b/matita/components/binaries/matex/matex.ml @@ -39,7 +39,7 @@ 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 macro_decode = R.quad R.string R.string R.int R.int let init registry = R.load_from registry; diff --git a/matita/components/binaries/matex/options.ml b/matita/components/binaries/matex/options.ml index 1a2522142..b361841c6 100644 --- a/matita/components/binaries/matex/options.ml +++ b/matita/components/binaries/matex/options.ml @@ -70,7 +70,7 @@ let alpha_sort = ref default_alpha (* data for sort-based alpha-convers let alpha_gref = ref default_alpha (* data for constant renaming *) -let macro_gref = ref default_macro (* data eta-conversion and constant rendering *) +let macro_gref = ref default_macro (* data for eta-conversion and constant rendering *) let is_global_id s = !global_alpha && s <> dno_id diff --git a/matita/components/binaries/matex/options.mli b/matita/components/binaries/matex/options.mli index da4f7a46d..3801a8d19 100644 --- a/matita/components/binaries/matex/options.mli +++ b/matita/components/binaries/matex/options.mli @@ -39,7 +39,7 @@ val alpha_sort: (string * string * string) list ref val alpha_gref: (string * string) list ref -val macro_gref: (string * string * int) list ref +val macro_gref: (string * string * int * int) list ref val clear: unit -> unit diff --git a/matita/components/binaries/matex/test/ground_1.conf.xml b/matita/components/binaries/matex/test/ground_1.conf.xml index 77d65746f..aff4fc4dd 100644 --- a/matita/components/binaries/matex/test/ground_1.conf.xml +++ b/matita/components/binaries/matex/test/ground_1.conf.xml @@ -1,29 +1,29 @@ - + matita.lambdadelta.ground_1.blt.defs.blt.blt.type FunLt 2 0 + matita.lambdadelta.ground_1.plist.defs.papp.papp.type Append 2 0 + matita.lambdadelta.ground_1.plist.defs.PConsTail.PConsTail.type RevConsB 3 0 + matita.lambdadelta.ground_1.plist.defs.PList.PCons.type ConsB 3 0 + matita.lambdadelta.ground_1.plist.defs.Ss.Ss.type Succ 1 0 + diff --git a/matita/components/binaries/matex/test/ground_1.sty b/matita/components/binaries/matex/test/ground_1.sty index 582e49cef..58f2592de 100644 --- a/matita/components/binaries/matex/test/ground_1.sty +++ b/matita/components/binaries/matex/test/ground_1.sty @@ -1,10 +1,26 @@ \NeedsTeXFormat{LaTeX2e}[1995/12/01] -\ProvidesPackage{ground_1}[2016/05/23 Notation for "cic:/matita/lambdadelta/ground_1/"] +\ProvidesPackage{ground_1}[2016/06/19 Notation for "cic:/matita/lambdadelta/ground_1/"] +\RequirePackage{matex} \ExecuteOptions{} \ProcessOptions* \makeatletter +\newcommand*\ld@cm[1]{\setpunctlink{,}{#1}} +\newcommand*\ld@oa[1]{\setopenlink{\langle}{#1}} +\newcommand*\ld@ca[1]{\setcloselink{\rangle}{#1}} + +\newcommand*\ld@append[1]{\setbinlink{@}{#1}} +\newcommand*\ld@cons[1]{\setbinlink{\copyright}{#1}} +\newcommand*\ld@funlt[1]{\setbinlink{\olessthan}{#1}} + +\newcommand*\ld@tupleB[3]{\ld@oa{#1}#2\ld@cm{#1}#3\ld@ca{#1}} + +\newcommand*\Append[3]{#2\ld@append{#1}#3} +\newcommand*\ConsB[4]{\ld@tupleB{#1}{#2}{#3}\ld@cons{#1}#4} +\newcommand*\FunLt[3]{#2\ld@funlt{#1}#3} +\newcommand*\RevConsB[4]{#2\ld@cons{#1}\ld@tupleB{#1}{#3}{#4}} + \makeatother \endinput diff --git a/matita/components/binaries/matex/test/legacy_1.conf.xml b/matita/components/binaries/matex/test/legacy_1.conf.xml index e215669f8..606b6b776 100644 --- a/matita/components/binaries/matex/test/legacy_1.conf.xml +++ b/matita/components/binaries/matex/test/legacy_1.conf.xml @@ -1,18 +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.ex.ex.type LEx 2 1 + matita.lambdadelta.legacy_1.coq.defs.ex2.ex2.type LEx 3 1 + matita.lambdadelta.legacy_1.coq.defs.land.land.type LAnd 2 0 + matita.lambdadelta.legacy_1.coq.defs.or.or.type LOr 2 0 - 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 + matita.lambdadelta.legacy_1.coq.defs.eq.eq.type EQ 3 0 + matita.lambdadelta.legacy_1.coq.defs.le.le.type LE 2 0 + matita.lambdadelta.legacy_1.coq.defs.lt.type LT 2 0 + matita.lambdadelta.legacy_1.coq.defs.minus.minus.type Minus 2 0 + matita.lambdadelta.legacy_1.coq.defs.nat.S.type Succ 1 0 + matita.lambdadelta.legacy_1.coq.defs.not.type LNot 1 0 + matita.lambdadelta.legacy_1.coq.defs.plus.plus.type Plus 2 0 + matita.lambdadelta.legacy_1.coq.defs.pred.type Pred 1 0
diff --git a/matita/components/binaries/matex/test/legacy_1.sty b/matita/components/binaries/matex/test/legacy_1.sty index 10edd9b62..0ee778345 100644 --- a/matita/components/binaries/matex/test/legacy_1.sty +++ b/matita/components/binaries/matex/test/legacy_1.sty @@ -1,5 +1,5 @@ \NeedsTeXFormat{LaTeX2e}[1995/12/01] -\ProvidesPackage{legacy_1}[2016/06/06 Notation for "cic:/matita/lambdadelta/legacy_1/"] +\ProvidesPackage{legacy_1}[2016/06/19 Notation for "cic:/matita/lambdadelta/legacy_1/"] \RequirePackage{matex} \RequirePackage{fdsymbol} \ExecuteOptions{} @@ -17,16 +17,17 @@ \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@minus[1]{\setbinlink{-}{#1}} \newcommand*\ld@lnot[1]{\setoplink{\lnot}{#1}} -\newcommand*\ld@plus[1]{\setbinlink{-}{#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*\ld@list[2]{\ma@list\relax\ma@arg{#1{#2}}\relax} + +\newcommand*\LAnd[1]{\ld@list\ld@land{#1}} +\newcommand*\LOr[1]{\ld@list\ld@lor{#1}} +\newcommand*\LEx[1]{\ld@lex{#1}\ma@list\relax\ma@skip\relax{\ld@list\ld@and{#1}}} \newcommand*\EQ[4]{#3\ld@eq{#1}#4} \newcommand*\LE[3]{#2\ld@le{#1}#3} diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty index 9b2e412c7..a46b2af1b 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/12 MaTeX Package] +\ProvidesPackage{matex}[2016/06/19 MaTeX Package] \RequirePackage{xcolor} \RequirePackage{stix} \ExecuteOptions{} @@ -47,6 +47,9 @@ \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*\setopenlink[2]{\mathopen{\ma@setlink{#1}{#2}}} +\newcommand*\setcloselink[2]{\mathclose{\ma@setlink{#1}{#2}}} +\newcommand*\setpunctlink[2]{\mathpunct{\ma@setlink{#1}{#2}}} \newcommand*\ObjIncNode{} \newcommand*\ObjNode{} @@ -62,20 +65,21 @@ \newenvironment{ma@step}[1]{\color{#1}}{\par} \newcommand*\ma@tmp{} -\newcommand*\ma@skip[4]{} -\newcommand*\ma@next[5]{\def\ma@tmp{#5}% - \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@last[4]{#4} +\newcommand*\ma@list[5]{\def\ma@tmp{#5}% + \ifx\ma@tmp\empty\let\ma@tmp=\ma@last\else #1#2{#5}\let\ma@tmp=\ma@list\fi + \ma@tmp{#3}{#2}{#3}{#4}% } -\newcommand*\ma@thop[1]{\mathop{#1}\allowbreak} +\newcommand*\ma@thop[1]{\mathpunct{#1}\allowbreak} \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} +\newcommand*\ma@args{(\ma@list\relax\ma@arg\ma@cm\ma@cp} +\newcommand*\ma@cases{\ma@list\relax\ma@arg\ma@or\relax} \newcommand*\ma@bind{\ma@thop{}} +\newcommand*\ma@skip[1]{} \newcommand*\PROP{\mathord\mathrm{PROP}} \newcommand*\CROP[1]{\mathord\mathrm{CROP}} @@ -106,7 +110,7 @@ \else\begin{ma@step}{#4}$\mathbf{\ma@setopttarget{#5}{#6}}$% \fi } -\newcommand*\ma@tail{\ma@next\ma@with\ma@term\ma@comma\ma@stop} +\newcommand*\ma@tail{\ma@list\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 } diff --git a/matita/components/registry/helm_registry.ml b/matita/components/registry/helm_registry.ml index 877de0a1c..08b1bb76f 100644 --- a/matita/components/registry/helm_registry.ml +++ b/matita/components/registry/helm_registry.ml @@ -121,6 +121,12 @@ let triple fst_unmarshaller snd_unmarshaller trd_unmarshaller v = | [fst; snd; trd] -> fst_unmarshaller fst, snd_unmarshaller snd, trd_unmarshaller trd | _ -> raise (Type_error "not a triple") +(* FG *) +let quad fst_unmarshaller snd_unmarshaller trd_unmarshaller fth_unmarshaller v = + match Str.split spaces_rex v with + | [fst; snd; trd; fth] -> fst_unmarshaller fst, snd_unmarshaller snd, trd_unmarshaller trd, fth_unmarshaller fth + | _ -> raise (Type_error "not a quad") + (* escapes for xml configuration file *) let (escape, unescape) = let (in_enc, out_enc) = (`Enc_utf8, `Enc_utf8) in @@ -220,6 +226,10 @@ let get_pair registry fst_unmarshaller snd_unmarshaller = let get_triple registry fst_unmarshaller snd_unmarshaller trd_unmarshaller = get_typed registry (triple fst_unmarshaller snd_unmarshaller trd_unmarshaller) +(* FG *) +let get_quad registry fst_unmarshaller snd_unmarshaller trd_unmarshaller fth_unmarshaller = + get_typed registry (quad fst_unmarshaller snd_unmarshaller trd_unmarshaller fth_unmarshaller) + let set_list registry marshaller ~key ~value = (* since ocaml hash table are crazy... *) while Hashtbl.mem registry key do @@ -424,6 +434,7 @@ let get_opt_default unmarshaller = get_opt_default default_registry unmarshaller let get_list unmarshaller = get_list default_registry unmarshaller let get_pair unmarshaller = get_pair default_registry unmarshaller let get_triple unmarshaller = get_triple default_registry unmarshaller +let get_quad unmarshaller = get_quad default_registry unmarshaller let set_typed marshaller = set_typed default_registry marshaller let set_opt unmarshaller = set_opt default_registry unmarshaller let set_list marshaller = set_list default_registry marshaller diff --git a/matita/components/registry/helm_registry.mli b/matita/components/registry/helm_registry.mli index 68434603d..29dd335fa 100644 --- a/matita/components/registry/helm_registry.mli +++ b/matita/components/registry/helm_registry.mli @@ -134,6 +134,7 @@ val float: string -> float val bool: string -> bool val pair: (string -> 'a) -> (string -> 'b) -> string -> 'a * 'b val triple: (string -> 'a) -> (string -> 'b) -> (string -> 'c) -> string -> 'a * 'b * 'c +val quad: (string -> 'a) -> (string -> 'b) -> (string -> 'c) -> (string -> 'd) -> string -> 'a * 'b * 'c * 'd (** {3 Typed getters} *) @@ -154,6 +155,9 @@ val get_pair: (string -> 'a) -> (string -> 'b) -> string -> 'a * 'b (** decode values which are blank separated list of values, of length 3 *) val get_triple: (string -> 'a) -> (string -> 'b) -> (string -> 'c) -> string -> 'a * 'b * 'c + (** decode values which are blank separated list of values, of length 4 *) +val get_quad: (string -> 'a) -> (string -> 'b) -> (string -> 'c) -> (string -> 'd) -> string -> 'a * 'b * 'c * 'd + (** {4 Shorthands} *) val get_string: string -> string -- 2.39.2