(* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
let (head, newmetas, args, newmeta) =
ProofEngineHelpers.saturate_term newmeta []
- context (S.lift index term)
+ context (S.lift index term) 0
in
let p =
if List.length args = 0 then
match termty with
| C.Prod (name, s, t) ->
let head, newmetas, args, newmeta =
- ProofEngineHelpers.saturate_term newmeta [] context termty
+ ProofEngineHelpers.saturate_term newmeta [] context termty 0
in
let p =
if List.length args = 0 then
CicUniv.empty_ugraph in
let (ty_eq,metasenv',arguments,fresh_meta) =
ProofEngineHelpers.saturate_term
- (ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq in
+ (ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq 0 in
let equality =
if List.length arguments = 0 then
equality
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 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 ~term (proof, goal) =
(* Assumption: The term "term" must be closed in the current context *)
let module T = CicTypeChecker in
let termty,_ =
CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph in
let termty =
- CicSubstitution.subst_vars exp_named_subst_diff termty
- 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. *)
+ 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
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
res @ locate_in_term what ~where:ty context
-(* saturate_term newmeta metasenv context ty *)
-(* Given a type [ty] (a backbone), it returns its head and a new metasenv in *)
-(* which there is new a META for each hypothesis, a list of arguments for the *)
-(* new applications and the index of the last new META introduced. The nth *)
-(* argument in the list of arguments is just the nth new META. *)
-let saturate_term newmeta metasenv context ty =
+(* saturate_term newmeta metasenv context ty goal_arity *)
+(* Given a type [ty] (a backbone), it returns its suffix of length *)
+(* [goal_arity] head and a new metasenv in which there is new a META for each *)
+(* hypothesis, a list of arguments for the new applications and the index of *)
+(* the last new META introduced. The nth argument in the list of arguments is *)
+(* just the nth new META. *)
+let saturate_term newmeta metasenv context ty goal_arity =
let module C = Cic in
let module S = CicSubstitution in
+ assert (goal_arity >= 0);
let rec aux newmeta ty =
- let ty' = ty in
- match ty' with
+ match ty with
C.Cast (he,_) -> aux newmeta he
(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type
(* If the expected type is a Type, then also Set is OK ==>
CicMkImplicit.identity_relocation_list_for_metavariable context
in
let newargument = C.Meta (newmeta,irl) in
- let (res,newmetasenv,arguments,lastmeta) =
+ let res,newmetasenv,arguments,lastmeta,prod_no =
aux (newmeta + 1) (S.subst newargument t)
in
- let s' = CicReduction.normalize ~delta:false context s in
- res,(newmeta,context,s')::newmetasenv,newargument::arguments,lastmeta
- (** NORMALIZE RATIONALE
- * we normalize the target only NOW since we may be in this case:
- * A1 -> A2 -> T where T = (\lambda x.A3 -> P) k
- * and we want a mesasenv with ?1:A1 and ?2:A2 and not
- * ?1, ?2, ?3 (that is the one we whould get if we start from the
- * beta-normalized A1 -> A2 -> A3 -> P **)
- | t -> (CicReduction.normalize ~delta:false context t),[],[],newmeta
+ if prod_no + 1 = goal_arity then
+ let head = CicReduction.normalize ~delta:false context ty in
+ head,[],[],newmeta,goal_arity + 1
+ else
+ (** NORMALIZE RATIONALE
+ * we normalize the target only NOW since we may be in this case:
+ * A1 -> A2 -> T where T = (\lambda x.A3 -> P) k
+ * and we want a mesasenv with ?1:A1 and ?2:A2 and not
+ * ?1, ?2, ?3 (that is the one we whould get if we start from the
+ * beta-normalized A1 -> A2 -> A3 -> P **)
+ let s' = CicReduction.normalize ~delta:false context s in
+ res,(newmeta,context,s')::newmetasenv,newargument::arguments,
+ lastmeta,prod_no + 1
+ | t ->
+ let head = CicReduction.normalize ~delta:false context t in
+ match CicReduction.whd context head with
+ C.Prod _ as head' -> aux newmeta head'
+ | _ -> head,[],[],newmeta,0
in
(* WARNING: here we are using the invariant that above the most *)
(* recente new_meta() there are no used metas. *)
- let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
+ let res,newmetasenv,arguments,lastmeta,_ = aux newmeta ty in
res,metasenv @ newmetasenv,arguments,lastmeta
let lookup_type metasenv context hyp =
?equality:(Cic.context -> Cic.term -> Cic.term -> bool) ->
Cic.term -> Cic.conjecture -> (Cic.context * Cic.term) list
-(* saturate_term newmeta metasenv context ty *)
-(* Given a type [ty] (a backbone), it returns its head and a new metasenv in *)
-(* which there is new a META for each hypothesis, a list of arguments for the *)
-(* new applications and the index of the last new META introduced. The nth *)
-(* argument in the list of arguments is just the nth new META. *)
+(* saturate_term newmeta metasenv context ty goal_arity *)
+(* Given a type [ty] (a backbone), it returns its suffix of length *)
+(* [goal_arity] head and a new metasenv in which there is new a META for each *)
+(* hypothesis, a list of arguments for the new applications and the index of *)
+(* the last new META introduced. The nth argument in the list of arguments is *)
+(* just the nth new META. *)
val saturate_term:
- int -> Cic.metasenv -> Cic.context -> Cic.term ->
+ int -> Cic.metasenv -> Cic.context -> Cic.term -> int ->
Cic.term * Cic.metasenv * Cic.term list * int
(* returns the index and the type of a premise in a context *)
projects / helm.git / commitdiff