X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=9815580b6444ef8bb31669e0fd60aaae5cebb60b;hb=797f61edb93f41eb2c5e281bc9457f6bff633063;hp=3ee088696db48a6bc58eb67372214132f5df906c;hpb=2921483dad22e14c2e697cbe5597a0b32af04090;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 3ee088696..9815580b6 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -191,26 +191,38 @@ let mk_exp_args hd tl classes synth =
    let args = aux args in
    if args = [] then hd else C.AAppl ("", hd :: args)
 
+let mk_convert st ?name sty ety note =
+   let e = Cn.hole "" in
+   let csty, cety = H.cic sty, H.cic ety in
+   let _note = Printf.sprintf "%s\nSINTH: %s\nEXP: %s"
+      note (Pp.ppterm csty) (Pp.ppterm cety)
+   in
+   if Ut.alpha_equivalence csty cety then [(* T.Note note *)] else 
+   match name with
+      | None         -> [T.Change (sty, ety, None, e, ""(*note*))]
+      | Some (id, i) -> 
+         begin match get_entry st id with
+	    | C.Def _  -> assert false (* [T.ClearBody (id, note)] *)
+	    | C.Decl _ -> [T.Change (ety, sty, Some (id, Some id), e, "" (* note *))] 
+         end
+
 let convert st ?name v = 
    match get_inner_types st v with
-      | None            -> []
-      | Some (sty, ety) ->
-	 let e = Cn.hole "" in
-         let csty, cety = H.cic sty, H.cic ety in
-	 if Ut.alpha_equivalence csty cety then [] else 
-	 match name with
-	    | 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, Some id), e, "")] 
-	       end
-
+      | None            -> [(*T.Note "NORMAL: NO INNER TYPES"*)]
+      | Some (sty, ety) -> mk_convert st ?name sty ety "NORMAL"
+
+let convert_elim st ?name t v pattern =
+   match t, get_inner_types st t, get_inner_types st v with
+      | _, None, _
+      | _, _, None                                            -> [(* T.Note "ELIM: NO INNER TYPES"*)]
+      | C.AAppl (_, hd :: tl), Some (tsty, _), Some (vsty, _) ->
+         let where = List.hd (List.rev tl) in
+         let cty = Cn.elim_inferred_type 
+	     st.context (H.cic vsty) (H.cic where) (H.cic hd) (H.cic pattern)
+	 in
+         mk_convert st ?name (Cn.fake_annotate "" st.context cty) tsty "ELIM"
+      | _, Some _, Some _                                     -> assert false
+	  
 let get_intro = function 
    | C.Anonymous -> None
    | C.Name s    -> Some s
@@ -230,23 +242,25 @@ let mk_arg st = function
    | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what
    | _                              -> []
 
-let mk_fwd_rewrite st dtext name tl direction =   
+let mk_fwd_rewrite st dtext name tl direction t =   
    assert (List.length tl = 6);
    let what, where, predicate = List.nth tl 5, List.nth tl 3, List.nth tl 2 in
    let e = Cn.mk_pattern 1 predicate in
    match where with
-      | C.ARel (_, _, _, premise) ->
-         let script = mk_arg st what in
+      | C.ARel (_, _, i, premise) as v ->
          let where = Some (premise, name) in
+         let _script = convert_elim st ~name:(premise, i) t v e in 
+         let script = mk_arg st what @ mk_arg st v (* @ script *) in
 	 let st = {st with context = Cn.clear st.context premise} in 
 	 st, T.Rewrite (direction, what, where, e, dtext) :: script
       | _                         -> assert false
 
-let mk_rewrite st dtext what qs tl direction = 
+let mk_rewrite st dtext where qs tl direction t = 
    assert (List.length tl = 5);
    let predicate = List.nth tl 2 in
    let e = Cn.mk_pattern 1 predicate in
-   [T.Rewrite (direction, what, None, e, dtext); T.Branch (qs, "")]
+   let script = convert_elim st t t e in
+   script @ [T.Rewrite (direction, where, None, e, dtext); T.Branch (qs, "")]
 
 let rec proc_lambda st name v t =
    let dno = DTI.does_not_occur 1 (H.cic t) in
@@ -272,9 +286,9 @@ and proc_letin st what name v t =
          | Some (ity, _) ->
 	    let st, rqv = match v with
                | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right hd tl ->
-	          mk_fwd_rewrite st dtext intro tl true
+	          mk_fwd_rewrite st dtext intro tl true v
 	       | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl  ->
-	          mk_fwd_rewrite st dtext intro tl false
+	          mk_fwd_rewrite st dtext intro tl false v
 	       | v                                                     ->
 	          let qs = [proc_proof (next st) v; [T.Id ""]] in
 	          st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
@@ -300,7 +314,7 @@ and proc_rel st what =
 and proc_mutconstruct st what = 
    let _, dtext = test_depth st in
    let script = [T.Apply (what, dtext)] in 
-   mk_intros st what script   
+   mk_intros st what script
 
 and proc_appl st what hd tl =
    let proceed, dtext = test_depth st in
@@ -329,14 +343,14 @@ and proc_appl st what hd tl =
 	    let names = get_ind_names uri tyno in
 	    let qs = proc_bkd_proofs (next st) synth names classes tl in
             if is_rewrite_right hd then 
-	       script @ mk_rewrite st dtext where qs tl false
+	       script @ mk_rewrite st dtext where qs tl false what
 	    else if is_rewrite_left hd then 
-	       script @ mk_rewrite st dtext where qs tl true
+	       script @ mk_rewrite st dtext where qs tl true what
 	    else
 	       let predicate = List.nth tl (parsno - i) in
                let e = Cn.mk_pattern j predicate in
 	       let using = Some hd in
-	       script @
+	       convert_elim st what what e @ script @ 
 	       [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
 	 | None        ->
 	    let qs = proc_bkd_proofs (next st) synth [] classes tl in