in
PET.mk_tactic (apply_tac ~term)
+let applyP_tac ~term =
+ let applyP_tac status =
+ let res = PET.apply_tactic (apply_tac ~term) status in res
+ in
+ PET.mk_tactic applyP_tac
+
let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ()=
let intros_tac (proof, goal)
=
=
let module PET = ProofEngineTypes in
let generalize_tac mk_fresh_name_callback
- ~pattern:(term,hyps_pat,concl_pat) status
+ ~pattern:(term,hyps_pat,_) status
=
if hyps_pat <> [] then raise GeneralizationInHypothesesNotImplementedYet;
let (proof, goal) = status in
~conjecture ~pattern in
let context = CicMetaSubst.apply_subst_context subst context in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
- let pbo = CicMetaSubst.apply_subst subst pbo in
+ let pbo = lazy (CicMetaSubst.apply_subst subst (Lazy.force pbo)) in
let pty = CicMetaSubst.apply_subst subst pty in
let term =
match term with
List.map
(fun id ->
let rel,_ = ProofEngineHelpers.find_hyp id context in
- id,(Some (PET.const_lazy_term rel), [], None)
+ id,(Some (fun ctx m u -> CicSubstitution.lift (List.length ctx - List.length context) rel,m,u), [], Some (ProofEngineTypes.hole))
) generalize_hyps in
let tactics =
List.map
PET.mk_tactic reorder_pattern
;;
-let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
- let cases_tac ~term (proof, goal) =
+let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ?(pattern = PET.conclusion_pattern None) term =
+ let cases_tac pattern (proof, goal) =
let module TC = CicTypeChecker in
let module U = UriManager in
let module R = CicReduction in
let module C = Cic in
let (curi,metasenv,_subst, proofbo,proofty, attrs) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ let pattern = pattern_after_generalize_pattern_tac pattern in
+ let _cpattern =
+ match pattern with
+ | None, [], Some cpattern ->
+ let rec is_hole =
+ function
+ Cic.Implicit (Some `Hole) -> true
+ | Cic.Prod (Cic.Anonymous,so,tgt) -> is_hole so && is_hole tgt
+ | _ -> false
+ in
+ if not (is_hole cpattern) then
+ raise (PET.Fail (lazy "not implemented"))
+ | _ -> raise (PET.Fail (lazy "not implemented")) in
let termty,_ = TC.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
let termty = CicReduction.whd context termty in
let (termty,metasenv',arguments,fresh_meta) =
right_args
| _ -> assert false
in
- let outtype =
+ let outtypes =
let n_right_args = List.length right_args in
let n_lambdas = n_right_args + 1 in
let lifted_ty = CicSubstitution.lift n_lambdas ty in
if not !replaced then
(* this means the matched term is not there,
* but maybe right params are: we user rels (to right args lambdas) *)
- replace ~what ~with_what:(with_what false) ~where:captured
+ [replace ~what ~with_what:(with_what false) ~where:captured]
else
(* since the matched is there, rights should be inferrable *)
- replace ~what ~with_what:(with_what true) ~where:captured
+ [replace ~what ~with_what:(with_what false) ~where:captured;
+ replace ~what ~with_what:(with_what true) ~where:captured]
in
let captured_term_ty =
let term_ty = CicSubstitution.lift n_right_args termty in
fstn [] args paramsno @ mkrels n_right_args)
| _ -> raise NotAnInductiveTypeToEliminate
in
- let rec add_lambdas = function
+ let rec add_lambdas captured_ty = function
| 0 -> captured_ty
| 1 ->
- C.Lambda (C.Name "matched", captured_term_ty, (add_lambdas 0))
+ C.Lambda (C.Name "matched", captured_term_ty, (add_lambdas captured_ty 0))
| n ->
C.Lambda (C.Name ("right_"^(string_of_int (n-1))),
- C.Implicit None, (add_lambdas (n-1)))
+ C.Implicit None, (add_lambdas captured_ty (n-1)))
in
- add_lambdas n_lambdas
- in
- let term_to_refine = C.MutCase (uri,typeno,outtype,term,patterns) in
- let refined_term,_,metasenv'',_ =
- CicRefine.type_of_aux' metasenv' context term_to_refine
- CicUniv.oblivion_ugraph
- in
- let new_goals =
- ProofEngineHelpers.compare_metasenvs
- ~oldmetasenv:metasenv ~newmetasenv:metasenv''
- in
- let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
- let proof'', new_goals' =
- PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal)
+ List.map (fun x -> add_lambdas x n_lambdas) captured_ty
in
- (* The apply_tactic can have closed some of the new_goals *)
- let patched_new_goals =
- let (_,metasenv''',_subst,_,_,_) = proof'' in
- List.filter
- (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
- new_goals @ new_goals'
- in
- proof'', patched_new_goals
+ let rec first = (* easier than using tacticals *)
+ function
+ | [] -> raise (PET.Fail (lazy ("unable to generate a working outtype")))
+ | outtype::rest ->
+ let term_to_refine = C.MutCase (uri,typeno,outtype,term,patterns) in
+ try
+ let refined_term,_,metasenv'',_ =
+ CicRefine.type_of_aux' metasenv' context term_to_refine
+ CicUniv.oblivion_ugraph
+ in
+ let new_goals =
+ ProofEngineHelpers.compare_metasenvs
+ ~oldmetasenv:metasenv ~newmetasenv:metasenv''
+ in
+ let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
+ let proof'', new_goals' =
+ PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal)
+ in
+ (* The apply_tactic can have closed some of the new_goals *)
+ let patched_new_goals =
+ let (_,metasenv''',_subst,_,_,_) = proof'' in
+ List.filter
+ (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
+ new_goals @ new_goals'
+ in
+ proof'', patched_new_goals
+ with PET.Fail _ | CicRefine.RefineFailure _ | CicRefine.Uncertain _ -> first rest
in
- PET.mk_tactic (cases_tac ~term)
+ first outtypes
+ in
+ let reorder_pattern ((proof, goal) as status) =
+ let _,metasenv,_,_,_,_ = proof in
+ let conjecture = CicUtil.lookup_meta goal metasenv in
+ let _,context,_ = conjecture in
+ let pattern = ProofEngineHelpers.sort_pattern_hyps context pattern in
+ PET.apply_tactic
+ (Tacticals.then_ ~start:(generalize_pattern_tac pattern)
+ ~continuation:(PET.mk_tactic (cases_tac pattern))) status
+ in
+ PET.mk_tactic reorder_pattern
;;
projects / helm.git / blobdiff