alpha equivalence fixed: in the case "meta against meta" we did not recur on theexpli...

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

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 7fd8290ba224783c9856a4cb84a1e2576749c90e..bff721a3e7b5a247e9bca1e0f442b9202ee31a53 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -26,6 +26,7 @@
 module C    = Cic
 module I    = CicInspect
 module D    = Deannotate
+module S    = CicSubstitution
 module TC   = CicTypeChecker 
 module Un   = CicUniv
 module UM   = UriManager
@@ -35,7 +36,6 @@ module A    = Cic2acic
 module Ut   = CicUtil
 module E    = CicEnvironment
 module PEH  = ProofEngineHelpers
-module PER  = ProofEngineReduction
 module Pp   = CicPp
 
 module Cl   = ProceduralClassify
@@ -155,20 +155,50 @@ 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"
 
+let mk_exp_args hd tl classes =
+   let meta id = C.AImplicit (id, None) in
+   let map v (cl, b) =
+      if I.S.mem 0 cl && b then v else meta ""
+   in
+   let rec aux = function
+      | [] -> []
+      | hd :: tl -> if hd = meta "" then aux tl else List.rev (hd :: tl)
+   in
+   let args = List.rev_map2 map tl classes in
+   let args = aux args in
+   if args = [] then hd else C.AAppl ("", hd :: args)
+
 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 e = Cn.mk_pattern 0 (T.mk_arel 1 "") in
+         let csty, cety = cic sty, cic ety in
+        if Ut.alpha_equivalence csty cety then [] else 
         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, 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, id), e, "")] 
+              end
 
 let get_intro = function 
    | C.Anonymous -> unused_premise
@@ -180,7 +210,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 (_, _, i, name) as what -> convert st ~name:(name, i) what
    | _                              -> []
 
 let mk_fwd_rewrite st dtext name tl direction =   
@@ -220,7 +250,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
@@ -272,6 +302,7 @@ and proc_appl st what hd tl =
               [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
         | None        ->
            let qs = proc_bkd_proofs (next st) synth classes tl in
+           let hd = mk_exp_args hd tl classes in
            script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
    else
       [T.Apply (what, dtext)]