- new devel contribs/LAMBDA-TYPES/Base-2 with the automatically generated

[helm.git] / components / acic_procedural / acic2Procedural.ml

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index 3ee088696db48a6bc58eb67372214132f5df906c..9815580b6444ef8bb31669e0fd60aaae5cebb60b 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/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