From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 11 Jan 2016 16:46:16 +0000 (+0000)
Subject: - plain anticipation for CIC proofs terms
X-Git-Tag: make_still_working~663
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ea6b4322051d3eb1794bfca3928f6e1773f971ba;p=helm.git

- plain anticipation for CIC proofs terms
- support for (co)fixpoint objects
- Makefile for testing
- minor updates
---

diff --git a/matita/components/binaries/matex/Makefile b/matita/components/binaries/matex/Makefile
index 42e1360e2..4e1e3ca66 100644
--- a/matita/components/binaries/matex/Makefile
+++ b/matita/components/binaries/matex/Makefile
@@ -7,10 +7,11 @@ include ../Makefile.common
 
 REGISTRY = $(RT_BASE_DIR)/matita.conf.xml
 
-OBJ = cic:/matita/lambdadelta/basic_1/pr0/pr0/pr0_confluence.con
+OBJS = cic:/matita/lambdadelta/basic_1/pr0/pr0/pr0_confluence.con\
+       cic:/matita/lambdadelta/basic_1/pr0/defs/pr0_ind.con
 
 test:
-	@echo MaTeX $(OBJ)
-	$(H)./matex.native -O test $(REGISTRY) $(OBJ)
+	@echo MaTeX: $(OBJS:cic:/matita/lambdadelta/basic_1/pr0/%.con=%)
+	$(H)./matex.native -O test -t -p $(REGISTRY) $(OBJS)
 
 .PHONY: test
diff --git a/matita/components/binaries/matex/TeX.ml b/matita/components/binaries/matex/TeX.ml
index c213d4d96..184a6937c 100644
--- a/matita/components/binaries/matex/TeX.ml
+++ b/matita/components/binaries/matex/TeX.ml
@@ -11,7 +11,10 @@
 
 module L = List
 
+module X = Ground
+
 type item = Free  of string  (* free text *)
+          | Text  of string  (* quoted text *)
           | Macro of string  (* macro *)
           | Group of text    (* group *)
          
@@ -19,16 +22,17 @@ and text = item list         (* structured text *)
 
 let file_ext = ".tex"
 
-let empty = [Free ""]
-
-let newline = [Free "%\n"]
-
 let group s = Group s
 
-let arg s = Group [Free s]
+let arg s = Group [Text s]
 
-let mk_rev_args riss =
-   L.rev_map group (empty :: riss)
+let free s = Group [Free s]
 
 let mk_segs us =
    L.rev_map arg ("" :: (L.rev us))
+
+let mk_rev_args riss =
+   L.rev_map group ([] :: riss)
+
+let rev_mk_args iss is =
+   free "" :: X.rev_map_append group iss is
diff --git a/matita/components/binaries/matex/TeXOutput.ml b/matita/components/binaries/matex/TeXOutput.ml
index 053c890bb..f92101c30 100644
--- a/matita/components/binaries/matex/TeXOutput.ml
+++ b/matita/components/binaries/matex/TeXOutput.ml
@@ -13,19 +13,25 @@ module L = List
 module P = Printf
 module S = String
 
+module X = Ground
 module T = TeX
 
 (* internal functions *******************************************************)
 
 let special = "\\{}$&#^_~%" (* LaTeX reserves these characters *)
 
-let quote c =
-   if S.contains special c then '.' else c
+let special = [
+   '_', "\\_";
+]
+
+let quote s c = try s ^ L.assoc c special with
+   | Not_found -> s ^ S.make 1 c 
 
 let rec out_item och = function
-   | T.Free s  -> P.fprintf och "%s" (S.map quote s)
-   | T.Macro s -> P.fprintf och "\\%s" s
-   | T.Group t -> P.fprintf och "%%\n{%a}" out_text t
+   | T.Free s  -> P.fprintf och "%s" s
+   | T.Text s  -> P.fprintf och "%s" (X.fold_string quote "" s)
+   | T.Macro s -> P.fprintf och "\\%s%%\n" s
+   | T.Group t -> P.fprintf och "{%a}%%\n" out_text t
 
 (* interface functions ******************************************************)
 
diff --git a/matita/components/binaries/matex/anticipate.ml b/matita/components/binaries/matex/anticipate.ml
new file mode 100644
index 000000000..1681d2d03
--- /dev/null
+++ b/matita/components/binaries/matex/anticipate.ml
@@ -0,0 +1,147 @@
+(*
+    ||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 C = NCic
+module T = NCicTypeChecker
+
+module X = Ground
+module G = Options
+module K = Kernel
+
+(* internal functions *******************************************************)
+
+let fresh = ref 0
+
+let malformed s =
+   X.error ("anticipate: malformed term: " ^ s)
+
+let ok s =
+   X.log ("anticipate: ok " ^ s)
+
+let not_prop1 c u = match (K.whd c (K.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
+   P.sprintf "%s%u" !G.proc_id !fresh, w, v, C.Rel K.fst_var
+
+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
+      let s, w, v, tt = anticipate c t in
+      Some (i, s, w, v), (tt :: rtts)
+
+let lift_arg ri i tts t =
+   if ri = i then t :: tts
+   else K.lift K.fst_var 1 t :: tts
+
+let rec proc_term c t = match t with
+   | C.Appl []
+   | C.Meta _
+   | C.Implicit _             -> malformed "2"
+   | C.Sort _
+   | C.Rel _
+   | C.Const _
+   | C.Prod _                 -> [], t
+   | C.Lambda (s, w, t)       -> 
+      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
+         let dt, tt = proc_term (K.add_def s w v c) t in
+         dt @ K.add_def s w v [], tt
+      else
+         let dv, vv = proc_term c v in
+         let l = L.length dv in
+         let c = dv @ c in
+         let w = K.lift K.fst_var l w in
+         let t = K.lift K.snd_var l t in
+         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 ts                -> proc_appl c t ts
+   | C.Match (w, u, v, ts)    -> proc_case c t w u v ts
+
+and proc_appl c t ts = match X.foldi_left (proc_arg c) 1 initial ts with
+   | None             , _    -> [], t
+   | 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))
+
+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
+      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
+      proc_term c (K.letin s w0 v0 (K.case w u vv ts))
+   | Some (i, s, w0, v0), rtts ->
+      let ri = L.length rtts - i in
+      let u = K.lift K.fst_var 1 u in
+      let v = K.lift K.fst_var 1 v in
+      let tts = X.foldi_left (lift_arg ri) 0 [] rtts in
+      proc_term c (K.letin s w0 v0 (K.case w u v tts))
+
+and shift_term c t =
+   let d, tt = proc_term c t in
+   K.shift tt d
+
+let shift_named s c t =
+try
+   fresh := 0;
+   let tt = shift_term 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)
+   | Invalid_argument "List.nth" -> malformed "4" (* to be removed *)
+
+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
+
+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
+      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_obj obj = proc_obj obj
diff --git a/matita/components/binaries/matex/anticipate.mli b/matita/components/binaries/matex/anticipate.mli
new file mode 100644
index 000000000..e934bb462
--- /dev/null
+++ b/matita/components/binaries/matex/anticipate.mli
@@ -0,0 +1,18 @@
+(*
+    ||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 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 4f31b07a2..9b7ba8253 100644
--- a/matita/components/binaries/matex/engine.ml
+++ b/matita/components/binaries/matex/engine.ml
@@ -11,139 +11,179 @@
 
 module F = Filename
 module L = List
+module P = Printf
 module S = String
 
 module U = NUri
 module R = NReference
 module C = NCic
-module P = NCicPp
 module E = NCicEnvironment
+module V = NCicTypeChecker
 
+module X = Ground
 module G = Options
+module K = Kernel
 module T = TeX
 module O = TeXOutput
+module A = Anticipate
 
-let status = new P.status
+type status = {
+   n: string;   (* object name *)
+   s: int list; (* scope *)
+} 
 
 (* internal functions *******************************************************)
 
-let rec segments_of_string ss l s =
-   match try Some (S.index s '/') with Not_found -> None with
-      | None   -> s :: ss
-      | Some i -> segments_of_string (S.sub s 0 i :: ss) (l-i-1) (S.sub s (i+1) (l-i-1))
-
-let segments_of_uri u =
-   let s = U.string_of_uri u in
-   let s = F.chop_extension s in
-   let l = S.length s in
-   let i = S.index s ':' in
-   let s = S.sub s (i+2) (l-i-2) in
-   segments_of_string [] (l-i-2) s
-
-let rec mk_string sep r = function
-   | []      -> r 
-   | s :: ss -> mk_string sep (s ^ sep ^ r) ss 
-
 let alpha c s = s
 
 let malformed s =
-   failwith ("MaTeX: malformed term: " ^ s)
+   X.error ("engine: malformed term: " ^ s)
 
 let not_supported () =
-   failwith "MaTeX: object not supported"
+   X.error "engine: object not supported"
+
+(* generic term processing *)
 
 let proc_sort = function
-   | C.Prop             -> [T.Macro "Prop"]
-   | C.Type [`Type, u]  -> [T.Macro "Type"; T.arg (U.string_of_uri u)]
-   | C.Type [`CProp, u] -> [T.Macro "Crop"; T.arg (U.string_of_uri u)]
-   | C.Type _           -> malformed "1"
-
-let proc_gref ss = function
-   | C.Constant _             , R.Decl          ->
-      T.Macro "GRef" :: T.mk_segs ("type" :: ss)
-   | C.Constant _             , R.Def _         ->
-      T.Macro "GRef" :: T.mk_segs ("body" :: ss)
-   | C.Inductive (_, _, us, _), R.Ind (_, i, _) -> 
-      let _, name, _, _ = L.nth us i in
-      T.Macro "IRef" :: T.mk_segs (name :: ss)
-   | C.Inductive (_, _, us, _), R.Con (i, j, _) ->
-      let _, _, _, ts = L.nth us i in
-      let _, name, _ = L.nth ts (pred j) in
-      T.Macro "IRef" :: T.mk_segs (name :: ss)
-   | C.Fixpoint (_, ts, _)    , R.Fix (i, _, _) ->
-      let _, name, _, _, _ = L.nth ts i in
-      T.Macro "IRef" :: T.mk_segs (name :: ss)
-   | C.Fixpoint (_, ts, _)    , R.CoFix i       ->
-      let _, name, _, _, _ = L.nth ts i in
-      T.Macro "IRef" :: T.mk_segs (name :: ss)
-   | _                                          ->
-      malformed "2"
+   | C.Prop             -> [T.Macro "PROP"]
+   | C.Type [`Type, u]  -> [T.Macro "TYPE"; T.arg (U.string_of_uri u)]
+   | C.Type [`CProp, u] -> [T.Macro "CROP"; T.arg (U.string_of_uri u)]
+   | C.Type _           -> malformed "T1"
 
 let rec proc_term c = function
    | C.Appl []
    | C.Meta _
-   | C.Implicit _          -> malformed "3" 
-   | C.Rel m               ->
-      let name = L.nth c (m-1) in
-      [T.Macro "LRef"; T.arg name]
-   | C.Appl ts             ->
+   | C.Implicit _           -> malformed "T2" 
+   | C.Rel m                ->
+      let name = K.resolve_lref c m in
+      [T.Macro "LREF"; T.arg name; T.free name]
+   | C.Appl ts              ->
       let riss = L.rev_map (proc_term c) ts in
-      T.Macro "Appl" :: T.mk_rev_args riss
-  | C.Prod (s, w, t)       ->
+      T.Macro "APPL" :: T.mk_rev_args riss
+   | C.Prod (s, w, t)       ->
       let s = alpha c s in
       let is_w = proc_term c w in
-      let is_t = proc_term (s::c) t in
-      T.Macro "Prod" :: T.arg s :: T.Group is_w :: is_t
-  | C.Lambda (s, w, t)     -> 
+      let is_t = proc_term (K.add_dec s w c) t in
+      T.Macro "PROD" :: T.arg s :: T.Group is_w :: is_t
+   | C.Lambda (s, w, t)     -> 
       let s = alpha c s in
       let is_w = proc_term c w in
-      let is_t = proc_term (s::c) t in
-      T.Macro "Abst" :: T.arg s :: T.Group is_w :: is_t
-  | C.LetIn (s, w, v, t)   -> 
+      let is_t = proc_term (K.add_dec s w c) t in
+      T.Macro "ABST" :: T.arg s :: T.Group is_w :: is_t
+   | C.LetIn (s, w, v, t)   -> 
       let s = alpha c s in
       let is_w = proc_term c w in
       let is_v = proc_term c v in
-      let is_t = proc_term (s::c) t in
-      T.Macro "Abbr" :: T.arg s :: T.Group is_w :: T.Group is_v :: is_t
-  | C.Sort s               ->
+      let is_t = proc_term (K.add_def s w v c) t in
+      T.Macro "ABBR" :: T.arg s :: T.Group is_w :: T.Group is_v :: is_t
+   | C.Sort s               ->
       proc_sort s
-  | C.Const (R.Ref (u, r)) ->
-      let ss = segments_of_uri u in
-      let _, _, _, _, obj = E.get_checked_obj status u in  
-      proc_gref ss (obj, r)
-  | C.Match (w, u, v, ts)  ->
+   | 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_concat "." "type" ss)]
+   | C.Match (w, u, v, ts)  ->
       let is_w = proc_term c (C.Const w) in
       let is_u = proc_term c u in
       let is_v = proc_term c v in
       let riss = L.rev_map (proc_term c) ts in
-      T.Macro "Case" :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss
+      T.Macro "CASE" :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss
 
 let proc_term c t = try proc_term c t with
    | E.ObjectNotFound _ 
+   | Invalid_argument "List.nth"
    | Failure "nth" 
-   | Invalid_argument "List.nth" -> malformed "4"
+   | Failure "name_of_reference" -> malformed "T3"
+
+(* proof processing *)
+
+let init n = {
+   n = n; s = [];
+}
+
+let mk_dec w s is =
+   let w = if !G.no_types then [] else w in
+   T.Group w :: T.free s :: T.arg s :: T.Macro "DECL" :: is
+
+let rec proc_proof st ris c t = match t with
+   | C.Appl []
+   | C.Meta _
+   | C.Implicit _  
+   | C.Sort _
+   | C.Prod _              -> malformed "P1"
+   | C.Const _
+   | C.Rel _               -> proc_proof st ris c (C.Appl [t])
+   | C.Lambda (s, w, t)    -> 
+      let s = alpha c s in
+      let is_w = proc_term c w in
+      proc_proof st (T.Macro "PRIM" :: mk_dec is_w s ris) (K.add_dec s w c) t
+   | C.Appl ts              ->
+      let rts = X.rev_neg_filter (A.not_prop2 c) [] ts in
+      let ris = T.Macro "STEP" :: ris in
+      let tts = L.rev_map (proc_term c) rts in
+      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 ris = T.Macro "DEST" :: ris in
+      let tts = L.rev_map (proc_term c) rts in
+      T.rev_mk_args tts ris
+   | C.LetIn (s, w, v, t)  -> 
+      let s = alpha c s in
+      let is_w = proc_term c w in
+      if A.not_prop1 c w then
+         let is_v = proc_term c v in
+         proc_proof st (T.Group is_v :: T.Macro "BODY" :: mk_dec is_w s ris) (K.add_def s w v c) t
+      else
+         let ris_v = proc_proof st ris c v in
+         proc_proof st (mk_dec is_w s ris_v) (K.add_def s w v c) t
+
+let proc_proof c t = try proc_proof (init "") [] c t with 
+   | E.ObjectNotFound _ 
+   | Invalid_argument "List.nth"
+   | Failure "nth" 
+   | Failure "name_of_reference" -> malformed "P2"
+   | V.TypeCheckerFailure s
+   | V.AssertFailure s           -> malformed (Lazy.force s)
+
+(* top level processing *)
+
+let proc_top_type s t = 
+   [T.Macro "Object"; T.arg s; T.free s; T.Group (proc_term [] t)]
+
+let proc_top_body s t = proc_term [] t
+
+let proc_top_proof s t =
+   let tt = A.process_top_term s t in (* anticipation *)
+   L.rev (proc_proof [] tt)
 
 let open_out_tex s =
    open_out (F.concat !G.out_dir (s ^ T.file_ext))
 
-let proc_obj u =
-   let ss = segments_of_uri u in
-   let _, _, _, _, obj = E.get_checked_obj status u in 
-   match obj with
-      | C.Constant (_, _, None, u, _)   -> not_supported ()
-      | C.Constant (_, _, Some t, u, _) ->
-         let name = mk_string "." "body" ss in
-         let och = open_out_tex name in
-         O.out_text och (proc_term [] t);
-         O.out_text och T.newline;
-         close_out och;
-         let name = mk_string "." "type" ss in
+let proc_pair s ss u xt =
+   let name = X.rev_concat "." "type" ss in
+   let och = open_out_tex name in
+   O.out_text och (proc_top_type s u);
+   close_out och;
+   match xt with
+      | None   -> ()
+      | Some t ->
+         let name = X.rev_concat "." "body" ss in
          let och = open_out_tex name in
-         O.out_text och (proc_term [] u);
-         O.out_text och T.newline;
+         let text = if A.not_prop1 [] u then proc_top_body else proc_top_proof in
+         O.out_text och (text s t);
          close_out och
-      | C.Fixpoint (_, _, _)            -> not_supported ()
-      | C.Inductive (_, _, _, _)        -> not_supported ()
+
+let proc_fun ss (r, s, i, u, t) =
+   proc_pair s (s :: ss) u (Some t)
+
+let proc_obj u =
+   let ss = K.segments_of_uri u in
+   let _, _, _, _, obj = E.get_checked_obj G.status u in 
+   match obj with 
+      | C.Constant (_, s, xt, u, _) -> proc_pair s ss u xt
+      | C.Fixpoint (_, fs, _)       -> L.iter (proc_fun ss) fs
+      | C.Inductive (_, _, _, _)    -> not_supported ()
 
 (* interface functions ******************************************************)
 
diff --git a/matita/components/binaries/matex/ground.ml b/matita/components/binaries/matex/ground.ml
new file mode 100644
index 000000000..022ab63f2
--- /dev/null
+++ b/matita/components/binaries/matex/ground.ml
@@ -0,0 +1,53 @@
+(*
+    ||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 = String
+
+exception Error of string
+
+(* interface functions ******************************************************)
+
+let rec segments_of_string ss l s =
+   match try Some (S.index s '/') with Not_found -> None with
+      | None   -> s :: ss
+      | Some i -> segments_of_string (S.sub s 0 i :: ss) (l-i-1) (S.sub s (i+1) (l-i-1))
+
+let rec rev_concat sep r = function
+   | []                  -> r 
+   | s :: ss             ->
+      if r = "" then rev_concat sep s ss else
+      rev_concat sep (s ^ sep ^ r) ss 
+
+let fold_string map a s =
+   let l = S.length s in
+   let rec aux i a =
+      if i >= l then a else aux (succ i) (map a s.[i])
+   in
+   aux 0 a
+
+let rec rev_neg_filter filter r = function
+   | []       -> r
+   | hd :: tl ->
+      if filter hd then rev_neg_filter filter r tl else rev_neg_filter filter (hd :: r) tl
+
+let rec foldi_left mapi i a = function
+   | []       -> a
+   | hd :: tl -> foldi_left mapi (succ i) (mapi i a hd) tl
+
+let rec rev_map_append map l r = match l with
+   | []       -> r
+   | hd :: tl -> rev_map_append map tl (map hd :: r)
+
+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
new file mode 100644
index 000000000..e9892a7e0
--- /dev/null
+++ b/matita/components/binaries/matex/ground.mli
@@ -0,0 +1,28 @@
+(*
+    ||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_______________________________________________________________ *)
+
+exception Error of string
+
+val error: string -> 'a
+
+val log: string -> unit
+
+val segments_of_string: string list -> int -> string -> string list
+
+val rev_concat: string -> string -> string list -> string
+
+val fold_string: ('a -> char -> 'a) -> 'a -> string -> 'a
+
+val rev_neg_filter : ('a -> bool) -> 'a list -> 'a list -> 'a list
+
+val foldi_left: (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a 
+
+val rev_map_append: ('a -> 'b) -> 'a list -> 'b list -> 'b list
diff --git a/matita/components/binaries/matex/kernel.ml b/matita/components/binaries/matex/kernel.ml
new file mode 100644
index 000000000..f9ed0c466
--- /dev/null
+++ b/matita/components/binaries/matex/kernel.ml
@@ -0,0 +1,123 @@
+(*
+    ||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 F = Filename
+module P = Printf
+module S = String
+
+module U = NUri
+module C = NCic
+module B = NCicSubstitution
+module D = NCicReduction
+module K = NCicTypeChecker
+module H = HLog
+module A = NCicLibrary
+module E = NCicEnvironment
+module R = NReference
+
+module X = Ground
+module G = Options
+
+(* internal functions *******************************************************)
+
+let trusted _ = true
+
+let no_log _ _ = ()
+
+let mk_type_universe i =
+   [`Type, U.uri_of_string (P.sprintf "cic:/matita/pts/Type%s.univ" i)]
+
+(* interface functions ******************************************************)
+
+let init () =
+   A.init (); 
+   K.set_trust trusted;
+   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
+
+let fst_var = 1
+
+let snd_var = 2
+
+let lambda s w t = C.Lambda (s, w, t)
+
+let letin s w v t = C.LetIn (s, w, v, t)
+
+let case w u v ts = C.Match (w, u, v, ts)
+
+let add_dec s w c = (s, C.Decl w) :: c
+
+let add_def s w v c = (s, C.Def (v, w)) :: c
+
+let rec shift t = function
+   | []                     -> t
+   | (s, C.Decl w) :: c     -> shift (lambda s w t) c
+   | (s, C.Def (v, w)) :: c -> shift (letin s w v t) c
+
+let rec is_atomic = function
+   | C.Appl [t]   -> is_atomic t
+   | C.Appl []
+   | C.Meta _
+   | C.Implicit _ 
+   | C.Sort _
+   | C.Rel _
+   | C.Const _    -> true
+   | C.Appl _
+   | C.Prod _
+   | C.Lambda _ 
+   | C.LetIn _
+   | C.Match _    -> false
+
+let resolve_lref c i = fst (L.nth c (i - fst_var))
+
+let lift d e t =
+   B.lift G.status ~from:d e t
+
+let lifts d e ts =
+    L.rev_map (lift d e) (L.rev ts)
+
+let whd c t =
+   D.whd G.status ~delta:max_int ~subst:[] c t
+
+let typeof c t =
+   K.typeof G.status [] [] c t
+
+let segments_of_uri u =
+   let s = U.string_of_uri u in
+   let s = F.chop_extension s in
+   let l = S.length s in
+   let i = S.index s ':' in
+   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
+   | C.Constant (_, name, _, _, _), R.Decl      ->
+      ss, name
+   | C.Constant (_, name, _, _, _), R.Def _     ->
+      ss, name
+   | C.Inductive (_, _, us, _), R.Ind (_, i, _) -> 
+      let _, name, _, _ = L.nth us i in
+      (name :: ss), name
+   | C.Inductive (_, _, us, _), R.Con (i, j, _) ->
+      let _, _, _, ts = L.nth us i in
+      let _, name, _ = L.nth ts (pred j) in
+      (name :: ss), name
+   | C.Fixpoint (_, ts, _)    , R.Fix (i, _, _) ->
+      let _, name, _, _, _ = L.nth ts i in
+      (name :: ss), name
+   | C.Fixpoint (_, ts, _)    , R.CoFix i       ->
+      let _, name, _, _, _ = L.nth ts i in
+      (name :: ss), name
+   | _                                          ->
+      failwith "name_of_reference"
diff --git a/matita/components/binaries/matex/matex.ml b/matita/components/binaries/matex/matex.ml
index db1785c79..59460ce4a 100644
--- a/matita/components/binaries/matex/matex.ml
+++ b/matita/components/binaries/matex/matex.ml
@@ -15,31 +15,26 @@ module F = Filename
 module U = NUri
 module R = Helm_registry
 module L = Librarian
-module B = NCicLibrary
-module C = NCicTypeChecker
-module H = HLog
 
+module X = Ground
 module G = Options
 module E = Engine
 module O = TeXOutput
+module K = Kernel
 
 let help_O = "<dir> Set this output directory"
 let help_X = " Clear configuration and options"
+let help_p = " omit types (default: no)"
+let help_t = " Test anticipation (default: no)"
 
 let help   = ""
 
 (* internal functions *******************************************************)
 
-let trusted _ = true
-
-let no_log _ _ = ()
-
 let init registry =
    R.load_from registry; 
    if !G.no_init then begin
-      B.init (); 
-      C.set_trust trusted;
-      H.set_log_callback no_log;
+      K.init ();
       G.no_init := false;
    end
 
@@ -47,10 +42,10 @@ let is_registry s =
    F.check_suffix s ".conf.xml"
 
 let no_init () =
-   failwith "MaTeX: registry not initialized" 
+   failwith "MaTeX: main: registry not initialized" 
 
 let malformed s =
-   failwith ("MaTeX: malformed argument: " ^ s)
+   failwith ("MaTeX: main: malformed argument: " ^ s)
 
 let process s =
    if is_registry s then init s
@@ -59,7 +54,12 @@ let process s =
    else malformed s
 
 let main =
+try
    A.parse [
       "-O", A.String ((:=) G.out_dir), help_O;
       "-X", A.Unit G.clear, help_X;
+      "-p", A.Set G.no_types, help_p;
+      "-t", A.Set G.test, help_t;
    ] process help
+with
+   | X.Error s -> X.log s
diff --git a/matita/components/binaries/matex/options.ml b/matita/components/binaries/matex/options.ml
index dc094441e..14dc4e2c9 100644
--- a/matita/components/binaries/matex/options.ml
+++ b/matita/components/binaries/matex/options.ml
@@ -11,7 +11,8 @@
 
 module F = Filename
 
-module R  = Helm_registry
+module R = Helm_registry
+module P = NCicPp
 
 (* internal *****************************************************************)
 
@@ -19,13 +20,30 @@ let default_no_init = true
 
 let default_out_dir = F.current_dir_name
 
+let default_proc_id = "H"
+
+let default_test = false
+
+let default_no_types = false
+
 (* interface ****************************************************************)
 
+let status = new P.status
+
 let no_init = ref default_no_init
 
-let out_dir = ref default_out_dir
+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 clear () =
    R.clear ();
    no_init := default_no_init;
-   out_dir := default_out_dir
+   out_dir := default_out_dir;
+   proc_id := default_proc_id;
+   test := default_test;
+   no_types := default_no_types
diff --git a/matita/components/binaries/matex/options.mli b/matita/components/binaries/matex/options.mli
index 3cd2afa74..2c0e9b9b6 100644
--- a/matita/components/binaries/matex/options.mli
+++ b/matita/components/binaries/matex/options.mli
@@ -9,8 +9,16 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
+val status: NCicPp.status
+
 val no_init: bool ref
 
 val out_dir: string ref
 
+val proc_id: string ref
+
+val test: bool ref 
+
+val no_types: bool ref 
+
 val clear: unit -> unit
diff --git a/matita/components/binaries/matex/test/Make b/matita/components/binaries/matex/test/Make
new file mode 100644
index 000000000..e69de29bb
diff --git a/matita/components/binaries/matex/test/Makefile b/matita/components/binaries/matex/test/Makefile
new file mode 100644
index 000000000..b19199965
--- /dev/null
+++ b/matita/components/binaries/matex/test/Makefile
@@ -0,0 +1,38 @@
+LATEX  = latex
+DVIPS  = dvips
+BIBTEX = bibtex
+PSPDF  = ps2pdf -dEmbedAllFonts=true -dPDFSETTINGS=/prepress
+UNLOG  = ./unlog.pl
+
+MAIN = test
+
+SOURCES = $(shell cat Make)
+
+all: $(MAIN).dvi 
+
+ps: $(MAIN).ps
+
+pdf: $(MAIN).pdf
+
+tar: $(MAIN).tar
+
+again:
+	$(MAKE) --no-print-directory -B
+
+clean:
+	$(RM) *.log *.dvi *.aux *.spl *.ps *.blg *.pdf *.tar *~
+
+bibtex: $(MAIN).log
+	$(BIBTEX) $(MAIN)
+
+$(MAIN).dvi $(MAIN).log $(MAIN).aux: $(MAIN).tex $(SOURCES)
+	$(LATEX) $<
+
+$(MAIN).ps: $(MAIN).dvi 
+	$(DVIPS) $<
+
+$(MAIN).pdf: $(MAIN).ps
+	$(PSPDF) $<
+
+$(MAIN).tar: $(MAIN).log
+	$(UNLOG) $< $@
diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty
index 195789fe3..50338f5df 100644
--- a/matita/components/binaries/matex/test/matex.sty
+++ b/matita/components/binaries/matex/test/matex.sty
@@ -1,16 +1,37 @@
-\newcommand*\Skip[1]{}
-\newcommand*\Next[2]{\def\TMP{#2}\ifx\TMP\empty\let\next=\Skip\else #1{#2}\let\next=\Next\fi\next #1}
-
-\newcommand*\Visit[1]{ #1}
-
-\newcommand*\Prop{PROP}
-\newcommand*\Crop[1]{CROP}
-\newcommand*\Type[1]{TYPE}
-\newcommand*\LRef[1]{(L #1)}
-\newcommand*\GRef[2]{(G #2)\Next\Skip}
-\newcommand*\IRef[1]{(J #1)\Next\Skip}
-\newcommand*\Abbr[3]{(D #1 #2 #3) }
-\newcommand*\Abst[2]{(I #1 #2) }
-\newcommand*\Prod[2]{(P #1 #2) }
-\newcommand*\Appl{(A)\Next\Visit}
-\newcommand*\Case[3]{(C #1 #2 #3)\Next\Visit}
+\makeatletter
+
+\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}
+
+\newtheorem{prop}{Proposition}
+
+\newcommand*\ObjLabel[1]{\label{obj:#1}}
+\newcommand*\ObjRef[1]{\ref{obj:#1}}
+
+\newcommand*\Object[3]{\begin{prop}[#1]\hfil\\\setlabel{#1}\ObjLabel{#2}#3\end{prop}}
+
+\newcommand*\@skip[2]{}
+\newcommand*\Next[3]{\def\@tmp{#3}\ifx\@tmp\empty #2\let\next=\@skip\else #1{#3}\let\next=\Next\fi\next #1#2}
+
+\newcommand*\@proc[1]{ #1}
+
+\newcommand*\PROP{PROP}
+\newcommand*\CROP[1]{CROP}
+\newcommand*\TYPE[1]{TYPE}
+\newcommand*\LREF[2]{#1}
+\newcommand*\GREF[2]{#1}
+\newcommand*\ABBR[3]{(D #1 #2 #3) }
+\newcommand*\ABST[2]{(I #1 #2) }
+\newcommand*\PROD[2]{(P #1 #2) }
+\newcommand*\APPL{(A)\Next\@proc\relax}
+\newcommand*\CASE[3]{(C #1 #2 #3)\Next\@proc\relax}
+
+\def\@arg#1{, #1}
+\def\@stop{.\vskip10pt}
+
+\newcommand*\DECL[3]{\textbf{#1} : #3\vskip10pt}
+\newcommand*\PRIM{}
+\newcommand*\BODY[1]{is #1\vskip10pt}
+\newcommand*\STEP[1]{by #1\Next\@arg\@stop}
+\newcommand*\DEST[1]{by cases on #1\Next\@arg\@stop}
+
+\makeatother
diff --git a/matita/components/binaries/matex/test/test.tex b/matita/components/binaries/matex/test/test.tex
index ddf18c408..e30233190 100644
--- a/matita/components/binaries/matex/test/test.tex
+++ b/matita/components/binaries/matex/test/test.tex
@@ -1,13 +1,26 @@
 \documentclass{article}
 
+\usepackage[bookmarks=false,ps2pdf]{hyperref}
+\usepackage[american]{babel}
 \usepackage{matex}
 
 \begin{document}
 
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.type.tex}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.body.tex}
+
+\bigskip
+
 \input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.type}
 
-% \bigskip
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.body}
 
-% \input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.body}
+\ObjRef{pr0_ind}
+\ObjRef{pr0_confluence}
 
 \end{document}