From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 30 Apr 2016 21:33:47 +0000 (+0000)
Subject: - matex: support for alpha-conversion completed
X-Git-Tag: make_still_working~595
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2fa001c86e37c76c840122655cb4ffba8bb30cad;p=helm.git

- matex: support for alpha-conversion completed
- matex.sty: hyperlinks without labels
- registry: support or triples
---

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 = "<dir> Set this output directory"
 let help_X = " Clear configuration and options"
+let help_a = " Log alpha-unconverted identifiers (default: no)"
 let help_l = "<file> 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 @@
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+  <section name="matex.alpha">
+    <key name="type">matita.lambdadelta.basic_1.T.defs.B.B.type b I</key>
+    <key name="type">matita.lambdadelta.basic_1.T.defs.B.B.type ee I</key>
+    <key name="type">matita.lambdadelta.basic_1.T.defs.B.B.type x I</key>
+
+    <key name="type">matita.lambdadelta.basic_1.T.defs.F.F.type ee I</key>
+    <key name="type">matita.lambdadelta.basic_1.T.defs.F.F.type f I</key>
+    <key name="type">matita.lambdadelta.basic_1.T.defs.F.F.type x I</key>
+
+    <key name="type">matita.lambdadelta.basic_1.T.defs.K.K.type e I</key>
+    <key name="type">matita.lambdadelta.basic_1.T.defs.K.K.type ee I</key>
+    <key name="type">matita.lambdadelta.basic_1.T.defs.K.K.type k I</key>
+    <key name="type">matita.lambdadelta.basic_1.T.defs.K.K.type h I</key>
+    <key name="type">matita.lambdadelta.basic_1.T.defs.K.K.type x I</key>
+
+    <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type _ X</key>
+    <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type a X</key>
+    <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type c L</key>
+    <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type d L</key>
+    <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type e K</key>
+    <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type ee X</key>
+    <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type x X</key>
+    <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type y Y</key>
+
+    <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type _ X</key>
+    <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type e X</key>
+    <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type ee X</key>
+    <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type t T</key>
+    <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type u U</key>
+    <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type v V</key>
+    <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type w W</key>
+    <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type wi W</key>
+    <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type x X</key>
+    <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type y Y</key>
+    <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type z Z</key>
+
+    <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type _ Xs</key>
+    <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type e Xs</key>
+    <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ee Xs</key>
+    <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type t Ts</key>
+    <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ts Ts</key>
+    <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ul Us</key>
+    <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type us Us</key>
+    <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type vs Vs</key>
+    <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ws Ws</key>
+    <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type xs Xs</key>
+    <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type x Xs</key>
+    <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type y Ys</key>
+
+    <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type _ X</key>
+    <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type a A</key>
+    <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type b B</key>
+    <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type e X</key>
+    <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type ee X</key>
+    <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type l X</key>
+    <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type x X</key>
+    <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type y Y</key>
+
+    <key name="type">matita.lambdadelta.basic_1.G.defs.G.G.type g h</key>
+
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type _ x</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type d' d</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type d d</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type e e</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type ee e</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type f f</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type g g</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type h h</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type i i</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type j j</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type k k</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type l l</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type m m</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type n n</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type next f</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type v v</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type w w</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type x x</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type y y</key>
+
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.bool.bool.type b b</key>
+    <key name="type">matita.lambdadelta.legacy_1.coq.defs.bool.bool.type x x</key>
+
+    <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type _ f</key>
+    <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type e f</key>
+    <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type ee f</key>
+    <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type hds f</key>
+    <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type is f</key>
+    <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type p f</key>
+    <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type q f</key>
+    <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type y f</key>
+
+    <key name="type">Prop P R</key>
+    <key name="type">Prop Q R</key>
+
+    <key name="type">Type[cic:/matita/pts/Type0.univ] P S</key>
+
+    <key name="sort">Prop H H</key>
+    <key name="sort">Prop Hle H</key>
+    <key name="sort">Prop IH IH</key>
+    <key name="sort">Prop IHc IH</key>
+    <key name="sort">Prop IHd IH</key>
+    <key name="sort">Prop IHe IH</key>
+    <key name="sort">Prop IHh IH</key>
+    <key name="sort">Prop IHi IH</key>
+    <key name="sort">Prop IHj IH</key>
+    <key name="sort">Prop IHn IH</key>
+    <key name="sort">Prop IHx IH</key>
+    <key name="sort">Prop a H</key>
+    <key name="sort">Prop c H</key>
+    <key name="sort">Prop d H</key>
+    <key name="sort">Prop e H</key>
+    <key name="sort">Prop f H</key>
+    <key name="sort">Prop g H</key>
+    <key name="sort">Prop h H</key>
+    <key name="sort">Prop i H</key>
+    <key name="sort">Prop l H</key>
+    <key name="sort">Prop n H</key>
+    <key name="sort">Prop p H</key>
+    <key name="sort">Prop s H</key>
+    <key name="sort">Prop t H</key>
+    <key name="sort">Prop w H</key>
+    <key name="sort">Prop x H</key>
+
+    <key name="sort">Type[cic:/matita/pts/Type0.univ] f a</key>
+  </section>
+</helm_registry>
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