X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=bff721a3e7b5a247e9bca1e0f442b9202ee31a53;hb=579d312fed0670e7528e106d2df94d72a18ee277;hp=7fd8290ba224783c9856a4cb84a1e2576749c90e;hpb=c465c17581bf606e0330cbd89b238279c184ad35;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 7fd8290ba..bff721a3e 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -26,6 +26,7 @@
 module C    = Cic
 module I    = CicInspect
 module D    = Deannotate
+module S    = CicSubstitution
 module TC   = CicTypeChecker 
 module Un   = CicUniv
 module UM   = UriManager
@@ -35,7 +36,6 @@ module A    = Cic2acic
 module Ut   = CicUtil
 module E    = CicEnvironment
 module PEH  = ProofEngineHelpers
-module PER  = ProofEngineReduction
 module Pp   = CicPp
 
 module Cl   = ProceduralClassify
@@ -155,20 +155,50 @@ try
    ty
 with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
 
+let get_entry st id =
+   let rec aux = function
+      | []                                        -> assert false
+      | Some (C.Name name, e) :: _ when name = id -> e
+      | _ :: tl                                   -> aux tl
+   in
+   aux st.context
+   
 (* proof construction *******************************************************)
 
 let unused_premise = "UNUSED"
 
+let mk_exp_args hd tl classes =
+   let meta id = C.AImplicit (id, None) in
+   let map v (cl, b) =
+      if I.S.mem 0 cl && b then v else meta ""
+   in
+   let rec aux = function
+      | [] -> []
+      | hd :: tl -> if hd = meta "" then aux tl else List.rev (hd :: tl)
+   in
+   let args = List.rev_map2 map tl classes in
+   let args = aux args in
+   if args = [] then hd else C.AAppl ("", hd :: args)
+
 let convert st ?name v = 
    match get_inner_types st v with
-      | None          -> []
-      | Some (st, et) ->
-         let cst, cet = cic st, cic et in
-	 if PER.alpha_equivalence cst cet then [] else 
+      | None            -> []
+      | Some (sty, ety) ->
 	 let e = Cn.mk_pattern 0 (T.mk_arel 1 "") in
+         let csty, cety = cic sty, cic ety in
+	 if Ut.alpha_equivalence csty cety then [] else 
 	 match name with
-	    | None    -> [T.Change (st, et, None, e, "")]
-	    | Some id -> [T.Change (st, et, Some (id, id), e, ""); T.ClearBody (id, "")]
+	    | None         -> [T.Change (sty, ety, None, e, "")]
+	    | Some (id, i) -> 
+               begin match get_entry st id with
+	          | C.Def _  -> [T.ClearBody (id, "")]
+	          | C.Decl w -> 
+	             let w = S.lift i w in
+		     if Ut.alpha_equivalence csty w then [] 
+		     else 
+		     [T.Note (Pp.ppterm csty); T.Note (Pp.ppterm w);
+		     T.Change (sty, ety, Some (id, id), e, "")] 
+	       end
 
 let get_intro = function 
    | C.Anonymous -> unused_premise
@@ -180,7 +210,7 @@ let mk_intros st script =
    T.Intros (Some count, List.rev st.intros, "") :: script
 
 let mk_arg st = function
-   | C.ARel (_, _, _, name) as what -> convert st ~name what
+   | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what
    | _                              -> []
 
 let mk_fwd_rewrite st dtext name tl direction =   
@@ -220,7 +250,7 @@ and proc_letin st what name v t =
 	          let qs = [[T.Id ""]; proc_proof (next st) v] in
 	          [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
 	    in
-	    C.Decl (get_type "TC1" st v), rqv
+	    C.Decl (cic ity), rqv
 	 | None          ->
 	    C.Def (cic v, None), [T.LetIn (intro, v, dtext)]
       in
@@ -272,6 +302,7 @@ and proc_appl st what hd tl =
 	       [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
 	 | None        ->
 	    let qs = proc_bkd_proofs (next st) synth classes tl in
+	    let hd = mk_exp_args hd tl classes in
 	    script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
    else
       [T.Apply (what, dtext)]