PrimitiveTactics: intros _ now aveilable

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

diff --git a/components/acic_procedural/proceduralConversion.ml b/components/acic_procedural/proceduralConversion.ml
index 80aae9e7f3668b83fcee3378d7cb148174b5c31c..68b47341c05caff79f8972eb645c16c8fef30d73 100644 (file)
--- a/components/acic_procedural/proceduralConversion.ml
+++ b/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
@@ -142,3 +144,51 @@ let generalize n =
 let mk_pattern psno predicate =
    let body = generalize psno predicate in
    clear_absts 0 psno body
+
+let get_clears c p xet = 
+   let meta = C.Implicit None in
+   let rec aux c names p 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 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 et = C.Prod (n, v, et) in
+        aux (hd :: c) names p 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 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 et = C.LetIn (n, v, et) in
+        aux (hd :: c) names p et tl
+      | Some (C.Anonymous as n, C.Decl v) as hd :: tl     ->
+        let p = C.Lambda (n, meta, p) in
+        let et = C.Lambda (n, meta, et) in
+        aux (hd :: c) names p et tl
+      | Some (C.Anonymous as n, C.Def (v, _)) as hd :: tl ->
+        let p = C.LetIn (n, meta, p) in
+        let et = C.LetIn (n, meta, et) in
+        aux (hd :: c) names p et tl
+      | None :: tl                                        -> assert false
+   in
+   match xet with 
+      | Some et -> aux [] [] p 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