From 2fa001c86e37c76c840122655cb4ffba8bb30cad Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 30 Apr 2016 21:33:47 +0000 Subject: [PATCH] - matex: support for alpha-conversion completed - matex.sty: hyperlinks without labels - registry: support or triples --- matita/components/binaries/matex/Makefile | 13 +- matita/components/binaries/matex/alpha.ml | 159 ++++++++++++++++++ matita/components/binaries/matex/alpha.mli | 12 ++ .../components/binaries/matex/anticipate.ml | 35 ++-- .../components/binaries/matex/anticipate.mli | 6 - matita/components/binaries/matex/engine.ml | 29 ++-- matita/components/binaries/matex/ground.ml | 2 + matita/components/binaries/matex/ground.mli | 2 + matita/components/binaries/matex/kernel.ml | 17 +- matita/components/binaries/matex/matex.ml | 10 +- matita/components/binaries/matex/options.ml | 25 ++- matita/components/binaries/matex/options.mli | 6 + .../components/binaries/matex/test/Makefile | 4 +- .../binaries/matex/test/basic_1.conf.xml | 129 ++++++++++++++ .../components/binaries/matex/test/matex.sty | 22 ++- .../components/binaries/matex/test/test.tex | 6 - matita/components/registry/helm_registry.ml | 11 ++ matita/components/registry/helm_registry.mli | 4 + 18 files changed, 417 insertions(+), 75 deletions(-) create mode 100644 matita/components/binaries/matex/alpha.ml create mode 100644 matita/components/binaries/matex/alpha.mli create mode 100644 matita/components/binaries/matex/test/basic_1.conf.xml diff --git a/matita/components/binaries/matex/Makefile b/matita/components/binaries/matex/Makefile index 342ba027d..9212a0662 100644 --- a/matita/components/binaries/matex/Makefile +++ b/matita/components/binaries/matex/Makefile @@ -6,19 +6,20 @@ REQUIRES = helm-ng_library include ../Makefile.common PROBE = ../probe/probe.native -REGISTRY = $(RT_BASE_DIR)/matita.conf.xml +REGISTRY = $(RT_BASE_DIR)/matita.conf.xml test/basic_1.conf.xml OBJS = Make.objs +SRCS = Make.srcs BASEURI = cic:/matita/lambdadelta/basic_1/ -test: test/$(OBJS) +test: test/$(SRCS) -$(OBJS): +test/$(OBJS): $(REGISTRY) @echo probe: $(BASEURI) $(H)$(PROBE) $(REGISTRY) -g $(BASEURI) -os > $@ -test/$(OBJS): $(OBJS) ./matex.native - @echo MaTeX: processing $(OBJS) - $(H)./matex.native -O test -l $(OBJS) -t -p $(REGISTRY) `cat $<` +test/$(SRCS): test/$(OBJS) $(REGISTRY) ./matex.native + @echo MaTeX: processing $< + $(H)./matex.native -O test -l $(SRCS) -p -a $(REGISTRY) `cat $<` .PHONY: test diff --git a/matita/components/binaries/matex/alpha.ml b/matita/components/binaries/matex/alpha.ml new file mode 100644 index 000000000..59e8c989f --- /dev/null +++ b/matita/components/binaries/matex/alpha.ml @@ -0,0 +1,159 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module L = List +module P = Printf +module S = Scanf +module N = String + +module U = NUri +module C = NCic +module R = NReference +module E = NCicEnvironment +module T = NCicTypeChecker + +module X = Ground +module G = Options +module K = Kernel + +let dno = "_" (* does not occur *) + +let nan = -1 (* not a number *) + +(* internal functions *******************************************************) + +let malformed s = + X.error ("alpha: malformed term: " ^ s) + +let ok s = + X.log ("alpha: ok " ^ s) + +let rec trim r = + let r1, r2 = S.sscanf r "%s@_%s" X.id2 in + if r2 = "" then r1 else trim r1 + +let split s = + let rec aux i l = + let j = pred i in + if j >=0 && s.[j] >= '0' && s.[j] <= '9' then aux j (succ l) else i, l + in + let i, l = aux (N.length s) 0 in + let s1, s2 = N.sub s 0 i, N.sub s i l in + let s1 = if s1 = "" then "_" else s1 in + s1, if l = 0 then nan else int_of_string s2 + +let rec strip = function + | C.Appl (t :: _) + | C.Prod (_, _, t) -> strip t + | t -> t + +let get_constant c t = match strip (K.whd c t) with + | C.Sort (C.Prop) -> + P.sprintf "Prop" + | C.Sort (C.Type [`Type, u]) -> + P.sprintf "Type[%s]" (U.string_of_uri u) + | C.Sort (C.Type [`CProp, u]) -> + P.sprintf "CProp[%s]" (U.string_of_uri u) + | C.Const (R.Ref (u, r)) -> + let ss = K.segments_of_uri u in + let _, _, _, _, obj = E.get_checked_obj G.status u in + let ss, _ = K.name_of_reference ss (obj, r) in + X.rev_map_concat X.id "." "type" ss + | _ -> "" + +let read l s r = + let rec aux = function + | [] -> "" + | (a, b, c) :: tl -> + if s = a && (r = b || r = c) then c else aux tl + in + aux l + +let type_check r c w = + let s0 = get_constant c w in + let r0 = read !G.alpha_type s0 r in + if r0 <> "" then r0 else + let s1 = get_constant c (K.typeof c w) in + let r0 = read !G.alpha_sort s1 r in + if r0 <> "" then r0 else begin + if !G.log_alpha then + X.log (P.sprintf "alpha: not found %s: type \"%s\" sort \"%s\"" r s0 s1); + r + end + +let rec get r = function + | [] -> r + | (h, d) :: tl -> + if fst r = h && snd r <= d then h, succ d else get r tl + +let alpha d c s w t = + if K.does_not_occur K.fst_var c t then dno, nan else + let r, i = split (trim s) in + get (type_check r c w, i) d + +let mk_name (s, i) = + if i < 0 then s else P.sprintf "%s%u" s i + +let add_name r d = r :: d + +let rec proc_term d c t = match t with + | C.Meta _ + | C.Implicit _ + | C.Sort _ + | C.Rel _ + | C.Const _ -> t + | C.Appl ts -> + let tts = proc_terms d c ts in + K.appl tts + | C.Match (w, u, v, ts) -> + let uu = proc_term d c u in + let vv = proc_term d c v in + let tts = proc_terms d c ts in + K.case w uu vv tts + | C.Prod (s, w, t) -> + let rr = alpha d c s w t in + let ss = mk_name rr in + let ww = proc_term d c w in + let tt = proc_term (add_name rr d) (K.add_dec ss w c) t in + K.prod ss ww tt + | C.Lambda (s, w, t) -> + let rr = alpha d c s w t in + let ss = mk_name rr in + let ww = proc_term d c w in + let tt = proc_term (add_name rr d) (K.add_dec ss w c) t in + K.lambda ss ww tt + | C.LetIn (s, w, v, t) -> + let rr = alpha d c s w t in + let ss = mk_name rr in + let ww = proc_term d c w in + let vv = proc_term d c v in + let tt = proc_term (add_name rr d) (K.add_def ss w v c) t in + K.letin ss ww vv tt + +and proc_terms d c ts = + let rtts = L.rev_map (proc_term d c) ts in + L.rev rtts + +let proc_named_term s d c t = +try + let tt = proc_term d c t in + if !G.test then begin + let _ = K.typeof c tt in + ok s + end; + tt +with + | T.TypeCheckerFailure s + | T.AssertFailure s -> malformed (Lazy.force s) + +(* interface functions ******************************************************) + +let process_top_term s t = proc_named_term s [] [] t diff --git a/matita/components/binaries/matex/alpha.mli b/matita/components/binaries/matex/alpha.mli new file mode 100644 index 000000000..5b4c6ae50 --- /dev/null +++ b/matita/components/binaries/matex/alpha.mli @@ -0,0 +1,12 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +val process_top_term: string -> NCic.term -> NCic.term diff --git a/matita/components/binaries/matex/anticipate.ml b/matita/components/binaries/matex/anticipate.ml index 47fc2cae1..e6f51e554 100644 --- a/matita/components/binaries/matex/anticipate.ml +++ b/matita/components/binaries/matex/anticipate.ml @@ -29,15 +29,6 @@ let malformed s = let ok s = X.log ("anticipate: ok " ^ s) -let typeof c t = K.whd c (K.typeof c t) - -let not_prop1 c u = match typeof c u with - | C.Sort (C.Prop) -> false - | C.Sort _ -> true - | _ -> malformed "1" - -let not_prop2 c t = not_prop1 c (K.typeof c t) - let anticipate c v = incr fresh; let w = K.typeof c v in @@ -48,7 +39,7 @@ let initial = None, [] let proc_arg c i (d, rtts) t = match d with | Some _ -> d, (t :: rtts) | None -> - if K.is_atomic t || not_prop2 c t then d, (t :: rtts) else + if K.is_atomic t || K.not_prop2 c t then d, (t :: rtts) else let s, w, v, tt = anticipate c t in Some (i, s, w, v), (tt :: rtts) @@ -68,7 +59,7 @@ let rec proc_term c t = match t with let tt = shift_term (K.add_dec s w c) t in [], K.lambda s w tt | C.LetIn (s, w, v, t) -> - if not_prop1 c w then + if K.not_prop1 c w then let dt, tt = proc_term (K.add_def s w v c) t in dt @ K.add_def s w v [], tt else @@ -80,7 +71,7 @@ let rec proc_term c t = match t with let dt, tt = proc_term (K.add_def s w vv c) t in dt @ (K.add_def s w vv dv), tt | C.Appl [t] -> proc_term c t - | C.Appl (C.Appl ts :: vs) -> proc_term c (C.Appl (ts @ vs)) + | C.Appl (C.Appl ts :: vs) -> proc_term c (K.appl (ts @ vs)) | C.Appl ts -> proc_appl c t ts | C.Match (w, u, v, ts) -> proc_case c t w u v ts @@ -89,11 +80,11 @@ and proc_appl c t ts = match X.foldi_left (proc_arg c) 1 initial ts with | Some (i, s, w, v), rtts -> let ri = L.length rtts - i in let tts = X.foldi_left (lift_arg ri) 0 [] rtts in - proc_term c (K.letin s w v (C.Appl tts)) + proc_term c (K.letin s w v (K.appl tts)) and proc_case c t w u v ts = match X.foldi_left (proc_arg c) 1 initial ts with | None , _ -> - if K.is_atomic v || not_prop1 c (C.Const w) then [], t else + if K.is_atomic v || K.not_prop1 c (C.Const w) then [], t else let s, w0, v0, vv = anticipate c v in let u = K.lift K.fst_var 1 u in let ts = K.lifts K.fst_var 1 ts in @@ -109,7 +100,7 @@ and shift_term c t = let d, tt = proc_term c t in K.shift tt d -let shift_named s c t = +let shift_named_term s c t = try fresh := 0; let tt = shift_term c t in @@ -124,25 +115,21 @@ with let proc_fun c = let r, s, i, u, t = c in - if not_prop1 [] u then c else - r, s, i, u, shift_named s [] t + if K.not_prop1 [] u then c else + r, s, i, u, shift_named_term s [] t let proc_obj obj = match obj with | C.Inductive _ | C.Constant (_, _, None, _, _) -> obj | C.Constant (r, s, Some t, u, a) -> - if not_prop1 [] u then obj else - let tt = shift_named s [] t in + if K.not_prop1 [] u then obj else + let tt = shift_named_term s [] t in C.Constant (r, s, Some tt, u, a) | C.Fixpoint (b, cs, a) -> C.Fixpoint (b, L.map proc_fun cs, a) (* interface functions ******************************************************) -(* not_prop1 *) - -(* not_prop2 *) - -let process_top_term s t = shift_named s [] t +let process_top_term s t = shift_named_term s [] t let process_obj obj = proc_obj obj diff --git a/matita/components/binaries/matex/anticipate.mli b/matita/components/binaries/matex/anticipate.mli index ec5a77775..465cff23b 100644 --- a/matita/components/binaries/matex/anticipate.mli +++ b/matita/components/binaries/matex/anticipate.mli @@ -9,12 +9,6 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val typeof: NCic.context -> NCic.term -> NCic.term - -val not_prop1: NCic.context -> NCic.term -> bool - -val not_prop2: NCic.context -> NCic.term -> bool - val process_top_term: string -> NCic.term -> NCic.term val process_obj: NCic.obj_kind -> NCic.obj_kind diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml index 165986b47..0174af613 100644 --- a/matita/components/binaries/matex/engine.ml +++ b/matita/components/binaries/matex/engine.ml @@ -26,6 +26,7 @@ module K = Kernel module T = TeX module O = TeXOutput module A = Anticipate +module N = Alpha type status = { n: string; (* reference name *) @@ -95,7 +96,7 @@ let proc_term is c t = try proc_term is c t with let typeof c = function | C.Appl [t] - | t -> A.typeof c t + | t -> K.whd_typeof c t let init () = { n = ""; s = [1] @@ -142,19 +143,19 @@ let rec proc_proof st ris c t = match t with let ris = mk_open st ris in proc_proof (next st) (mk_dec "PRIM" is_w s ris) (K.add_dec s w c) t | C.Appl (t0 :: ts) -> - let rts = X.rev_neg_filter (A.not_prop2 c) [t0] ts in + let rts = X.rev_neg_filter (K.not_prop2 c) [t0] ts in let ris = T.Macro "STEP" :: mk_inferred st c t ris in let tts = L.rev_map (proc_term [] c) rts in mk_exit st (T.rev_mk_args tts ris) | C.Match (w, u, v, ts) -> - let rts = X.rev_neg_filter (A.not_prop2 c) [v] ts in + let rts = X.rev_neg_filter (K.not_prop2 c) [v] ts in let ris = T.Macro "DEST" :: mk_inferred st c t ris in let tts = L.rev_map (proc_term [] c) rts in mk_exit st (T.rev_mk_args tts ris) | C.LetIn (s, w, v, t) -> let is_w = proc_term [] c w in let ris = mk_open st ris in - if A.not_prop1 c w then + if K.not_prop1 c w then let is_v = proc_term [] c v in let ris = T.Group is_v :: T.Macro "BODY" :: mk_dec "DECL" is_w s ris in proc_proof (next st) ris (K.add_def s w v c) t @@ -176,13 +177,15 @@ let proc_proof rs c t = try proc_proof (init ()) rs c t with let note = T.Note "This file was automatically generated by MaTeX: do not edit" -let proc_item item s t = +let proc_item item s ss t = + 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 s :: proc_term is [] t + note :: T.Macro "begin" :: T.arg item :: T.arg s :: T.free ss :: proc_term is [] tt -let proc_top_proof s t = - let tt = A.process_top_term s t in (* anticipation *) - let ris = [T.free s; T.arg s; T.arg "proof"; T.Macro "begin"; note] in +let proc_top_proof s ss t = + 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 L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof ris [] tt) let open_out_tex s = @@ -197,20 +200,20 @@ let proc_pair s ss u = function | None -> let name = X.rev_map_concat X.id "." "type" ss in let och = open_out_tex name in - O.out_text och (proc_item "axiom" s u); + O.out_text och (proc_item "axiom" s name u); close_out och | Some t -> let text_u, text_t = - if A.not_prop1 [] u then proc_item "declaration", proc_item "definition" + if K.not_prop1 [] u then proc_item "declaration", proc_item "definition" else proc_item "proposition", proc_top_proof in let name = X.rev_map_concat X.id "." "type" ss in let och = open_out_tex name in - O.out_text och (text_u s u); + O.out_text och (text_u s name u); close_out och; let name = X.rev_map_concat X.id "." "body" ss in let och = open_out_tex name in - O.out_text och (text_t s t); + O.out_text och (text_t s name t); close_out och let proc_fun ss (r, s, i, u, t) = diff --git a/matita/components/binaries/matex/ground.ml b/matita/components/binaries/matex/ground.ml index c24162ae0..0e9f28c55 100644 --- a/matita/components/binaries/matex/ground.ml +++ b/matita/components/binaries/matex/ground.ml @@ -19,6 +19,8 @@ exception Error of string let id x = x +let id2 x y = x, y + let rec segments_of_string ss l s = match try Some (S.index s '/') with Not_found -> None with | None -> s :: ss diff --git a/matita/components/binaries/matex/ground.mli b/matita/components/binaries/matex/ground.mli index 5c02eb9d1..90ef8ddd5 100644 --- a/matita/components/binaries/matex/ground.mli +++ b/matita/components/binaries/matex/ground.mli @@ -17,6 +17,8 @@ val log: string -> unit val id: 'a -> 'a +val id2: 'a -> 'b -> 'a * 'b + val segments_of_string: string list -> int -> string -> string list val rev_map_concat: ('a -> string) -> string -> string -> 'a list -> string diff --git a/matita/components/binaries/matex/kernel.ml b/matita/components/binaries/matex/kernel.ml index f9ed0c466..17116677c 100644 --- a/matita/components/binaries/matex/kernel.ml +++ b/matita/components/binaries/matex/kernel.ml @@ -44,12 +44,16 @@ let init () = H.set_log_callback no_log; let u0 = mk_type_universe "0" in let u1 = mk_type_universe "1" in - E.add_lt_constraint u0 u1 + E.add_lt_constraint ~acyclic:true u0 u1 let fst_var = 1 let snd_var = 2 +let appl ts = C.Appl ts + +let prod s w t = C.Prod (s, w, t) + let lambda s w t = C.Lambda (s, w, t) let letin s w v t = C.LetIn (s, w, v, t) @@ -93,6 +97,17 @@ let whd c t = let typeof c t = K.typeof G.status [] [] c t +let whd_typeof c t = whd c (typeof c t) + +let not_prop1 c u = match whd_typeof c u with + | C.Sort (C.Prop) -> false + | _ -> true + +let not_prop2 c t = not_prop1 c (typeof c t) + +let does_not_occur i c t = + K.does_not_occur G.status ~subst:[] c 0 i t + let segments_of_uri u = let s = U.string_of_uri u in let s = F.chop_extension s in diff --git a/matita/components/binaries/matex/matex.ml b/matita/components/binaries/matex/matex.ml index 7e296aa03..46ef1c894 100644 --- a/matita/components/binaries/matex/matex.ml +++ b/matita/components/binaries/matex/matex.ml @@ -24,20 +24,25 @@ 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_l = " Output the list of generated files in this file" let help_p = " omit types (default: no)" -let help_t = " Test anticipation (default: no)" +let help_t = " Test term transformations (default: no)" let help = "" (* internal functions *******************************************************) +let alpha_decode = R.triple R.string R.string R.string + let init registry = R.load_from registry; if !G.no_init then begin K.init (); G.no_init := false; - end + end; + G.alpha_type := R.get_list alpha_decode "matex.alpha.type"; + G.alpha_sort := R.get_list alpha_decode "matex.alpha.sort" let is_registry s = F.check_suffix s ".conf.xml" @@ -63,6 +68,7 @@ begin try A.parse [ "-O", A.String ((:=) G.out_dir), help_O; "-X", A.Unit G.clear, help_X; + "-a", A.Set G.log_alpha, help_a; "-l", A.String set_list, help_l; "-p", A.Set G.no_types, help_p; "-t", A.Set G.test, help_t; diff --git a/matita/components/binaries/matex/options.ml b/matita/components/binaries/matex/options.ml index ba1f39849..8b94b003d 100644 --- a/matita/components/binaries/matex/options.ml +++ b/matita/components/binaries/matex/options.ml @@ -26,23 +26,33 @@ let default_test = false let default_no_types = false +let default_log_alpha = false + let default_list_och = None +let default_alpha = [] + (* interface ****************************************************************) let status = new P.status let no_init = ref default_no_init -let out_dir = ref default_out_dir (* directory of generated files *) +let out_dir = ref default_out_dir (* directory of generated files *) + +let proc_id = ref default_proc_id (* identifer of anticipations *) + +let test = ref default_test (* test anticipation *) + +let no_types = ref default_no_types (* omit types *) -let proc_id = ref default_proc_id (* identifer of anticipations *) +let log_alpha = ref default_log_alpha (* log alpha-unconverted identifiers *) -let test = ref default_test (* test anticipation *) +let list_och = ref default_list_och (* output stream for list file *) -let no_types = ref default_no_types (* omit types *) +let alpha_type = ref default_alpha (* data of type-based alpha-conversion *) -let list_och = ref default_list_och (* output stream for list file *) +let alpha_sort = ref default_alpha (* data of sort-based alpha-conversion *) let close_list () = match !list_och with | None -> () @@ -55,4 +65,7 @@ let clear () = proc_id := default_proc_id; test := default_test; no_types := default_no_types; - list_och := default_list_och + log_alpha := default_log_alpha; + list_och := default_list_och; + alpha_type := default_alpha; + alpha_sort := default_alpha diff --git a/matita/components/binaries/matex/options.mli b/matita/components/binaries/matex/options.mli index 4629423c5..15a272520 100644 --- a/matita/components/binaries/matex/options.mli +++ b/matita/components/binaries/matex/options.mli @@ -21,8 +21,14 @@ val test: bool ref val no_types: bool ref +val log_alpha: 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 clear: unit -> unit val close_list: unit -> unit diff --git a/matita/components/binaries/matex/test/Makefile b/matita/components/binaries/matex/test/Makefile index 00db5d193..cb19e9a6d 100644 --- a/matita/components/binaries/matex/test/Makefile +++ b/matita/components/binaries/matex/test/Makefile @@ -6,7 +6,7 @@ UNLOG = ./unlog.pl MAIN = test -SOURCES = $(shell cat Make) $(shell cat Make.objs) +SOURCES = $(shell cat Make) $(shell cat Make.srcs) all: $(MAIN).dvi @@ -38,4 +38,4 @@ $(MAIN).tar: $(MAIN).log $(UNLOG) $< $@ objs.tex: - @sed "s/\(.*\).tex/\\\\input{\1}/" Make.objs > $@ + @sed "s/\(.*\).tex/\\\\input{\1}/" Make.srcs > $@ diff --git a/matita/components/binaries/matex/test/basic_1.conf.xml b/matita/components/binaries/matex/test/basic_1.conf.xml new file mode 100644 index 000000000..d9d2d67dc --- /dev/null +++ b/matita/components/binaries/matex/test/basic_1.conf.xml @@ -0,0 +1,129 @@ + + +
+ matita.lambdadelta.basic_1.T.defs.B.B.type b I + matita.lambdadelta.basic_1.T.defs.B.B.type ee I + matita.lambdadelta.basic_1.T.defs.B.B.type x I + + matita.lambdadelta.basic_1.T.defs.F.F.type ee I + matita.lambdadelta.basic_1.T.defs.F.F.type f I + matita.lambdadelta.basic_1.T.defs.F.F.type x I + + matita.lambdadelta.basic_1.T.defs.K.K.type e I + matita.lambdadelta.basic_1.T.defs.K.K.type ee I + matita.lambdadelta.basic_1.T.defs.K.K.type k I + matita.lambdadelta.basic_1.T.defs.K.K.type h I + matita.lambdadelta.basic_1.T.defs.K.K.type x I + + matita.lambdadelta.basic_1.C.defs.C.C.type _ X + matita.lambdadelta.basic_1.C.defs.C.C.type a X + matita.lambdadelta.basic_1.C.defs.C.C.type c L + matita.lambdadelta.basic_1.C.defs.C.C.type d L + matita.lambdadelta.basic_1.C.defs.C.C.type e K + matita.lambdadelta.basic_1.C.defs.C.C.type ee X + matita.lambdadelta.basic_1.C.defs.C.C.type x X + matita.lambdadelta.basic_1.C.defs.C.C.type y Y + + matita.lambdadelta.basic_1.T.defs.T.T.type _ X + matita.lambdadelta.basic_1.T.defs.T.T.type e X + matita.lambdadelta.basic_1.T.defs.T.T.type ee X + matita.lambdadelta.basic_1.T.defs.T.T.type t T + matita.lambdadelta.basic_1.T.defs.T.T.type u U + matita.lambdadelta.basic_1.T.defs.T.T.type v V + matita.lambdadelta.basic_1.T.defs.T.T.type w W + matita.lambdadelta.basic_1.T.defs.T.T.type wi W + matita.lambdadelta.basic_1.T.defs.T.T.type x X + matita.lambdadelta.basic_1.T.defs.T.T.type y Y + matita.lambdadelta.basic_1.T.defs.T.T.type z Z + + matita.lambdadelta.basic_1.tlist.defs.TList.TList.type _ Xs + matita.lambdadelta.basic_1.tlist.defs.TList.TList.type e Xs + matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ee Xs + matita.lambdadelta.basic_1.tlist.defs.TList.TList.type t Ts + matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ts Ts + matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ul Us + matita.lambdadelta.basic_1.tlist.defs.TList.TList.type us Us + matita.lambdadelta.basic_1.tlist.defs.TList.TList.type vs Vs + matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ws Ws + matita.lambdadelta.basic_1.tlist.defs.TList.TList.type xs Xs + matita.lambdadelta.basic_1.tlist.defs.TList.TList.type x Xs + matita.lambdadelta.basic_1.tlist.defs.TList.TList.type y Ys + + matita.lambdadelta.basic_1.A.defs.A.A.type _ X + matita.lambdadelta.basic_1.A.defs.A.A.type a A + matita.lambdadelta.basic_1.A.defs.A.A.type b B + matita.lambdadelta.basic_1.A.defs.A.A.type e X + matita.lambdadelta.basic_1.A.defs.A.A.type ee X + matita.lambdadelta.basic_1.A.defs.A.A.type l X + matita.lambdadelta.basic_1.A.defs.A.A.type x X + matita.lambdadelta.basic_1.A.defs.A.A.type y Y + + matita.lambdadelta.basic_1.G.defs.G.G.type g h + + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type _ x + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type d' d + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type d d + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type e e + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type ee e + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type f f + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type g g + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type h h + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type i i + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type j j + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type k k + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type l l + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type m m + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type n n + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type next f + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type v v + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type w w + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type x x + matita.lambdadelta.legacy_1.coq.defs.nat.nat.type y y + + matita.lambdadelta.legacy_1.coq.defs.bool.bool.type b b + matita.lambdadelta.legacy_1.coq.defs.bool.bool.type x x + + matita.lambdadelta.ground_1.plist.defs.PList.PList.type _ f + matita.lambdadelta.ground_1.plist.defs.PList.PList.type e f + matita.lambdadelta.ground_1.plist.defs.PList.PList.type ee f + matita.lambdadelta.ground_1.plist.defs.PList.PList.type hds f + matita.lambdadelta.ground_1.plist.defs.PList.PList.type is f + matita.lambdadelta.ground_1.plist.defs.PList.PList.type p f + matita.lambdadelta.ground_1.plist.defs.PList.PList.type q f + matita.lambdadelta.ground_1.plist.defs.PList.PList.type y f + + Prop P R + Prop Q R + + Type[cic:/matita/pts/Type0.univ] P S + + Prop H H + Prop Hle H + Prop IH IH + Prop IHc IH + Prop IHd IH + Prop IHe IH + Prop IHh IH + Prop IHi IH + Prop IHj IH + Prop IHn IH + Prop IHx IH + Prop a H + Prop c H + Prop d H + Prop e H + Prop f H + Prop g H + Prop h H + Prop i H + Prop l H + Prop n H + Prop p H + Prop s H + Prop t H + Prop w H + Prop x H + + Type[cic:/matita/pts/Type0.univ] f a +
+ diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty index a889be7ad..11becffe8 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/02/21 MaTeX Package] +\ProvidesPackage{matex}[2016/04/28 MaTeX Package] \RequirePackage{xcolor} \ExecuteOptions{} \ProcessOptions* @@ -16,22 +16,26 @@ \newcommand*\ma@prim{ma@purple} \newcommand*\ma@qed{ma@blue} -\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}} \newcommand*\neverindent{\setlength\parindent{0pt}} -\newcommand*\ObjLabel[1]{\label{obj:#1}} -\newcommand*\ObjRef[1]{\ref{obj:#1}} +%\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}} +%\newcommand*\ObjLabel[1]{\label{obj:#1}\hypertarget{obj:#1}{}} +%\newcommand*\ObjRef[1]{\hyperlink{obj:#1}{\ref*{obj:#1}}} +%\newcommand*\ma@setlabel[2]{\setlabel{#1}\ObjLabel{#2}} + +\newcommand*\ma@settarget[2]{\hypertarget{obj:#2}{}} +\newcommand*\ma@setlink[2]{\hyperlink{obj:#2}{#1}} + \newcommand*\ObjIncNode{} \newcommand*\ObjNode{} -\newcommand*\ma@setlabel[2]{\setlabel{#1}\ObjLabel{#2}} \newcommand*\ma@thehead[2]{\ObjIncNode\textbf{#1 \ObjNode(#2)}\neverindent\par} \newcommand*\ma@theneck[1]{\textsl{#1}\neverindent\par} -\newenvironment{axiom}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Axiom}{#1}}{\par} -\newenvironment{declaration}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Declaration}{#1}}{\par} +\newenvironment{axiom}[2]{\ma@settarget{#1}{#2}\ma@thehead{Axiom}{#1}}{\par} +\newenvironment{declaration}[2]{\ma@settarget{#1}{#2}\ma@thehead{Declaration}{#1}}{\par} \newenvironment{definition}[2]{}{\par} -\newenvironment{proposition}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Proposition}{#1}}{\par} +\newenvironment{proposition}[2]{\ma@settarget{#1}{#2}\ma@thehead{Proposition}{#1}}{\par} \newenvironment{proof}[2]{\ma@theneck{Proof}}{\par} \newenvironment{ma@step}[1]{\color{#1}}{\par} @@ -46,7 +50,7 @@ \newcommand*\CROP[1]{CROP} \newcommand*\TYPE[1]{TYPE} \newcommand*\LREF[2]{#1} -\newcommand*\GREF[2]{#1} +\newcommand*\GREF[2]{\ma@setlink{#1}{#2}} \newcommand*\ABBR[3]{(D #1 #2 #3) } \newcommand*\ABST[2]{(I #1 #2) } \newcommand*\PROD[2]{(P #1 #2) } diff --git a/matita/components/binaries/matex/test/test.tex b/matita/components/binaries/matex/test/test.tex index a85f8c8f6..fe150474c 100644 --- a/matita/components/binaries/matex/test/test.tex +++ b/matita/components/binaries/matex/test/test.tex @@ -12,10 +12,4 @@ \input{objs} -\bigskip - -\ObjRef{pr0} -\ObjRef{pr0_ind} -\ObjRef{pr0_confluence} - \end{document} diff --git a/matita/components/registry/helm_registry.ml b/matita/components/registry/helm_registry.ml index fd0df5013..877de0a1c 100644 --- a/matita/components/registry/helm_registry.ml +++ b/matita/components/registry/helm_registry.ml @@ -115,6 +115,12 @@ let pair fst_unmarshaller snd_unmarshaller v = | [fst; snd] -> fst_unmarshaller fst, snd_unmarshaller snd | _ -> raise (Type_error "not a pair") +(* FG *) +let triple fst_unmarshaller snd_unmarshaller trd_unmarshaller v = + match Str.split spaces_rex v with + | [fst; snd; trd] -> fst_unmarshaller fst, snd_unmarshaller snd, trd_unmarshaller trd + | _ -> raise (Type_error "not a triple") + (* escapes for xml configuration file *) let (escape, unescape) = let (in_enc, out_enc) = (`Enc_utf8, `Enc_utf8) in @@ -210,6 +216,10 @@ let get_list registry unmarshaller key = let get_pair registry fst_unmarshaller snd_unmarshaller = get_typed registry (pair fst_unmarshaller snd_unmarshaller) +(* FG *) +let get_triple registry fst_unmarshaller snd_unmarshaller trd_unmarshaller = + get_typed registry (triple fst_unmarshaller snd_unmarshaller trd_unmarshaller) + let set_list registry marshaller ~key ~value = (* since ocaml hash table are crazy... *) while Hashtbl.mem registry key do @@ -413,6 +423,7 @@ let get_opt unmarshaller = get_opt default_registry unmarshaller 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 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 77c6f6cc3..68434603d 100644 --- a/matita/components/registry/helm_registry.mli +++ b/matita/components/registry/helm_registry.mli @@ -133,6 +133,7 @@ val int: string -> int 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 (** {3 Typed getters} *) @@ -150,6 +151,9 @@ val get_list: (string -> 'a) -> string -> 'a list (** decode values which are blank separated list of values, of length 2 *) 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 + (** {4 Shorthands} *) val get_string: string -> string -- 2.39.2