decompose: delta-expansion of the type to eliminate now works fine

[helm.git] / helm / software / components / tactics / eliminationTactics.ml

diff --git a/helm/software/components/tactics/eliminationTactics.ml b/helm/software/components/tactics/eliminationTactics.ml
index c98f020d7139a522be67d9b0c97f26a71a76f18e..e74886e95e1146235ef0114fd3b350d4360a5e13 100644 (file)
--- a/helm/software/components/tactics/eliminationTactics.ml
+++ b/helm/software/components/tactics/eliminationTactics.ml
@@ -26,9 +26,12 @@
 (* $Id$ *)
 
 module C    = Cic
+module I    = CicInspect
+module S    = CicSubstitution
+module TC   = CicTypeChecker 
 module P    = PrimitiveTactics
 module T    = Tacticals
-module S    = ProofEngineStructuralRules
+module PESR = ProofEngineStructuralRules
 module F    = FreshNamesGenerator
 module PET  = ProofEngineTypes
 module H    = ProofEngineHelpers
@@ -50,28 +53,51 @@ let split c t =
 
 (****************************************************************************)
 
-type type_class = Other
-                | Ind
-               | Con of C.lazy_term
-
 let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None 
 
-let get_inductive_type uri tyno =
+let get_inductive_def uri =
    match E.get_obj Un.empty_ugraph uri with
       | C.InductiveDefinition (tys, _, lpsno, _), _ -> 
-         let _, inductive, arity, _ = List.nth tys tyno in
-         lpsno, inductive, arity
+         lpsno, tys
       | _                                           -> assert false
 
-let rec check_type = function 
-   | C.MutInd (uri, tyno, _) -> 
-      let lpsno, inductive, arity = get_inductive_type uri tyno in
-      let _, psno = split [] arity in
-      if lpsno <> psno && inductive then Other else Ind 
-(*   | C.Const (uri, _) as t     -> 
-      if List.mem (uri, None) types then Con (PET.const_lazy_term t) else Other
-*)   | C.Appl (hd :: tl)         -> check_type hd
-   | _                         -> Other
+let is_not_recursive uri tyno tys = 
+   let map mutinds (_, ty) = 
+(* FG: we can do much better here *)      
+      let map mutinds t = I.S.union mutinds (I.get_mutinds_of_uri uri t) in
+(**********************************)      
+      let premises, _ = split [] ty in
+      List.fold_left map mutinds (List.tl premises)
+   in
+   let msg = "recursiveness check non implemented for mutually inductive types" in
+   if List.length tys > 1 then raise (PET.Fail (lazy msg)) else
+   let _, _, _, constructors = List.nth tys tyno in
+   let mutinds = List.fold_left map I.S.empty constructors in
+   I.S.is_empty mutinds
+
+let rec check_type sorts metasenv context t = 
+   match R.whd ~delta:true context t with
+      | C.MutInd (uri, tyno, _) as t -> 
+         let lpsno, tys = get_inductive_def uri in
+         let _, inductive, arity, _ = List.nth tys tyno in
+         let _, psno = split [] arity in
+         let not_relation = (lpsno = psno) in
+         let not_recursive = is_not_recursive uri tyno tys in
+         let ty_ty, _ = TC.type_of_aux' metasenv context t Un.empty_ugraph in
+         let sort = match split context ty_ty with
+            | C.Sort sort ::_ , _ -> CicPp.ppsort sort
+           | C.Meta _ :: _, _    -> CicPp.ppsort (C.Type (Un.fresh ()))
+           | _                   -> assert false
+         in
+         let right_sort = List.mem sort sorts in
+         if not_relation && inductive && not_recursive && right_sort then
+        begin
+            HLog.warn (Printf.sprintf "Decomposing %s %u" (UriManager.string_of_uri uri) (succ tyno));
+            true 
+         end
+        else false 
+      | C.Appl (hd :: tl)         -> check_type sorts metasenv context hd
+      | _                         -> false
 
 (* unexported tactics *******************************************************)
 
@@ -95,17 +121,17 @@ let rec scan_tac ~old_context_length ~index ~tactic =
    in
    PET.mk_tactic scan_tac
 
-let elim_clear_unfold_tac ~mk_fresh_name_callback ~what =
+let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
    let elim_clear_unfold_tac status =
       let (proof, goal) = status in
       let _, metasenv, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let index, ty = H.lookup_type metasenv context what in
-      let tac = match check_type ty with 
-         | Ind   -> T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
-                           ~continuation:(S.clear [what])
-         | Con t -> RT.unfold_tac (Some t) ~pattern:(premise_pattern what)
-        | Other -> 
+      let tac = 
+         if check_type sorts metasenv context (S.lift index ty) then 
+            T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
+                   ~continuation:(PESR.clear [what])
+        else 
            let msg = "unexported elim_clear: not an decomposable type" in
            raise (PET.Fail (lazy msg))
       in
@@ -142,12 +168,13 @@ let warn s = debug_print (lazy ("DECOMPOSE: " ^ (Lazy.force s)))
 
 (* roba seria ------------------------------------------------------------- *)
 
-let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
+let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort C.CProp]) 
+                  ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
    let decompose_tac status =
       let (proof, goal) = status in
       let _, metasenv,_,_, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
-      let tactic = elim_clear_unfold_tac ~mk_fresh_name_callback in
+      let tactic = elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback in
       let old_context_length = List.length context in      
       let tac = scan_tac ~old_context_length ~index:old_context_length ~tactic
       in