X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FeliminationTactics.ml;h=5a293bcafcd4683661b077eee638a24d7992e971;hb=0e3324ad8e6a552ee89f02371412f7bc2e83379f;hp=85eade2d08e0291ac53b7a5cab724f47b4831e26;hpb=8ae990161006978a019f0afda4ff8d56a78d1fd0;p=helm.git diff --git a/helm/software/components/tactics/eliminationTactics.ml b/helm/software/components/tactics/eliminationTactics.ml index 85eade2d0..5a293bcaf 100644 --- a/helm/software/components/tactics/eliminationTactics.ml +++ b/helm/software/components/tactics/eliminationTactics.ml @@ -34,29 +34,16 @@ module T = Tacticals module PESR = ProofEngineStructuralRules module F = FreshNamesGenerator module PET = ProofEngineTypes -module H = ProofEngineHelpers module RT = ReductionTactics module E = CicEnvironment module R = CicReduction module Un = CicUniv - -(* from ProceduralClasify ***************************************************) - -let split c t = - let add s v c = Some (s, C.Decl v) :: c in - let rec aux whd a n c = function - | C.Prod (s, v, t) -> aux false (v :: a) (succ n) (add s v c) t - | v when whd -> v :: a, n - | v -> aux true a n c (R.whd ~delta:true c v) - in - aux false [] 0 c t - -(****************************************************************************) +module PEH = ProofEngineHelpers let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None let get_inductive_def uri = - match E.get_obj Un.empty_ugraph uri with + match E.get_obj Un.oblivion_ugraph uri with | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, tys | _ -> assert false @@ -64,9 +51,9 @@ let get_inductive_def uri = 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 map mutinds (_, t) = I.S.union mutinds (I.get_mutinds_of_uri uri t) in (**********************************) - let premises, _ = split [] ty in + let premises, _ = PEH.split_with_whd ([], ty) in List.fold_left map mutinds (List.tl premises) in let msg = "recursiveness check non implemented for mutually inductive types" in @@ -80,14 +67,14 @@ let rec check_type sorts metasenv context t = | 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 _, psno = PEH.split_with_whd ([], 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 + let ty_ty, _ = TC.type_of_aux' metasenv context t Un.oblivion_ugraph in + let sort = match PEH.split_with_whd (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 @@ -104,11 +91,11 @@ let rec check_type sorts metasenv context t = let rec scan_tac ~old_context_length ~index ~tactic = let scan_tac status = let (proof, goal) = status in - let _, metasenv, _, _, _ = proof in + let _, metasenv, _subst, _, _, _ = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in let context_length = List.length context in let rec aux index = - match H.get_name context index with + match PEH.get_name context index with | _ when index <= 0 -> (proof, [goal]) | None -> aux (pred index) | Some what -> @@ -124,13 +111,12 @@ let rec scan_tac ~old_context_length ~index ~tactic = 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 _, metasenv, _subst, _, _, _ = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in - let index, ty = H.lookup_type metasenv context what in - let pattern = PET.conclusion_pattern (Some (C.Rel index)) in + let index, ty = PEH.lookup_type metasenv context what in let tac = if check_type sorts metasenv context (S.lift index ty) then - T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback pattern) + 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 @@ -149,9 +135,8 @@ let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) ?depth P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback in let elim_type_tac status = - let pattern = PET.conclusion_pattern (Some (C.Rel 1)) in let tac = - T.thens ~start: (P.cut_tac what) ~continuations:[elim pattern; T.id_tac] + T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac] in PET.apply_tactic tac status in @@ -170,11 +155,11 @@ let warn s = debug_print (lazy ("DECOMPOSE: " ^ (Lazy.force s))) (* roba seria ------------------------------------------------------------- *) -let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort C.CProp]) +let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort (C.CProp (CicUniv.fresh ()))]) ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () = let decompose_tac status = let (proof, goal) = status in - let _, metasenv,_,_, _ = proof in + let _, metasenv, _subst, _,_, _ = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in let tactic = elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback in let old_context_length = List.length context in