X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=f39aa18bd96ee3a162baa10fa6da07ca3b6f8805;hb=55ec3926f6fbb5dba13705659fe94d0db38b2666;hp=4ccb78ace32522efbd43d8b9706bbe7f81deca71;hpb=cf4301b669442bdd78984d3a3a1e38660db1f2ea;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 4ccb78ace..f39aa18bd 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -54,7 +54,8 @@ type status = {
    intros: string option list;
    clears: string list;
    clears_note: string;
-   case: int list
+   case: int list;
+   skip_thm_and_qed : bool;
 }
 
 (* helpers ******************************************************************)
@@ -191,62 +192,76 @@ 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
 
-let mk_intros st script =
+let mk_intros st what script =
    let intros st script =
       if st.intros = [] then script else
       let count = List.length st.intros in
       T.Intros (Some count, List.rev st.intros, "") :: script
    in
    let clears st script =
-      if st.clears = [] then script else T.Clear (st.clears, st.clears_note) :: script
+      if true (* st.clears = [] *) then script else T.Clear (st.clears, st.clears_note) :: script
    in
-   intros st (clears st script)   
+   intros st (clears st (convert st what @ script))   
 
 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 +287,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)]
@@ -289,18 +304,18 @@ and proc_letin st what name v t =
    else
       [T.Apply (what, dtext)]
    in
-   mk_intros st script
+   mk_intros st what script
 
 and proc_rel st what = 
    let _, dtext = test_depth st in
    let text = "assumption" in
    let script = [T.Apply (what, dtext ^ text)] in 
-   mk_intros st script
+   mk_intros st what script
 
 and proc_mutconstruct st what = 
    let _, dtext = test_depth st in
    let script = [T.Apply (what, dtext)] in 
-   mk_intros st script   
+   mk_intros st what script
 
 and proc_appl st what hd tl =
    let proceed, dtext = test_depth st in
@@ -320,7 +335,7 @@ and proc_appl st what hd tl =
       in
       let synth = mk_synth I.S.empty decurry in
       let text = "" (* Printf.sprintf "%u %s" parsno (Cl.to_string h) *) in
-      let script = List.rev (mk_arg st hd) @ convert st what in
+      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
@@ -329,14 +344,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
@@ -345,12 +360,12 @@ and proc_appl st what hd tl =
    else
       [T.Apply (what, dtext)]
    in
-   mk_intros st script
+   mk_intros st what script
 
 and proc_other st what =
    let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head what) in
    let script = [T.Note text] in
-   mk_intros st script
+   mk_intros st what script
 
 and proc_proof st t = 
    let f st =
@@ -362,7 +377,7 @@ and proc_proof st t =
       in
       let context, clears = Cn.get_clears st.context (H.cic t) xtypes in
       let note = Pp.ppcontext st.context ^ note in
-      {st with context = context; clears = clears; clears_note = note}
+      {st with context = context; clears = clears; clears_note = note; }
    in
    match t with
       | C.ALambda (_, name, w, t)        -> proc_lambda st name w t
@@ -408,13 +423,15 @@ let proc_obj st = function
       let ast = proc_proof st v in
       let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
       let text = Printf.sprintf "tactics: %u\nnodes: %u" steps nodes in
-      T.Theorem (Some s, t, "") :: ast @ [T.Qed text]
+      if st.skip_thm_and_qed then ast
+      else T.Theorem (Some s, t, "") :: ast @ [T.Qed text]
    | _                                                               ->
       failwith "not a theorem"
 
 (* interface functions ******************************************************)
 
-let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj = 
+let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth
+?(skip_thm_and_qed=false) prefix aobj = 
    let st = {
       sorts       = ids_to_inner_sorts;
       types       = ids_to_inner_types;
@@ -425,7 +442,8 @@ let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj =
       intros      = [];
       clears      = [];
       clears_note = "";
-      case        = []
+      case        = [];
+      skip_thm_and_qed = skip_thm_and_qed;
    } in
    HLog.debug "Procedural: level 2 transformation";
    let steps = proc_obj st aobj in