X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FeliminationTactics.ml;h=e74886e95e1146235ef0114fd3b350d4360a5e13;hb=1f974ca07c502d85c9a3760aaaf633bae3c84fb6;hp=c98f020d7139a522be67d9b0c97f26a71a76f18e;hpb=cea3a50f515d1e39467073d2b447a9ddfa1a4852;p=helm.git diff --git a/helm/software/components/tactics/eliminationTactics.ml b/helm/software/components/tactics/eliminationTactics.ml index c98f020d7..e74886e95 100644 --- 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