X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FeliminationTactics.ml;h=5a293bcafcd4683661b077eee638a24d7992e971;hb=cf25aeb5fa2c00ebfe93454fbe33421d590506d4;hp=e98bcd3c878d6fa597ffda35b85a4ee2e0d4d906;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/tactics/eliminationTactics.ml b/helm/software/components/tactics/eliminationTactics.ml index e98bcd3c8..5a293bcaf 100644 --- a/helm/software/components/tactics/eliminationTactics.ml +++ b/helm/software/components/tactics/eliminationTactics.ml @@ -25,98 +25,122 @@ (* $Id$ *) -module C = Cic -module P = PrimitiveTactics -module T = Tacticals -module S = ProofEngineStructuralRules -module F = FreshNamesGenerator -module E = ProofEngineTypes -module H = ProofEngineHelpers - -(* -let induction_tac ~term status = - let (proof, goal) = status in - let module C = Cic in - let module R = CicReduction in - let module P = PrimitiveTactics in - let module T = Tacticals in - let module S = ProofEngineStructuralRules in - let module U = UriManager in - let (_,metasenv,_,_) = proof in - let _,context,ty = CicUtil.lookup_meta goal metasenv in - let termty = CicTypeChecker.type_of_aux' metasenv context term in (* per ora non serve *) - - T.then_ ~start:(T.repeat_tactic - ~tactic:(T.then_ ~start:(VariousTactics.generalize_tac ~term) (* chissa' se cosi' funziona? *) - ~continuation:(P.intros)) - ~continuation:(P.elim_intros_simpl ~term) - status -;; -*) +module C = Cic +module I = CicInspect +module S = CicSubstitution +module TC = CicTypeChecker +module P = PrimitiveTactics +module T = Tacticals +module PESR = ProofEngineStructuralRules +module F = FreshNamesGenerator +module PET = ProofEngineTypes +module RT = ReductionTactics +module E = CicEnvironment +module R = CicReduction +module Un = CicUniv +module PEH = ProofEngineHelpers + +let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None + +let get_inductive_def uri = + match E.get_obj Un.oblivion_ugraph uri with + | C.InductiveDefinition (tys, _, lpsno, _), _ -> + lpsno, tys + | _ -> assert false + +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, _ = 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 + 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 = 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.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 + 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 *******************************************************) -let get_name context index = - try match List.nth context (pred index) with - | Some (Cic.Name name, _) -> Some name - | _ -> None - with Invalid_argument "List.nth" -> None - 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 get_name context index with + match PEH.get_name context index with | _ when index <= 0 -> (proof, [goal]) | None -> aux (pred index) | Some what -> let tac = T.then_ ~start:(tactic ~what) ~continuation:(scan_tac ~old_context_length:context_length ~index ~tactic) in - try E.apply_tactic tac status - with E.Fail _ -> aux (pred index) - in aux (index + context_length - old_context_length - 1) + try PET.apply_tactic tac status + with PET.Fail _ -> aux (pred index) + in aux (index + context_length - old_context_length) in - E.mk_tactic scan_tac - -let rec check_inductive_types types = function - | C.MutInd (uri, typeno, _) -> List.mem (uri, typeno) types - | C.Appl (hd :: tl) -> check_inductive_types types hd - | _ -> false + PET.mk_tactic scan_tac -let elim_clear_tac ~mk_fresh_name_callback ~types ~what = - let elim_clear_tac status = +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 - if check_inductive_types types ty then - let tac = T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index)) - ~continuation:(S.clear what) - in - E.apply_tactic tac status - else raise (E.Fail (lazy "unexported elim_clear: not an eliminable type")) + 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 (C.Rel index)) + ~continuation:(PESR.clear [what]) + else + let msg = "unexported elim_clear: not an decomposable type" in + raise (PET.Fail (lazy msg)) + in + PET.apply_tactic tac status in - E.mk_tactic elim_clear_tac + PET.mk_tactic elim_clear_unfold_tac (* elim type ****************************************************************) let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) ?depth ?using what = - let elim what = - P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback what + let elim = + P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback in let elim_type_tac status = let tac = T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac] in - E.apply_tactic tac status + PET.apply_tactic tac status in - E.mk_tactic elim_type_tac + PET.mk_tactic elim_type_tac (* decompose ****************************************************************) @@ -129,89 +153,18 @@ let debug_print = fun _ -> () (** debugging print *) let warn s = debug_print (lazy ("DECOMPOSE: " ^ (Lazy.force s))) -(* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *) -let search_inductive_types ty = - let rec aux types = function - | C.MutInd (uri, typeno, _) when (not (List.mem (uri, typeno) types)) -> - (uri, typeno) :: types - | C.Appl applist -> List.fold_left aux types applist - | _ -> types - in - aux [] ty -(* N.B: in un caso tipo (and A forall C:Prop.(or B C)) l'or *non* viene selezionato! *) - (* roba seria ------------------------------------------------------------- *) -let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) - ?(user_types=[]) ~dbd what = +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 types = List.rev_append user_types (FwdQueries.decomposables dbd) in - let tactic = elim_clear_tac ~mk_fresh_name_callback ~types in - let old_context_length = List.length context in - let tac = T.then_ ~start:(tactic ~what) - ~continuation:(scan_tac ~old_context_length ~index:1 ~tactic) + 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 - E.apply_tactic tac status + PET.apply_tactic tac status in - E.mk_tactic decompose_tac - -(* -module R = CicReduction - - let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim status = - let (proof, goal) = status in - warn (lazy ("nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim))); - if nr_of_hyp_still_to_elim <> 0 then - let _,metasenv,_,_ = proof in - let _,context,_ = CicUtil.lookup_meta goal metasenv in - let old_context_len = List.length context in - let termty,_ = - CicTypeChecker.type_of_aux' metasenv context term' - CicUniv.empty_ugraph in - warn (lazy ("elim_clear termty= " ^ CicPp.ppterm termty)); - match termty with - C.MutInd (uri,typeno,exp_named_subst) - | C.Appl((C.MutInd (uri,typeno,exp_named_subst))::_) - when (List.mem (uri,typeno,exp_named_subst) urilist) -> - warn (lazy ("elim " ^ CicPp.ppterm termty)); - ProofEngineTypes.apply_tactic - (T.then_ - ~start:(P.elim_intros_simpl_tac term') - ~continuation:( - (* clear the hyp that has just been eliminated *) - ProofEngineTypes.mk_tactic (fun status -> - let (proof, goal) = status in - let _,metasenv,_,_ = proof in - let _,context,_ = CicUtil.lookup_meta goal metasenv in - let new_context_len = List.length context in - warn (lazy ("newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim))); - let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim + (new_context_len - old_context_len) - 1 in - let hyp_name = - match List.nth context new_nr_of_hyp_still_to_elim with - None - | Some (Cic.Anonymous,_) -> assert false - | Some (Cic.Name name,_) -> name - in - ProofEngineTypes.apply_tactic - (T.then_ - ~start:( - if (term'==term) (* if it's the first application of elim, there's no need to clear the hyp *) - then begin debug_print (lazy ("%%%%%%% no clear")); T.id_tac end - else begin debug_print (lazy ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim)))); (S.clear ~hyp:hyp_name) end) - ~continuation:(ProofEngineTypes.mk_tactic (elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim))) - status - ))) - status - | _ -> - let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim - 1 in - warn (lazy ("fail; hyp=" ^ (string_of_int new_nr_of_hyp_still_to_elim))); - elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim status - else (* no hyp to elim left in this goal *) - ProofEngineTypes.apply_tactic T.id_tac status - - in - elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1 status -*) + PET.mk_tactic decompose_tac