elim tactic: now takes a pattern instead of just a term

[helm.git] / components / tactics / proofEngineReduction.ml

diff --git a/components/tactics/proofEngineReduction.ml b/components/tactics/proofEngineReduction.ml
index 6d198d4d133e721539c30e77d86196787ff6c1b5..c359313dd1e87e1ec88d1ef8684c46d6e48e3098 100644 (file)
--- a/components/tactics/proofEngineReduction.ml
+++ b/components/tactics/proofEngineReduction.ml
@@ -46,8 +46,10 @@ exception WrongUriToInductiveDefinition;;
 exception WrongUriToConstant;;
 exception RelToHiddenHypothesis;;
 
+module C = Cic
+module S = CicSubstitution
+
 let alpha_equivalence =
- let module C = Cic in
   let rec aux t t' =
    if t = t' then true
    else
@@ -122,7 +124,6 @@ exception WhatAndWithWhatDoNotHaveTheSameLength;;
 
 (* "textual" replacement of several subterms with other ones *)
 let replace ~equality ~what ~with_what ~where =
- let module C = Cic in
   let find_image t =
    let rec find_image_aux =
     function
@@ -184,8 +185,6 @@ let replace ~equality ~what ~with_what ~where =
 (* replaces in a term a term with another one. *)
 (* Lifting are performed as usual.             *)
 let replace_lifting ~equality ~what ~with_what ~where =
- let module C = Cic in
- let module S = CicSubstitution in
   let find_image what t =
    let rec find_image_aux =
     function
@@ -282,8 +281,6 @@ let replace_lifting ~equality ~what ~with_what ~where =
 (* replaces in a term a list of terms with other ones. *)
 (* Lifting are performed as usual.                     *)
 let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
- let module C = Cic in
- let module S = CicSubstitution in
   let find_image t =
    let rec find_image_aux =
     function
@@ -373,12 +370,72 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
   substaux 1 where
 ;;
 
+(* This is the inverse of the subst function. *)
+let subst_inv ~equality ~what =
+   let rec find_image t = function
+      | []       -> false
+      | hd :: tl -> equality t hd || find_image t tl 
+   in
+   let rec subst_term k t =
+      if find_image t what then C.Rel k else inspect_term k t
+   and inspect_term k = function
+      | C.Rel n -> if n < k then C.Rel n else C.Rel (succ n)
+      | C.Sort _ as t -> t
+      | C.Implicit _ as t -> t
+      | C.Var (uri, enss) ->
+         let enss = List.map (subst_ens k) enss in
+         C.Var (uri, enss)
+      | C.Const (uri ,enss) ->
+         let enss = List.map (subst_ens k) enss in
+         C.Const (uri, enss)
+     | C.MutInd (uri, tyno, enss) ->
+         let enss = List.map (subst_ens k) enss in
+         C.MutInd (uri, tyno, enss)
+     | C.MutConstruct (uri, tyno, consno, enss) ->
+         let enss = List.map (subst_ens k) enss in
+         C.MutConstruct (uri, tyno, consno, enss)
+     | C.Meta (i, mss) -> 
+         let mss = List.map (subst_ms k) mss in
+         C.Meta(i, mss)
+     | C.Cast (t, v) -> C.Cast (subst_term k t, subst_term k v)
+     | C.Appl ts ->      
+         let ts = List.map (subst_term k) ts in
+         C.Appl ts
+     | C.MutCase (uri, tyno, outty, t, cases) ->
+         let cases = List.map (subst_term k) cases in
+        C.MutCase (uri, tyno, subst_term k outty, subst_term k t, cases)
+     | C.Prod (n, v, t) ->
+        C.Prod (n, subst_term k v, subst_term (succ k) t)
+     | C.Lambda (n, v, t) ->
+        C.Lambda (n, subst_term k v, subst_term (succ k) t)
+     | C.LetIn (n, v, t) ->
+        C.LetIn (n, subst_term k v, subst_term (succ k) t)
+     | C.Fix (i, fixes) ->
+        let fixesno = List.length fixes in
+        let fixes = List.map (subst_fix fixesno k) fixes in
+        C.Fix (i, fixes)
+     | C.CoFix (i, cofixes) ->
+        let cofixesno = List.length cofixes in
+        let cofixes = List.map (subst_cofix cofixesno k) cofixes in
+         C.CoFix (i, cofixes)
+   and subst_ens k (uri, t) = uri, subst_term k t   
+   and subst_ms k = function
+      | None   -> None
+      | Some t -> Some (subst_term k t)
+   and subst_fix fixesno k (n, ind, ty, bo) =
+      n, ind, subst_term k ty, subst_term (k + fixesno) bo
+   and subst_cofix cofixesno k (n, ty, bo) =
+      n, subst_term k ty, subst_term (k + cofixesno) bo
+in
+subst_term
+   
+
+
+
 (* Takes a well-typed term and fully reduces it. *)
 (*CSC: It does not perform reduction in a Case *)
 let reduce context =
  let rec reduceaux context l =
-  let module C = Cic in
-  let module S = CicSubstitution in
    function
       C.Rel n as t ->
        (match List.nth context (n-1) with
@@ -595,8 +652,6 @@ exception AlreadySimplified;;
 (*CSC: It does not perform simplification in a Case *)
 
 let simpl context =
- let module C = Cic in
- let module S = CicSubstitution in
  (* a simplified term is active if it can create a redex when used as an *)
  (* actual parameter                                                     *)
  let rec is_active =
@@ -805,8 +860,6 @@ let simpl context =
   List.map (function uri,t -> uri,reduceaux context [] t)
  (**** Step 2 ****)
  and try_delta_expansion context l term body =
-  let module C = Cic in
-  let module S = CicSubstitution in
    try
     let res,constant_args =
      let rec aux rev_constant_args l =