From 348f1670b30f52db99187b2e92b45348e18ebbbe Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 23 May 2016 20:27:38 +0000
Subject: [PATCH] initial support for LaTeX-defined notatopn

---
 matita/components/binaries/matex/Makefile     |  3 +-
 matita/components/binaries/matex/alpha.ml     |  9 +-
 matita/components/binaries/matex/engine.ml    | 32 +++++--
 matita/components/binaries/matex/kernel.ml    |  9 +-
 matita/components/binaries/matex/matex.ml     |  5 +-
 matita/components/binaries/matex/options.ml   | 11 ++-
 matita/components/binaries/matex/options.mli  |  2 +
 .../binaries/matex/test/basic_1.conf.xml      | 90 +++++++++++++++++++
 .../binaries/matex/test/basic_1.sty           | 10 +++
 .../binaries/matex/test/ground_1.conf.xml     | 28 ++++++
 .../binaries/matex/test/ground_1.sty          | 10 +++
 .../binaries/matex/test/legacy_1.conf.xml     | 17 ++++
 .../binaries/matex/test/legacy_1.sty          | 10 +++
 .../components/binaries/matex/test/test.tex   |  9 ++
 14 files changed, 228 insertions(+), 17 deletions(-)
 create mode 100644 matita/components/binaries/matex/test/basic_1.sty
 create mode 100644 matita/components/binaries/matex/test/ground_1.conf.xml
 create mode 100644 matita/components/binaries/matex/test/ground_1.sty
 create mode 100644 matita/components/binaries/matex/test/legacy_1.conf.xml
 create mode 100644 matita/components/binaries/matex/test/legacy_1.sty

diff --git a/matita/components/binaries/matex/Makefile b/matita/components/binaries/matex/Makefile
index e177cc077..c9a7b58ed 100644
--- a/matita/components/binaries/matex/Makefile
+++ b/matita/components/binaries/matex/Makefile
@@ -6,7 +6,8 @@ REQUIRES = helm-ng_library
 include ../Makefile.common
 
 PROBE    = ../probe/probe.native
-REGISTRY = $(RT_BASE_DIR)/matita.conf.xml test/basic_1.conf.xml
+REGISTRY = $(RT_BASE_DIR)/matita.conf.xml \
+           test/legacy_1.conf.xml test/ground_1.conf.xml test/basic_1.conf.xml
 OBJS     = Make.objs
 SRCS     = Make.srcs
 
diff --git a/matita/components/binaries/matex/alpha.ml b/matita/components/binaries/matex/alpha.ml
index 816edd4a5..4c4eccef7 100644
--- a/matita/components/binaries/matex/alpha.ml
+++ b/matita/components/binaries/matex/alpha.ml
@@ -73,11 +73,9 @@ let get_constant c t = match strip (K.whd c t) with
       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
+   | C.Const c                   ->
+      let s, _ = K.resolve_reference c in
+      s
    | _                           -> ""
 
 let read l s r =
@@ -173,6 +171,7 @@ try
    end;
    tt
 with
+   | E.ObjectNotFound s 
    | T.TypeCheckerFailure s
    | T.AssertFailure s           -> malformed (Lazy.force s)
 
diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml
index 7001fb99e..e9ec76e86 100644
--- a/matita/components/binaries/matex/engine.ml
+++ b/matita/components/binaries/matex/engine.ml
@@ -43,11 +43,29 @@ let internal s =
 let malformed s =
    X.error ("engine: malformed term: " ^ s)
 
+let missing s =
+   X.log ("engine: missing macro for " ^ s)
+
 (* generic term processing *)
 
 let mk_ptr st name = 
    if G.is_global_id name then P.sprintf "%s.%s" st.i name else ""
 
+let get_macro s =
+   let rec aux = function
+      | []                        -> "", G.nan
+      | (r, m, a) :: _ when r = s -> m, a
+      | _ :: tl                   -> aux tl
+   in
+   aux !G.macro
+
+let get_head = function
+   | C.Const c :: ts ->
+      let s, _ = K.resolve_reference c in
+      let macro, arity = get_macro s in
+      if arity = L.length ts then  Some (macro, ts) else begin missing s; None end 
+   | _               -> None
+
 let proc_sort st is = function
    | C.Prop             -> T.Macro "PROP" :: is
    | C.Type [`Type, u]  -> T.Macro "TYPE" :: T.arg (U.string_of_uri u) :: is
@@ -62,8 +80,12 @@ let rec proc_term st is = function
       let name = K.resolve_lref st.c m in
       T.Macro "LREF" :: T.arg name :: T.free (mk_ptr st name) :: is
    | C.Appl ts              ->
+      let macro, ts = match get_head ts with
+         | Some (macro, ts) -> macro, ts
+         | None             -> "APPL", ts
+      in
       let riss = L.rev_map (proc_term st []) ts in
-      T.Macro "APPL" :: T.mk_rev_args riss is
+      T.Macro macro :: T.mk_rev_args riss is
    | C.Prod (s, w, t)       ->
       let is_w = proc_term st [] w in
       let is_t = proc_term {st with c=K.add_dec s w st.c} is t in
@@ -79,11 +101,9 @@ let rec proc_term st is = function
       T.Macro "ABBR" :: T.arg s :: T.free (mk_ptr st s) :: T.Group is_w :: T.Group is_v :: is_t
    | C.Sort s               ->
       proc_sort st is s
-   | C.Const (R.Ref (u, r)) ->
-      let ss = K.segments_of_uri u in
-      let _, _, _, _, obj = E.get_checked_obj G.status u in  
-      let ss, name = K.name_of_reference ss (obj, r) in
-      T.Macro "GREF" :: T.arg name :: T.free (X.rev_map_concat X.id "." "type" ss) :: is
+   | C.Const c              ->
+      let s, name = K.resolve_reference c in
+      T.Macro "GREF" :: T.arg name :: T.free s :: is
    | C.Match (w, u, v, ts)  ->
       let is_w = proc_term st [] (C.Const w) in
       let is_u = proc_term st [] u in
diff --git a/matita/components/binaries/matex/kernel.ml b/matita/components/binaries/matex/kernel.ml
index 17116677c..8b6a81a3e 100644
--- a/matita/components/binaries/matex/kernel.ml
+++ b/matita/components/binaries/matex/kernel.ml
@@ -116,7 +116,7 @@ let segments_of_uri u =
    let s = S.sub s (i+2) (l-i-2) in
    X.segments_of_string [] (l-i-2) s
 
-let name_of_reference ss = function
+let names_of_reference ss = function
    | C.Constant (_, name, _, _, _), R.Decl      ->
       ss, name
    | C.Constant (_, name, _, _, _), R.Def _     ->
@@ -136,3 +136,10 @@ let name_of_reference ss = function
       (name :: ss), name
    | _                                          ->
       failwith "name_of_reference"
+
+let resolve_reference = function
+   | R.Ref (u, r) ->
+      let ss = segments_of_uri u in
+      let _, _, _, _, obj = E.get_checked_obj G.status u in  
+      let ss, name = names_of_reference ss (obj, r) in
+      X.rev_map_concat X.id "." "type" ss, name
diff --git a/matita/components/binaries/matex/matex.ml b/matita/components/binaries/matex/matex.ml
index 9ca51c1fe..24775c0a6 100644
--- a/matita/components/binaries/matex/matex.ml
+++ b/matita/components/binaries/matex/matex.ml
@@ -36,6 +36,8 @@ let help   = ""
 
 let alpha_decode = R.triple R.string R.string R.string
 
+let macro_decode = R.triple R.string R.string R.int
+
 let init registry =
    R.load_from registry; 
    if !G.no_init then begin
@@ -43,7 +45,8 @@ let init registry =
       G.no_init := false;
    end;
    G.alpha_type := R.get_list alpha_decode "matex.alpha.type";
-   G.alpha_sort := R.get_list alpha_decode "matex.alpha.sort"
+   G.alpha_sort := R.get_list alpha_decode "matex.alpha.sort";
+   G.macro      := R.get_list macro_decode "matex.macro"
 
 let is_registry s =
    F.check_suffix s ".conf.xml"
diff --git a/matita/components/binaries/matex/options.ml b/matita/components/binaries/matex/options.ml
index da60a79bb..3b4c39d41 100644
--- a/matita/components/binaries/matex/options.ml
+++ b/matita/components/binaries/matex/options.ml
@@ -34,6 +34,8 @@ let default_list_och = None
 
 let default_alpha = []
 
+let default_macro = []
+
 (* interface ****************************************************************)
 
 let dno_id = "_"                            (* identifier for not-occurring premises *)
@@ -58,9 +60,11 @@ let log_alpha = ref default_log_alpha       (* log alpha-unconverted identifiers
 
 let list_och = ref default_list_och         (* output stream for list file *)
 
-let alpha_type = ref default_alpha          (* data of type-based alpha-conversion *)
+let alpha_type = ref default_alpha          (* data for type-based alpha-conversion *)
+
+let alpha_sort = ref default_alpha          (* data for sort-based alpha-conversion *)
 
-let alpha_sort = ref default_alpha          (* data of sort-based alpha-conversion *)
+let macro = ref default_macro               (* data eta-conversion and macro rendering *)
 
 let is_global_id s =
    !global_alpha && s <> dno_id
@@ -80,4 +84,5 @@ let clear () =
    log_alpha := default_log_alpha;
    list_och := default_list_och;
    alpha_type := default_alpha;
-   alpha_sort := default_alpha
+   alpha_sort := default_alpha;
+   macro := default_macro
diff --git a/matita/components/binaries/matex/options.mli b/matita/components/binaries/matex/options.mli
index b2ad2cf47..8a7bbb8a2 100644
--- a/matita/components/binaries/matex/options.mli
+++ b/matita/components/binaries/matex/options.mli
@@ -35,6 +35,8 @@ val alpha_type: (string * string * string) list ref
 
 val alpha_sort: (string * string * string) list ref
 
+val macro: (string * string * int) list ref
+
 val clear: unit -> unit
 
 val close_list: unit -> unit
diff --git a/matita/components/binaries/matex/test/basic_1.conf.xml b/matita/components/binaries/matex/test/basic_1.conf.xml
index d9d2d67dc..6292ed4ce 100644
--- a/matita/components/binaries/matex/test/basic_1.conf.xml
+++ b/matita/components/binaries/matex/test/basic_1.conf.xml
@@ -126,4 +126,94 @@
 
     <key name="sort">Type[cic:/matita/pts/Type0.univ] f a</key>
   </section>
+<!--
+matita.lambdadelta.basic_1.A.defs.A.AHead.type
+matita.lambdadelta.basic_1.A.defs.A.ASort.type
+matita.lambdadelta.basic_1.A.fwd.A_rect.A_rect.type
+matita.lambdadelta.basic_1.aplus.defs.aplus.aplus.type
+matita.lambdadelta.basic_1.app.defs.app1.app1.type
+matita.lambdadelta.basic_1.app.defs.cbk.cbk.type
+matita.lambdadelta.basic_1.aprem.defs.aprem.aprem.type
+matita.lambdadelta.basic_1.arity.defs.arity.arity.type
+matita.lambdadelta.basic_1.asucc.defs.asucc.asucc.type
+matita.lambdadelta.basic_1.C.defs.C.CHead.type
+matita.lambdadelta.basic_1.C.defs.C.CSort.type
+matita.lambdadelta.basic_1.C.defs.cle.type
+matita.lambdadelta.basic_1.C.defs.clt.type
+matita.lambdadelta.basic_1.C.defs.CTail.CTail.type
+matita.lambdadelta.basic_1.C.defs.cweight.cweight.type
+matita.lambdadelta.basic_1.C.fwd.C_rect.C_rect.type
+matita.lambdadelta.basic_1.cimp.defs.cimp.type
+matita.lambdadelta.basic_1.clear.defs.clear.clear.type
+matita.lambdadelta.basic_1.clen.defs.clen.clen.type
+matita.lambdadelta.basic_1.cnt.defs.cnt.cnt.type
+matita.lambdadelta.basic_1.csuba.defs.csuba.csuba.type
+matita.lambdadelta.basic_1.csubc.defs.csubc.csubc.type
+matita.lambdadelta.basic_1.csubst0.defs.csubst0.csubst0.type
+matita.lambdadelta.basic_1.csubst1.defs.csubst1.csubst1.type
+matita.lambdadelta.basic_1.csubt.defs.csubt.csubt.type
+matita.lambdadelta.basic_1.csubv.defs.csubv.csubv.type
+matita.lambdadelta.basic_1.drop1.defs.drop1.drop1.type
+matita.lambdadelta.basic_1.drop1.defs.ptrans.ptrans.type
+matita.lambdadelta.basic_1.drop.defs.drop.drop.type
+matita.lambdadelta.basic_1.ex0.defs.leqz.leqz.type
+matita.lambdadelta.basic_1.flt.defs.flt.type
+matita.lambdadelta.basic_1.flt.defs.fweight.type
+matita.lambdadelta.basic_1.fsubst0.defs.fsubst0.fsubst0.type
+matita.lambdadelta.basic_1.G.defs.G.mk_G.type
+matita.lambdadelta.basic_1.G.defs.next.next.type
+matita.lambdadelta.basic_1.getl.defs.getl.getl.type
+matita.lambdadelta.basic_1.iso.defs.iso.iso.type
+matita.lambdadelta.basic_1.leq.defs.leq.leq.type
+matita.lambdadelta.basic_1.lift1.defs.lift1.lift1.type
+matita.lambdadelta.basic_1.lift1.defs.lifts1.lifts1.type
+matita.lambdadelta.basic_1.lift1.defs.trans.trans.type
+matita.lambdadelta.basic_1.lift.defs.lifts.lifts.type
+matita.lambdadelta.basic_1.lift.defs.lift.type
+matita.lambdadelta.basic_1.lift.defs.lref_map.lref_map.type
+matita.lambdadelta.basic_1.llt.defs.llt.type
+matita.lambdadelta.basic_1.llt.defs.lweight.lweight.type
+matita.lambdadelta.basic_1.next_plus.defs.next_plus.next_plus.type
+matita.lambdadelta.basic_1.nf2.defs.nf2.type
+matita.lambdadelta.basic_1.nf2.defs.nfs2.nfs2.type
+matita.lambdadelta.basic_1.pc1.defs.pc1.type
+matita.lambdadelta.basic_1.pc3.defs.pc3_left.pc3_left.type
+matita.lambdadelta.basic_1.pc3.defs.pc3.type
+matita.lambdadelta.basic_1.pr0.defs.pr0.pr0.type
+matita.lambdadelta.basic_1.pr1.defs.pr1.pr1.type
+matita.lambdadelta.basic_1.pr2.defs.pr2.pr2.type
+matita.lambdadelta.basic_1.pr3.defs.pr3.pr3.type
+matita.lambdadelta.basic_1.r.defs.r.type
+matita.lambdadelta.basic_1.sc3.defs.sc3.sc3.type
+matita.lambdadelta.basic_1.s.defs.s.type
+matita.lambdadelta.basic_1.sn3.defs.sn3.sn3.type
+matita.lambdadelta.basic_1.sn3.defs.sns3.sns3.type
+matita.lambdadelta.basic_1.sty0.defs.sty0.sty0.type
+matita.lambdadelta.basic_1.sty1.defs.sty1.sty1.type
+matita.lambdadelta.basic_1.subst0.defs.subst0.subst0.type
+matita.lambdadelta.basic_1.subst1.defs.subst1.subst1.type
+matita.lambdadelta.basic_1.subst.defs.subst.subst.type
+matita.lambdadelta.basic_1.T.defs.K.Bind.type
+matita.lambdadelta.basic_1.T.defs.K.Flat.type
+matita.lambdadelta.basic_1.T.defs.tle.type
+matita.lambdadelta.basic_1.T.defs.T.THead.type
+matita.lambdadelta.basic_1.T.defs.T.TLRef.type
+matita.lambdadelta.basic_1.T.defs.T.TSort.type
+matita.lambdadelta.basic_1.T.defs.tweight.tweight.type
+matita.lambdadelta.basic_1.T.fwd.T_rect.T_rect.type
+matita.lambdadelta.basic_1.tlist.defs.TApp.TApp.type
+matita.lambdadelta.basic_1.tlist.defs.THeads.THeads.type
+matita.lambdadelta.basic_1.tlist.defs.TList.TCons.type
+matita.lambdadelta.basic_1.tlist.defs.tslen.tslen.type
+matita.lambdadelta.basic_1.tlist.defs.tslt.type
+matita.lambdadelta.basic_1.tlt.defs.tlt.type
+matita.lambdadelta.basic_1.tlt.defs.wadd.type
+matita.lambdadelta.basic_1.tlt.defs.weight_map.weight_map.type
+matita.lambdadelta.basic_1.tlt.defs.weight.type
+matita.lambdadelta.basic_1.ty3.defs.ty3.ty3.type
+matita.lambdadelta.basic_1.ty3.defs.tys3.tys3.type
+matita.lambdadelta.basic_1.ty3.nf2.ty3_nf2_inv_abst_premise.type
+matita.lambdadelta.basic_1.wcpr0.defs.wcpr0.wcpr0.type
+matita.lambdadelta.basic_1.wf3.defs.wf3.wf3.type
+-->
 </helm_registry>
diff --git a/matita/components/binaries/matex/test/basic_1.sty b/matita/components/binaries/matex/test/basic_1.sty
new file mode 100644
index 000000000..270661075
--- /dev/null
+++ b/matita/components/binaries/matex/test/basic_1.sty
@@ -0,0 +1,10 @@
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesPackage{basic_1}[2016/05/23 Notation for "cic:/matita/lambdadelta/basic_1/"]
+\ExecuteOptions{}
+\ProcessOptions*
+
+\makeatletter
+
+\makeatother
+
+\endinput
diff --git a/matita/components/binaries/matex/test/ground_1.conf.xml b/matita/components/binaries/matex/test/ground_1.conf.xml
new file mode 100644
index 000000000..cb5860c1f
--- /dev/null
+++ b/matita/components/binaries/matex/test/ground_1.conf.xml
@@ -0,0 +1,28 @@
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+<!--
+matita.lambdadelta.ground_1.blt.defs.blt.blt.type
+matita.lambdadelta.ground_1.plist.defs.papp.papp.type
+matita.lambdadelta.ground_1.plist.defs.PConsTail.PConsTail.type
+matita.lambdadelta.ground_1.plist.defs.PList.PCons.type
+matita.lambdadelta.ground_1.plist.defs.Ss.Ss.type
+matita.lambdadelta.ground_1.types.defs.and3.and3.type
+matita.lambdadelta.ground_1.types.defs.ex2_2.ex2_2.type
+matita.lambdadelta.ground_1.types.defs.ex2_3.ex2_3.type
+matita.lambdadelta.ground_1.types.defs.ex_2.ex_2.type
+matita.lambdadelta.ground_1.types.defs.ex3_2.ex3_2.type
+matita.lambdadelta.ground_1.types.defs.ex3_3.ex3_3.type
+matita.lambdadelta.ground_1.types.defs.ex3_4.ex3_4.type
+matita.lambdadelta.ground_1.types.defs.ex_3.ex_3.type
+matita.lambdadelta.ground_1.types.defs.ex3.ex3.type
+matita.lambdadelta.ground_1.types.defs.ex4_2.ex4_2.type
+matita.lambdadelta.ground_1.types.defs.ex4_3.ex4_3.type
+matita.lambdadelta.ground_1.types.defs.ex4_4.ex4_4.type
+matita.lambdadelta.ground_1.types.defs.ex4_5.ex4_5.type
+matita.lambdadelta.ground_1.types.defs.ex4.ex4.type
+matita.lambdadelta.ground_1.types.defs.ex5_3.ex5_3.type
+matita.lambdadelta.ground_1.types.defs.ex6_6.ex6_6.type
+matita.lambdadelta.ground_1.types.defs.or3.or3.type
+matita.lambdadelta.ground_1.types.defs.or4.or4.type
+-->
+</helm_registry>
diff --git a/matita/components/binaries/matex/test/ground_1.sty b/matita/components/binaries/matex/test/ground_1.sty
new file mode 100644
index 000000000..582e49cef
--- /dev/null
+++ b/matita/components/binaries/matex/test/ground_1.sty
@@ -0,0 +1,10 @@
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesPackage{ground_1}[2016/05/23 Notation for "cic:/matita/lambdadelta/ground_1/"]
+\ExecuteOptions{}
+\ProcessOptions*
+
+\makeatletter
+
+\makeatother
+
+\endinput
diff --git a/matita/components/binaries/matex/test/legacy_1.conf.xml b/matita/components/binaries/matex/test/legacy_1.conf.xml
new file mode 100644
index 000000000..056d1dc31
--- /dev/null
+++ b/matita/components/binaries/matex/test/legacy_1.conf.xml
@@ -0,0 +1,17 @@
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+<!--
+matita.lambdadelta.legacy_1.coq.defs.eq.eq.type
+matita.lambdadelta.legacy_1.coq.defs.ex2.ex2.type
+matita.lambdadelta.legacy_1.coq.defs.ex.ex.type
+matita.lambdadelta.legacy_1.coq.defs.land.land.type
+matita.lambdadelta.legacy_1.coq.defs.le.le.type
+matita.lambdadelta.legacy_1.coq.defs.lt.type
+matita.lambdadelta.legacy_1.coq.defs.minus.minus.type
+matita.lambdadelta.legacy_1.coq.defs.nat.S.type
+matita.lambdadelta.legacy_1.coq.defs.not.type
+matita.lambdadelta.legacy_1.coq.defs.or.or.type
+matita.lambdadelta.legacy_1.coq.defs.plus.plus.type
+matita.lambdadelta.legacy_1.coq.defs.pred.type
+-->
+</helm_registry>
diff --git a/matita/components/binaries/matex/test/legacy_1.sty b/matita/components/binaries/matex/test/legacy_1.sty
new file mode 100644
index 000000000..d33196fb2
--- /dev/null
+++ b/matita/components/binaries/matex/test/legacy_1.sty
@@ -0,0 +1,10 @@
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesPackage{lambdadelta_1}[2016/05/23 Notation for "cic:/matita/lambdadelta/legacy_1/"]
+\ExecuteOptions{}
+\ProcessOptions*
+
+\makeatletter
+
+\makeatother
+
+\endinput
diff --git a/matita/components/binaries/matex/test/test.tex b/matita/components/binaries/matex/test/test.tex
index fe150474c..26adf2224 100644
--- a/matita/components/binaries/matex/test/test.tex
+++ b/matita/components/binaries/matex/test/test.tex
@@ -3,13 +3,22 @@
 \usepackage[bookmarks=false,ps2pdf]{hyperref}
 \usepackage[american]{babel}
 \usepackage{matex}
+\usepackage{legacy_1}
+\usepackage{ground_1}
+\usepackage{basic_1}
 
 \newcounter{node}
 \renewcommand*\ObjIncNode{\stepcounter{node}}
 \renewcommand*\ObjNode{\arabic{node} }
 
+\title{The Core Theory of the Formal System $\lambda\delta\hbox{-}1$}
+
+\author{Ferruccio Guidi}
+
 \begin{document}
 
+\maketitle
+
 \input{objs}
 
 \end{document}
-- 
2.39.2