alpha equivalence test factorized and moved to CicUtil

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

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index 08727be1cfde78d6c773dcc76177ff679351dbcd..fb99090e98b76df165c3cbd8244ee17fb70c1601 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/components/acic_procedural/acic2Procedural.ml
@@ -35,7 +35,6 @@ module A    = Cic2acic
 module Ut   = CicUtil
 module E    = CicEnvironment
 module PEH  = ProofEngineHelpers
-module PER  = ProofEngineReduction
 module Pp   = CicPp
 
 module Cl   = ProceduralClassify
@@ -155,6 +154,14 @@ try
    ty
 with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
 
+let get_entry st id =
+   let rec aux = function
+      | []                                        -> assert false
+      | Some (C.Name name, e) :: _ when name = id -> e
+      | _ :: tl                                   -> aux tl
+   in
+   aux st.context
+   
 (* proof construction *******************************************************)
 
 let unused_premise = "UNUSED"
@@ -174,14 +181,20 @@ let mk_exp_args hd tl classes =
 
 let convert st ?name v = 
    match get_inner_types st v with
-      | None          -> []
-      | Some (st, et) ->
-         let cst, cet = cic st, cic et in
-        if PER.alpha_equivalence cst cet then [] else 
+      | None            -> []
+      | Some (sty, ety) ->
+         let csty, cety = cic sty, cic ety in
+        if Ut.alpha_equivalence csty cety then [] else 
         let e = Cn.mk_pattern 0 (T.mk_arel 1 "") in
         match name with
-           | None    -> [T.Change (st, et, None, e, "")]
-           | Some id -> [T.Change (st, et, Some (id, id), e, ""); T.ClearBody (id, "")]
+           | None    -> [T.Change (sty, ety, None, e, "")]
+           | Some id -> 
+               begin match get_entry st id with
+                 | C.Def _  -> [T.ClearBody (id, "")]
+                 | C.Decl w -> 
+                    if Ut.alpha_equivalence csty w then [] 
+                    else [T.Change (sty, ety, Some (id, id), e, "")] 
+              end
 
 let get_intro = function 
    | C.Anonymous -> unused_premise
@@ -193,7 +206,7 @@ let mk_intros st script =
    T.Intros (Some count, List.rev st.intros, "") :: script
 
 let mk_arg st = function
-   | C.ARel (_, _, _, name) as what -> [] (* convert st ~name what *)
+   | C.ARel (_, _, _, name) as what -> convert st ~name what
    | _                              -> []
 
 let mk_fwd_rewrite st dtext name tl direction =   
@@ -233,7 +246,7 @@ and proc_letin st what name v t =
                  let qs = [[T.Id ""]; proc_proof (next st) v] in
                  [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
            in
-           C.Decl (get_type "TC1" st v), rqv
+           C.Decl (cic ity), rqv
         | None          ->
            C.Def (cic v, None), [T.LetIn (intro, v, dtext)]
       in