in
context, t, (C.Meta (newmeta,irl))
else
- raise (Fail "intro(s): not enough products or let-ins")
+ raise (Fail (lazy "intro(s): not enough products or let-ins"))
in
collect_context context howmany ty
| Some (n,Cic.Def (s,None)) ->
Some (n,Cic.Def ((subst_in canonical_context' s),None))
| None -> None
- | Some (_,Cic.Def (_,Some _)) -> assert false
+ | Some (n,Cic.Def (bo,Some ty)) ->
+ Some
+ (n,
+ Cic.Def
+ (subst_in canonical_context' bo,
+ Some (subst_in canonical_context' ty)))
in
entry'::canonical_context'
) canonical_context []
new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff
;;
-let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty =
+let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity =
let (consthead,newmetasenv,arguments,_) =
- saturate_term newmeta' metasenv' context termty in
+ saturate_term newmeta' metasenv' context termty goal_arity in
let subst,newmetasenv',_ =
CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
in
in
subst,newmetasenv',t
-let apply_tac_verbose ~term (proof, goal) =
+let rec count_prods context ty =
+ match CicReduction.whd context ty with
+ Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
+ | _ -> 0
+
+let apply_tac_verbose_with_subst ~term (proof, goal) =
(* Assumption: The term "term" must be closed in the current context *)
let module T = CicTypeChecker in
let module R = CicReduction in
in
let metasenv' = metasenv@newmetasenvfragment in
let termty,_ =
- CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph in
- let termty =
- CicSubstitution.subst_vars exp_named_subst_diff termty
+ CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
in
-(*CSC: this code is suspect and/or bugged: we try first without reduction
- and then using whd. However, the saturate_term always tries with full
- reduction without delta. *)
+ let termty =
+ CicSubstitution.subst_vars exp_named_subst_diff termty in
+ let goal_arity = count_prods context ty in
let subst,newmetasenv',t =
- try
+ let rec add_one_argument n =
+ try
new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty
- termty
- with CicUnification.UnificationFailure _ ->
- new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty
- (CicReduction.whd context termty)
+ termty n
+ with CicUnification.UnificationFailure _ when n > 0 ->
+ add_one_argument (n - 1)
+ in
+ add_one_argument goal_arity
in
let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
let apply_subst = CicMetaSubst.apply_subst subst in
in
let bo' = apply_subst t in
let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
-(* prerr_endline ("me: " ^ CicMetaSubst.ppmetasenv newmetasenv'' subst); *)
let subst_in =
(* if we just apply the subtitution, the type is irrelevant:
we may use Implicit, since it will be dropped *)
let (newproof, newmetasenv''') =
subst_meta_and_metasenv_in_proof proof metano subst_in newmetasenv''
in
- (subst_in,
- (newproof,
- List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
+ (((metano,(context,bo',Cic.Implicit None))::subst)(* subst_in *), (* ALB *)
+ (newproof,
+ List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
-let apply_tac ~term status = snd (apply_tac_verbose ~term status)
-let apply_tac_verbose ~term status =
+(* ALB *)
+let apply_tac_verbose_with_subst ~term status =
try
- apply_tac_verbose ~term status
+(* apply_tac_verbose ~term status *)
+ apply_tac_verbose_with_subst ~term status
(* TODO cacciare anche altre eccezioni? *)
with
- | CicUnification.UnificationFailure _ as e ->
- raise (Fail (Printexc.to_string e))
- | CicTypeChecker.TypeCheckerFailure _ as e ->
- raise (Fail (Printexc.to_string e))
+ | CicUnification.UnificationFailure msg
+ | CicTypeChecker.TypeCheckerFailure msg ->
+ raise (Fail msg)
+
+(* ALB *)
+let apply_tac_verbose ~term status =
+ let subst, status = apply_tac_verbose_with_subst ~term status in
+ (CicMetaSubst.apply_subst subst), status
+
+let apply_tac ~term status = snd (apply_tac_verbose ~term status)
(* TODO per implementare i tatticali e' necessario che tutte le tattiche
sollevino _solamente_ Fail *)
apply_tac ~term status
(* TODO cacciare anche altre eccezioni? *)
with
- | CicUnification.UnificationFailure _ as e ->
- raise (Fail (Printexc.to_string e))
- | CicTypeChecker.TypeCheckerFailure _ as e ->
- raise (Fail (Printexc.to_string e))
+ | CicUnification.UnificationFailure msg
+ | CicTypeChecker.TypeCheckerFailure msg ->
+ raise (Fail msg)
in
mk_tactic (apply_tac ~term)
(newproof, [])
end
else
- raise (Fail "The type of the provided term is not the one expected.")
+ raise (Fail (lazy "The type of the provided term is not the one expected."))
in
mk_tactic (exact_tac ~term)
let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let (termty,metasenv',arguments,fresh_meta) =
ProofEngineHelpers.saturate_term
- (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty in
+ (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
let term = if arguments = [] then term else Cic.Appl (term::arguments) in
let uri,exp_named_subst,typeno,args =
match termty with
in
C.Appl (eliminator_ref :: make_tl term (args_no - 1))
in
- let metasenv', term_to_refine' =
- CicMkImplicit.expand_implicits metasenv' [] context term_to_refine in
let refined_term,_,metasenv'',_ =
- CicRefine.type_of_aux' metasenv' context term_to_refine'
+ CicRefine.type_of_aux' metasenv' context term_to_refine
CicUniv.empty_ugraph
in
let new_goals =
projects / helm.git / blobdiff