- Procedural convertible rewrites in the conclusion are now detected and replaced...

[helm.git] / helm / software / components / acic_procedural / procedural2.ml

diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml
index 06fc9b35843bf330a0020cd836acd47d443e52aa..826cfb986d5e44f4672c04d46c1c055fee87471b 100644 (file)
--- a/helm/software/components/acic_procedural/procedural2.ml
+++ b/helm/software/components/acic_procedural/procedural2.ml
@@ -26,6 +26,7 @@
 module C    = Cic
 module I    = CicInspect
 module S    = CicSubstitution
+module R    = CicReduction
 module TC   = CicTypeChecker 
 module Un   = CicUniv
 module UM   = UriManager
@@ -57,7 +58,7 @@ type status = {
    case     : int list
 }
 
-let debug = ref true
+let debug = ref false
 
 (* helpers ******************************************************************)
 
@@ -186,6 +187,11 @@ let is_reflexivity st step =
       | None             -> false
       | Some (uri, i, j) -> st.defaults && Obj.is_eq_URI uri && i = 1 && j = 1
 
+let are_convertible st pred sx dx =
+   let pred, sx, dx = H.cic pred, H.cic sx, H.cic dx in
+   let sx, dx = C.Appl [pred; sx], C.Appl [pred; dx] in
+   fst (R.are_convertible st.context sx dx Un.default_ugraph)
+
 (* proof construction *******************************************************)
 
 let anonymous_premise = C.Name "UNNAMED"
@@ -227,7 +233,7 @@ let mk_convert st ?name sty ety note =
             note sname (ppterm csty) (ppterm cety)
       else ""
    in
-   if H.alpha_equivalence ~flatten:true st.context csty cety then [T.Note note] else 
+   if H.alpha ~flatten:true st.context csty cety then [T.Note note] else 
    let sty, ety = H.acic_bc st.context sty, H.acic_bc st.context ety in
    match name with
       | None         -> [T.Change (sty, ety, None, e, note)]
@@ -294,11 +300,18 @@ let mk_rewrite st dtext where qs tl direction t ity =
       let a = ref "" in Ut.pp_term (fun s -> a := !a ^ s) [] st.context t; !a
    in 
    assert (List.length tl = 5);
-   let predicate = List.nth tl 2 in
-   let dtext = if !debug then dtext ^ ppterm (H.cic predicate) else dtext in
-   let e = Cn.mk_pattern 1 ity predicate in
+   let pred, sx, dx = List.nth tl 2, List.nth tl 1, List.nth tl 4 in
+   let dtext = if !debug then dtext ^ ppterm (H.cic pred) else dtext in
+   let e = Cn.mk_pattern 1 ity pred in
    let script = [T.Branch (qs, "")] in
-   if (Cn.does_not_occur e) then script else
+   if Cn.does_not_occur e then script else
+   if are_convertible st pred sx dx then 
+      let dtext = "convertible rewrite" ^ dtext in
+      let ity, ety, e = Cn.beta sx pred, Cn.beta dx pred, Cn.hole "" in
+      let city, cety = H.cic ity, H.cic ety in
+      if H.alpha ~flatten:true st.context city cety then script else
+      T.Change (ity, ety, None, e, dtext) :: script
+   else
    T.Rewrite (direction, where, None, e, dtext) :: script
 
 let rec proc_lambda st what name v t =
@@ -319,8 +332,8 @@ and proc_letin st what name v w t =
    let script = if proceed then 
       let st, hyp, rqv = match get_inner_types st what, get_inner_types st v with
          | Some (C.ALetIn (_, _, iv, iw, _), _), _ when
-           H.alpha_equivalence ~flatten:true st.context (H.cic v) (H.cic iv) &&
-           H.alpha_equivalence ~flatten:true st.context (H.cic w) (H.cic iw)
+           H.alpha ~flatten:true st.context (H.cic v) (H.cic iv) &&
+           H.alpha ~flatten:true st.context (H.cic w) (H.cic iw)
                                                   ->
            st, C.Def (H.cic v, H.cic w), [T.Intros (Some 1, [intro], dtext)]
         | _, Some (ity, ety)                      ->