X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=b37eef6bbc989034b8dbe2e7fd851dc454baf943;hb=3b8d99d5fdb79a5d979a8e200a4a4307fe362009;hp=b4f6053c04e493f2dcd5271ee74ebf0f3589e0c9;hpb=fdeb64c7f9e870d43a4eb87153bf72e6f5705f01;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index b4f6053c0..b37eef6bb 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -153,7 +153,7 @@ with Invalid_argument _ -> failwith "A2P.get_sort"
 *)
 let get_type msg st bo =
 try   
-   let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.empty_ugraph in
+   let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.oblivion_ugraph in
    ty
 with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
 
@@ -167,7 +167,7 @@ let get_entry st id =
 
 let get_ind_names uri tno =
 try   
-   let ts = match E.get_obj Un.empty_ugraph uri with
+   let ts = match E.get_obj Un.oblivion_ugraph uri with
       | C.InductiveDefinition (ts, _, _, _), _ -> ts 
       | _                                      -> assert false
    in
@@ -282,7 +282,7 @@ let rec proc_lambda st name v t =
    let intro = get_intro name in
    proc_proof (add st entry intro) t
 
-and proc_letin st what name v t =
+and proc_letin st what name v w t =
    let intro = get_intro name in
    let proceed, dtext = test_depth st in
    let script = if proceed then 
@@ -300,7 +300,7 @@ and proc_letin st what name v t =
 	    in
 	    st, C.Decl (H.cic ity), rqv
 	 | None          ->
-	    st, C.Def (H.cic v, None), [T.LetIn (intro, v, dtext)]
+	    st, C.Def (H.cic v, H.cic w), [T.LetIn (intro, v, dtext)]
       in
       let entry = Some (name, hyp) in
       let qt = proc_proof (next (add st entry intro)) t in
@@ -321,6 +321,11 @@ and proc_mutconstruct st what =
    let script = [T.Apply (what, dtext)] in 
    mk_intros st what script
 
+and proc_const st what = 
+   let _, dtext = test_depth st in
+   let script = [T.Apply (what, dtext)] in 
+   mk_intros st what script
+
 and proc_appl st what hd tl =
    let proceed, dtext = test_depth st in
    let script = if proceed then
@@ -342,20 +347,24 @@ and proc_appl st what hd tl =
       let script = List.rev (mk_arg st hd) in
       match rc with
          | Some (i, j, uri, tyno) ->
-	    let classes, tl, _, where = split2_last classes tl in
-	    let script = List.rev (mk_arg st where) @ script in
-	    let synth = I.S.add 1 synth in
+	    let classes2, tl2, _, where = split2_last classes tl in
+	    let script2 = List.rev (mk_arg st where) @ script in
+	    let synth2 = I.S.add 1 synth in
 	    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 what
+	    let qs = proc_bkd_proofs (next st) synth2 names classes2 tl2 in
+            if List.length qs <> List.length names then
+	       let qs = proc_bkd_proofs (next st) synth [] classes tl in
+	       let hd = mk_exp_args hd tl classes synth in
+	       script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
+	    else if is_rewrite_right hd then 
+	       script2 @ mk_rewrite st dtext where qs tl2 false what
 	    else if is_rewrite_left hd then 
-	       script @ mk_rewrite st dtext where qs tl true what
+	       script2 @ mk_rewrite st dtext where qs tl2 true what
 	    else
-	       let predicate = List.nth tl (parsno - i) in
+	       let predicate = List.nth tl2 (parsno - i) in
                let e = Cn.mk_pattern j predicate in
 	       let using = Some hd in
-	       (* convert_elim st what what e @ *) script @ 
+	       (* convert_elim st what what e @ *) script2 @ 
 	       [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
 	 | None        ->
 	    let qs = proc_bkd_proofs (next st) synth [] classes tl in
@@ -384,12 +393,13 @@ and proc_proof st t =
       {st with context = context; clears = clears; clears_note = note; }
    in
    match t with
-      | C.ALambda (_, name, w, t)        -> proc_lambda st name w t
-      | C.ALetIn (_, name, v, t) as what -> proc_letin (f st) what name v t
-      | C.ARel _ as what                 -> proc_rel (f st) what
-      | C.AMutConstruct _ as what        -> proc_mutconstruct (f st) what
-      | C.AAppl (_, hd :: tl) as what    -> proc_appl (f st) what hd tl
-      | what                             -> proc_other (f st) what
+      | C.ALambda (_, name, w, t)           -> proc_lambda st name w t
+      | C.ALetIn (_, name, v, w, t) as what -> proc_letin (f st) what name v w t
+      | C.ARel _ as what                    -> proc_rel (f st) what
+      | C.AMutConstruct _ as what           -> proc_mutconstruct (f st) what
+      | C.AConst _ as what                  -> proc_const (f st) what
+      | C.AAppl (_, hd :: tl) as what       -> proc_appl (f st) what hd tl
+      | what                                -> proc_other (f st) what
 
 and proc_bkd_proofs st synth names classes ts =
 try 
@@ -418,7 +428,8 @@ with Invalid_argument s -> failwith ("A2P.proc_bkd_proofs: " ^ s)
 
 (* object costruction *******************************************************)
 
-let is_theorem pars =   
+let is_theorem pars =
+   pars = [] ||
    List.mem (`Flavour `Theorem) pars || List.mem (`Flavour `Fact) pars || 
    List.mem (`Flavour `Remark) pars || List.mem (`Flavour `Lemma) pars