Procedural: clear tactics added

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

diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml
index 53898136940f369667b3625e126d5171690c61aa..b8cdc08ea1b3af2a0288ef6239f3718ad4aed5ea 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralConversion.ml
+++ b/helm/software/components/acic_procedural/proceduralConversion.ml
@@ -31,6 +31,8 @@ module D    = Deannotate
 module UM   = UriManager
 module Rd   = CicReduction
 
+module DTI  = DoubleTypeInference
+
 (* helpers ******************************************************************)
 
 let cic = D.deannotate_term
@@ -115,7 +117,7 @@ let generalize n =
       | C.AMutConstruct (id, _, _, _, _)
       | C.AMeta (id, _, _) -> meta id
       | C.ARel (id, _, m, _) -> 
-         if m = succ (k - n) then hole id else meta id
+         if succ (k - n) <= m && m <= k then hole id else meta id
       | C.AAppl (id, ts) -> 
          let ts = List.map (gen_term k) ts in
          if is_meta ts then meta id else C.AAppl (id, ts)
@@ -139,6 +141,58 @@ let generalize n =
    in
    gen_term 0
 
-let mk_pattern rpsno predicate =
-   let body = generalize rpsno predicate in
-   clear_absts 0 rpsno body
+let mk_pattern psno predicate =
+   let body = generalize psno predicate in
+   clear_absts 0 psno body
+
+let get_clears c p xtypes = 
+   let meta = C.Implicit None in
+   let rec aux c names p it et = function
+      | []                                                -> 
+         List.rev c, List.rev names         
+      | Some (C.Name name as n, C.Decl v) as hd :: tl     ->
+         let hd, names, v = 
+           if DTI.does_not_occur 1 p && DTI.does_not_occur 1 it && DTI.does_not_occur 1 et then 
+              Some (C.Anonymous, C.Decl v), name :: names, meta 
+           else 
+              hd, names, v
+        in
+        let p = C.Lambda (n, v, p) in
+        let it = C.Prod (n, v, it) in
+        let et = C.Prod (n, v, et) in
+        aux (hd :: c) names p it et tl
+      | Some (C.Name name as n, C.Def (v, x)) as hd :: tl ->
+         let hd, names, v = 
+           if DTI.does_not_occur 1 p && DTI.does_not_occur 1 it && DTI.does_not_occur 1 et then 
+              Some (C.Anonymous, C.Def (v, x)), name :: names, meta
+           else 
+              hd, names, v
+        in
+        let p = C.LetIn (n, v, p) in
+        let it = C.LetIn (n, v, it) in
+        let et = C.LetIn (n, v, et) in
+        aux (hd :: c) names p it et tl
+      | Some (C.Anonymous as n, C.Decl v) as hd :: tl     ->
+        let p = C.Lambda (n, meta, p) in
+        let it = C.Lambda (n, meta, it) in
+        let et = C.Lambda (n, meta, et) in
+        aux (hd :: c) names p it et tl
+      | Some (C.Anonymous as n, C.Def (v, _)) as hd :: tl ->
+        let p = C.LetIn (n, meta, p) in
+        let it = C.LetIn (n, meta, it) in
+        let et = C.LetIn (n, meta, et) in
+        aux (hd :: c) names p it et tl
+      | None :: tl                                        -> assert false
+   in
+   match xtypes with 
+      | Some (it, et) -> aux [] [] p it et c
+      | None          -> c, []
+
+let clear c hyp =
+   let rec aux c = function
+      | []            -> List.rev c
+      | Some (C.Name name, entry) :: tail when name = hyp ->
+        aux (Some (C.Anonymous, entry) :: c) tail
+      | entry :: tail -> aux (entry :: c) tail
+   in
+   aux [] c