in
PET.mk_tactic (letin_tac ~mk_fresh_name_callback term)
- (** functional part of the "exact" tactic *)
-let exact_tac ~term =
- let exact_tac ~term (proof, goal) =
- (* Assumption: the term bo must be closed in the current context *)
- let (_,metasenv,_subst,_,_, _) = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let module T = CicTypeChecker in
- let module R = CicReduction in
- let ty_term,u = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
- let b,_ = R.are_convertible context ty_term ty u in (* TASSI: FIXME *)
- if b then
- begin
- let (newproof, metasenv') =
- ProofEngineHelpers.subst_meta_in_proof proof metano term [] in
- (newproof, [])
- end
- else
- raise (PET.Fail (lazy "The type of the provided term is not the one expected."))
- in
- PET.mk_tactic (exact_tac ~term)
+(* FG: exact_tac := apply_tac as in NTactics *)
+let exact_tac ~term = apply_tac ~term
(* not really "primitive" tactics .... *)
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
+ List.map (fun x -> add_lambdas x n_lambdas) captured_ty
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)
- 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
+ first outtypes
+ in
let reorder_pattern ((proof, goal) as status) =
let _,metasenv,_,_,_,_ = proof in
let conjecture = CicUtil.lookup_meta goal metasenv in