diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 1806 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 410 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 764 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 54 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 850 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 1191 |
6 files changed, 2537 insertions, 2538 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index b8e1286b9e..17498c6384 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -33,7 +33,7 @@ let do_observe_tac s tac g = let e = ExplainErr.process_vernac_interp_error e in let goal = begin try (Printer.pr_goal g) with _ -> assert false end in msg_debug (str "observation "++ s++str " raised exception " ++ - Errors.print e ++ str " on goal " ++ goal ); + Errors.print e ++ str " on goal " ++ goal ); raise e;; let observe_tac_stream s tac g = @@ -47,19 +47,19 @@ let observe_tac s tac g = observe_tac_stream (str s) tac g let debug_queue = Stack.create () -let rec print_debug_queue e = - if not (Stack.is_empty debug_queue) +let rec print_debug_queue e = + if not (Stack.is_empty debug_queue) then begin - let lmsg,goal = Stack.pop debug_queue in + let lmsg,goal = Stack.pop debug_queue in let _ = - match e with - | Some e -> - Feedback.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal)) - | None -> - begin - Feedback.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal); - end in + match e with + | Some e -> + Feedback.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal)) + | None -> + begin + Feedback.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal); + end in print_debug_queue None ; end @@ -68,11 +68,11 @@ let observe strm = then Feedback.msg_debug strm else () -let do_observe_tac s tac g = +let do_observe_tac s tac g = let goal = Printer.pr_goal g in - let lmsg = (str "observation : ") ++ s in + let lmsg = (str "observation : ") ++ s in Stack.push (lmsg,goal) debug_queue; - try + try let v = tac g in ignore(Stack.pop debug_queue); v @@ -88,7 +88,7 @@ let observe_tac_stream s tac g = else tac g let observe_tac s = observe_tac_stream (str s) - + let list_chop ?(msg="") n l = try @@ -138,11 +138,11 @@ let is_trivial_eq sigma t = let res = try begin match EConstr.kind sigma t with - | App(f,[|_;t1;t2|]) when eq_constr sigma f (Lazy.force eq) -> - eq_constr sigma t1 t2 - | App(f,[|t1;a1;t2;a2|]) when eq_constr sigma f (jmeq ()) -> - eq_constr sigma t1 t2 && eq_constr sigma a1 a2 - | _ -> false + | App(f,[|_;t1;t2|]) when eq_constr sigma f (Lazy.force eq) -> + eq_constr sigma t1 t2 + | App(f,[|t1;a1;t2;a2|]) when eq_constr sigma f (jmeq ()) -> + eq_constr sigma t1 t2 && eq_constr sigma a1 a2 + | _ -> false end with e when CErrors.noncritical e -> false in @@ -157,19 +157,19 @@ let rec incompatible_constructor_terms sigma t1 t2 = isConstruct sigma c1 && isConstruct sigma c2 && ( not (eq_constr sigma c1 c2) || - List.exists2 (incompatible_constructor_terms sigma) arg1 arg2 + List.exists2 (incompatible_constructor_terms sigma) arg1 arg2 ) let is_incompatible_eq env sigma t = let res = try match EConstr.kind sigma t with - | App(f,[|_;t1;t2|]) when eq_constr sigma f (Lazy.force eq) -> - incompatible_constructor_terms sigma t1 t2 - | App(f,[|u1;t1;u2;t2|]) when eq_constr sigma f (jmeq ()) -> - (eq_constr sigma u1 u2 && - incompatible_constructor_terms sigma t1 t2) - | _ -> false + | App(f,[|_;t1;t2|]) when eq_constr sigma f (Lazy.force eq) -> + incompatible_constructor_terms sigma t1 t2 + | App(f,[|u1;t1;u2;t2|]) when eq_constr sigma f (jmeq ()) -> + (eq_constr sigma u1 u2 && + incompatible_constructor_terms sigma t1 t2) + | _ -> false with e when CErrors.noncritical e -> false in if res then observe (str "is_incompatible_eq " ++ pr_leconstr_env env sigma t); @@ -182,8 +182,8 @@ let change_hyp_with_using msg hyp_id t tac : tactic = ((* observe_tac msg *) Proofview.V82.of_tactic (assert_by (Name prov_id) t (Proofview.V82.tactic (tclCOMPLETE tac)))) [tclTHENLIST [ - (* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]); - (* observe_tac "change_hyp_with_using rename " *) (Proofview.V82.of_tactic (rename_hyp [prov_id,hyp_id])) + (* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]); + (* observe_tac "change_hyp_with_using rename " *) (Proofview.V82.of_tactic (rename_hyp [prov_id,hyp_id])) ]] g exception TOREMOVE @@ -195,15 +195,15 @@ let prove_trivial_eq h_id context (constructor,type_of_term,term) = [ tclDO nb_intros (Proofview.V82.of_tactic intro); (* introducing context *) (fun g -> - let context_hyps = - fst (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g)) - in - let context_hyps' = - (mkApp(constructor,[|type_of_term;term|])):: - (List.map mkVar context_hyps) - in - let to_refine = applist(mkVar h_id,List.rev context_hyps') in - refine to_refine g + let context_hyps = + fst (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g)) + in + let context_hyps' = + (mkApp(constructor,[|type_of_term;term|])):: + (List.map mkVar context_hyps) + in + let to_refine = applist(mkVar h_id,List.rev context_hyps') in + refine to_refine g ) ] @@ -244,18 +244,18 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = let f_eq,args = destApp sigma t in let constructor,t1,t2,t1_typ = try - if (eq_constr f_eq (Lazy.force eq)) - then - let t1 = (args.(1),args.(0)) - and t2 = (args.(2),args.(0)) - and t1_typ = args.(0) - in - (Lazy.force refl_equal,t1,t2,t1_typ) - else - if (eq_constr f_eq (jmeq ())) - then - (jmeq_refl (),(args.(1),args.(0)),(args.(3),args.(2)),args.(0)) - else nochange "not an equality" + if (eq_constr f_eq (Lazy.force eq)) + then + let t1 = (args.(1),args.(0)) + and t2 = (args.(2),args.(0)) + and t1_typ = args.(0) + in + (Lazy.force refl_equal,t1,t2,t1_typ) + else + if (eq_constr f_eq (jmeq ())) + then + (jmeq_refl (),(args.(1),args.(0)),(args.(3),args.(2)),args.(0)) + else nochange "not an equality" with e when CErrors.noncritical e -> nochange "not an equality" in if not ((closed0 sigma (fst t1)) && (closed0 sigma (snd t1)))then nochange "not a closed lhs"; @@ -263,60 +263,60 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = (* observe (str "compute_substitution : " ++ pr_lconstr t1 ++ str " === " ++ pr_lconstr t2); *) if isRel sigma t2 then - let t2 = destRel sigma t2 in - begin - try - let t1' = Int.Map.find t2 sub in - if not (eq_constr t1 t1') then nochange "twice bound variable"; - sub - with Not_found -> - assert (closed0 sigma t1); - Int.Map.add t2 t1 sub - end + let t2 = destRel sigma t2 in + begin + try + let t1' = Int.Map.find t2 sub in + if not (eq_constr t1 t1') then nochange "twice bound variable"; + sub + with Not_found -> + assert (closed0 sigma t1); + Int.Map.add t2 t1 sub + end else if isAppConstruct sigma t1 && isAppConstruct sigma t2 then - begin - let c1,args1 = find_rectype env sigma t1 - and c2,args2 = find_rectype env sigma t2 - in - if not (eq_constr c1 c2) then nochange "cannot solve (diff)"; - List.fold_left2 compute_substitution sub args1 args2 - end + begin + let c1,args1 = find_rectype env sigma t1 + and c2,args2 = find_rectype env sigma t2 + in + if not (eq_constr c1 c2) then nochange "cannot solve (diff)"; + List.fold_left2 compute_substitution sub args1 args2 + end else - if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reductionops.whd_all env sigma t1) t2) "cannot solve (diff)" + if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reductionops.whd_all env sigma t1) t2) "cannot solve (diff)" in let sub = compute_substitution Int.Map.empty (snd t1) (snd t2) in let sub = compute_substitution sub (fst t1) (fst t2) in let end_of_type_with_pop = pop end_of_type in (*the equation will be removed *) let new_end_of_type = (* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4 - Can be safely replaced by the next comment for Ocaml >= 3.08.4 + Can be safely replaced by the next comment for Ocaml >= 3.08.4 *) let sub = Int.Map.bindings sub in List.fold_left (fun end_of_type (i,t) -> liftn 1 i (substnl [t] (i-1) end_of_type)) - end_of_type_with_pop - sub + end_of_type_with_pop + sub in let old_context_length = List.length context + 1 in let witness_fun = mkLetIn(make_annot Anonymous Sorts.Relevant,make_refl_eq constructor t1_typ (fst t1),t, - mkApp(mkVar hyp_id,Array.init old_context_length (fun i -> mkRel (old_context_length - i))) - ) + mkApp(mkVar hyp_id,Array.init old_context_length (fun i -> mkRel (old_context_length - i))) + ) in let new_type_of_hyp,ctxt_size,witness_fun = List.fold_left_i - (fun i (end_of_type,ctxt_size,witness_fun) decl -> - try - let witness = Int.Map.find i sub in - if is_local_def decl then anomaly (Pp.str "can not redefine a rel!"); + (fun i (end_of_type,ctxt_size,witness_fun) decl -> + try + let witness = Int.Map.find i sub in + if is_local_def decl then anomaly (Pp.str "can not redefine a rel!"); (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_annot decl, witness, RelDecl.get_type decl, witness_fun)) - with Not_found -> - (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) - ) - 1 - (new_end_of_type,0,witness_fun) - context + with Not_found -> + (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) + ) + 1 + (new_end_of_type,0,witness_fun) + context in let new_type_of_hyp = Reductionops.nf_betaiota env sigma new_type_of_hyp in @@ -325,31 +325,31 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = in let prove_new_hyp : tactic = tclTHEN - (tclDO ctxt_size (Proofview.V82.of_tactic intro)) - (fun g -> - let all_ids = pf_ids_of_hyps g in - let new_ids,_ = list_chop ctxt_size all_ids in - let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in - let evm, _ = pf_apply Typing.type_of g to_refine in - tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g - ) + (tclDO ctxt_size (Proofview.V82.of_tactic intro)) + (fun g -> + let all_ids = pf_ids_of_hyps g in + let new_ids,_ = list_chop ctxt_size all_ids in + let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in + let evm, _ = pf_apply Typing.type_of g to_refine in + tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g + ) in let simpl_eq_tac = change_hyp_with_using "prove_pattern_simplification" hyp_id new_type_of_hyp prove_new_hyp in (* observe (str "In " ++ Ppconstr.pr_id hyp_id ++ *) -(* str "removing an equation " ++ fnl ()++ *) -(* str "old_typ_of_hyp :=" ++ *) -(* Printer.pr_lconstr_env *) -(* env *) -(* (it_mkProd_or_LetIn ~init:end_of_type ((x,None,t)::context)) *) -(* ++ fnl () ++ *) -(* str "new_typ_of_hyp := "++ *) -(* Printer.pr_lconstr_env env new_type_of_hyp ++ fnl () *) -(* ++ str "old context := " ++ pr_rel_context env context ++ fnl () *) -(* ++ str "new context := " ++ pr_rel_context env new_ctxt ++ fnl () *) -(* ++ str "old type := " ++ pr_lconstr end_of_type ++ fnl () *) -(* ++ str "new type := " ++ pr_lconstr new_end_of_type ++ fnl () *) +(* str "removing an equation " ++ fnl ()++ *) +(* str "old_typ_of_hyp :=" ++ *) +(* Printer.pr_lconstr_env *) +(* env *) +(* (it_mkProd_or_LetIn ~init:end_of_type ((x,None,t)::context)) *) +(* ++ fnl () ++ *) +(* str "new_typ_of_hyp := "++ *) +(* Printer.pr_lconstr_env env new_type_of_hyp ++ fnl () *) +(* ++ str "old context := " ++ pr_rel_context env context ++ fnl () *) +(* ++ str "new context := " ++ pr_rel_context env new_ctxt ++ fnl () *) +(* ++ str "old type := " ++ pr_lconstr end_of_type ++ fnl () *) +(* ++ str "new type := " ++ pr_lconstr new_end_of_type ++ fnl () *) (* ); *) new_ctxt,new_end_of_type,simpl_eq_tac @@ -361,8 +361,8 @@ let is_property sigma (ptes_info:ptes_info) t_x full_type_of_hyp = if isVar sigma pte && Array.for_all (closed0 sigma) args then try - let info = Id.Map.find (destVar sigma pte) ptes_info in - info.is_valid full_type_of_hyp + let info = Id.Map.find (destVar sigma pte) ptes_info in + info.is_valid full_type_of_hyp with Not_found -> false else false else false @@ -377,7 +377,7 @@ let h_reduce_with_zeta cl = Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags - with Genredexpr.rDelta = false; + with Genredexpr.rDelta = false; }) cl) @@ -397,12 +397,12 @@ let rewrite_until_var arg_num eq_ids : tactic = then tclIDTAC g else match eq_ids with - | [] -> anomaly (Pp.str "Cannot find a way to prove recursive property."); - | eq_id::eq_ids -> - tclTHEN - (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar eq_id)))) - (do_rewrite eq_ids) - g + | [] -> anomaly (Pp.str "Cannot find a way to prove recursive property."); + | eq_id::eq_ids -> + tclTHEN + (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar eq_id)))) + (do_rewrite eq_ids) + g in do_rewrite eq_ids @@ -418,129 +418,129 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = let reduced_type_of_hyp = Reductionops.nf_betaiotazeta env sigma real_type_of_hyp in (* length of context didn't change ? *) let new_context,new_typ_of_hyp = - decompose_prod_n_assum sigma (List.length context) reduced_type_of_hyp + decompose_prod_n_assum sigma (List.length context) reduced_type_of_hyp in tclTHENLIST - [ h_reduce_with_zeta (Locusops.onHyp hyp_id); - scan_type new_context new_typ_of_hyp ] + [ h_reduce_with_zeta (Locusops.onHyp hyp_id); + scan_type new_context new_typ_of_hyp ] else if isProd sigma type_of_hyp then begin let (x,t_x,t') = destProd sigma type_of_hyp in - let actual_real_type_of_hyp = it_mkProd_or_LetIn t' context in - if is_property sigma ptes_infos t_x actual_real_type_of_hyp then - begin - let pte,pte_args = (destApp sigma t_x) in - let (* fix_info *) prove_rec_hyp = (Id.Map.find (destVar sigma pte) ptes_infos).proving_tac in - let popped_t' = pop t' in - let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in - let prove_new_type_of_hyp = - let context_length = List.length context in - tclTHENLIST - [ - tclDO context_length (Proofview.V82.of_tactic intro); - (fun g -> - let context_hyps_ids = - fst (list_chop ~msg:"rec hyp : context_hyps" - context_length (pf_ids_of_hyps g)) - in - let rec_pte_id = pf_get_new_id rec_pte_id g in - let to_refine = - applist(mkVar hyp_id, - List.rev_map mkVar (rec_pte_id::context_hyps_ids) - ) - in -(* observe_tac "rec hyp " *) - (tclTHENS - (Proofview.V82.of_tactic (assert_before (Name rec_pte_id) t_x)) - [ - (* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps); -(* observe_tac "prove rec hyp" *) - (refine to_refine) - ]) - g - ) - ] - in - tclTHENLIST - [ -(* observe_tac "hyp rec" *) - (change_hyp_with_using "rec_hyp_tac" hyp_id real_type_of_hyp prove_new_type_of_hyp); - scan_type context popped_t' - ] - end - else if eq_constr sigma t_x coq_False then - begin -(* observe (str "Removing : "++ Ppconstr.pr_id hyp_id++ *) -(* str " since it has False in its preconds " *) -(* ); *) - raise TOREMOVE; (* False -> .. useless *) - end + let actual_real_type_of_hyp = it_mkProd_or_LetIn t' context in + if is_property sigma ptes_infos t_x actual_real_type_of_hyp then + begin + let pte,pte_args = (destApp sigma t_x) in + let (* fix_info *) prove_rec_hyp = (Id.Map.find (destVar sigma pte) ptes_infos).proving_tac in + let popped_t' = pop t' in + let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in + let prove_new_type_of_hyp = + let context_length = List.length context in + tclTHENLIST + [ + tclDO context_length (Proofview.V82.of_tactic intro); + (fun g -> + let context_hyps_ids = + fst (list_chop ~msg:"rec hyp : context_hyps" + context_length (pf_ids_of_hyps g)) + in + let rec_pte_id = pf_get_new_id rec_pte_id g in + let to_refine = + applist(mkVar hyp_id, + List.rev_map mkVar (rec_pte_id::context_hyps_ids) + ) + in +(* observe_tac "rec hyp " *) + (tclTHENS + (Proofview.V82.of_tactic (assert_before (Name rec_pte_id) t_x)) + [ + (* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps); +(* observe_tac "prove rec hyp" *) + (refine to_refine) + ]) + g + ) + ] + in + tclTHENLIST + [ +(* observe_tac "hyp rec" *) + (change_hyp_with_using "rec_hyp_tac" hyp_id real_type_of_hyp prove_new_type_of_hyp); + scan_type context popped_t' + ] + end + else if eq_constr sigma t_x coq_False then + begin +(* observe (str "Removing : "++ Ppconstr.pr_id hyp_id++ *) +(* str " since it has False in its preconds " *) +(* ); *) + raise TOREMOVE; (* False -> .. useless *) + end else if is_incompatible_eq env sigma t_x then raise TOREMOVE (* t_x := C1 ... = C2 ... *) - else if eq_constr sigma t_x coq_True (* Trivial => we remove this precons *) - then -(* observe (str "In "++Ppconstr.pr_id hyp_id++ *) -(* str " removing useless precond True" *) -(* ); *) - let popped_t' = pop t' in - let real_type_of_hyp = - it_mkProd_or_LetIn popped_t' context - in - let prove_trivial = - let nb_intro = List.length context in - tclTHENLIST [ - tclDO nb_intro (Proofview.V82.of_tactic intro); - (fun g -> - let context_hyps = - fst (list_chop ~msg:"removing True : context_hyps "nb_intro (pf_ids_of_hyps g)) - in - let to_refine = - applist (mkVar hyp_id, - List.rev (coq_I::List.map mkVar context_hyps) - ) - in - refine to_refine g - ) - ] - in - tclTHENLIST[ - change_hyp_with_using "prove_trivial" hyp_id real_type_of_hyp - ((* observe_tac "prove_trivial" *) prove_trivial); - scan_type context popped_t' - ] - else if is_trivial_eq sigma t_x - then (* t_x := t = t => we remove this precond *) - let popped_t' = pop t' in - let real_type_of_hyp = - it_mkProd_or_LetIn popped_t' context - in - let hd,args = destApp sigma t_x in - let get_args hd args = - if eq_constr sigma hd (Lazy.force eq) - then (Lazy.force refl_equal,args.(0),args.(1)) - else (jmeq_refl (),args.(0),args.(1)) - in - tclTHENLIST - [ - change_hyp_with_using - "prove_trivial_eq" - hyp_id - real_type_of_hyp - ((* observe_tac "prove_trivial_eq" *) - (prove_trivial_eq hyp_id context (get_args hd args))); - scan_type context popped_t' - ] - else - begin - try - let new_context,new_t',tac = change_eq env sigma hyp_id context x t_x t' in - tclTHEN - tac - (scan_type new_context new_t') - with NoChange -> - (* Last thing todo : push the rel in the context and continue *) + else if eq_constr sigma t_x coq_True (* Trivial => we remove this precons *) + then +(* observe (str "In "++Ppconstr.pr_id hyp_id++ *) +(* str " removing useless precond True" *) +(* ); *) + let popped_t' = pop t' in + let real_type_of_hyp = + it_mkProd_or_LetIn popped_t' context + in + let prove_trivial = + let nb_intro = List.length context in + tclTHENLIST [ + tclDO nb_intro (Proofview.V82.of_tactic intro); + (fun g -> + let context_hyps = + fst (list_chop ~msg:"removing True : context_hyps "nb_intro (pf_ids_of_hyps g)) + in + let to_refine = + applist (mkVar hyp_id, + List.rev (coq_I::List.map mkVar context_hyps) + ) + in + refine to_refine g + ) + ] + in + tclTHENLIST[ + change_hyp_with_using "prove_trivial" hyp_id real_type_of_hyp + ((* observe_tac "prove_trivial" *) prove_trivial); + scan_type context popped_t' + ] + else if is_trivial_eq sigma t_x + then (* t_x := t = t => we remove this precond *) + let popped_t' = pop t' in + let real_type_of_hyp = + it_mkProd_or_LetIn popped_t' context + in + let hd,args = destApp sigma t_x in + let get_args hd args = + if eq_constr sigma hd (Lazy.force eq) + then (Lazy.force refl_equal,args.(0),args.(1)) + else (jmeq_refl (),args.(0),args.(1)) + in + tclTHENLIST + [ + change_hyp_with_using + "prove_trivial_eq" + hyp_id + real_type_of_hyp + ((* observe_tac "prove_trivial_eq" *) + (prove_trivial_eq hyp_id context (get_args hd args))); + scan_type context popped_t' + ] + else + begin + try + let new_context,new_t',tac = change_eq env sigma hyp_id context x t_x t' in + tclTHEN + tac + (scan_type new_context new_t') + with NoChange -> + (* Last thing todo : push the rel in the context and continue *) scan_type (LocalAssum (x,t_x) :: context) t' - end + end end else tclIDTAC @@ -558,25 +558,25 @@ let clean_goal_with_heq ptes_infos continue_tac (dyn_infos:body_info) = in let tac,new_hyps = List.fold_left ( - fun (hyps_tac,new_hyps) hyp_id -> - let hyp_tac,new_hyp = - clean_hyp_with_heq ptes_infos dyn_infos.eq_hyps hyp_id env sigma - in - (tclTHEN hyp_tac hyps_tac),new_hyp@new_hyps + fun (hyps_tac,new_hyps) hyp_id -> + let hyp_tac,new_hyp = + clean_hyp_with_heq ptes_infos dyn_infos.eq_hyps hyp_id env sigma + in + (tclTHEN hyp_tac hyps_tac),new_hyp@new_hyps ) - (tclIDTAC,[]) - dyn_infos.rec_hyps + (tclIDTAC,[]) + dyn_infos.rec_hyps in let new_infos = { dyn_infos with - rec_hyps = new_hyps; - nb_rec_hyps = List.length new_hyps + rec_hyps = new_hyps; + nb_rec_hyps = List.length new_hyps } in tclTHENLIST [ - tac ; - (* observe_tac "clean_hyp_with_heq continue" *) (continue_tac new_infos) + tac ; + (* observe_tac "clean_hyp_with_heq continue" *) (continue_tac new_infos) ] g @@ -587,41 +587,41 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in tclTHENLIST [ - (* We first introduce the variables *) - tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps))); - (* Then the equation itself *) - Proofview.V82.of_tactic (intro_using heq_id); - onLastHypId (fun heq_id -> tclTHENLIST [ - (* Then the new hypothesis *) + (* We first introduce the variables *) + tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps))); + (* Then the equation itself *) + Proofview.V82.of_tactic (intro_using heq_id); + onLastHypId (fun heq_id -> tclTHENLIST [ + (* Then the new hypothesis *) tclMAP (fun id -> Proofview.V82.of_tactic (introduction id)) dyn_infos.rec_hyps; - observe_tac "after_introduction" (fun g' -> - (* We get infos on the equations introduced*) - let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in - (* compute the new value of the body *) - let new_term_value = - match EConstr.kind (project g') new_term_value_eq with - | App(f,[| _;_;args2 |]) -> args2 - | _ -> - observe (str "cannot compute new term value : " ++ pr_gls g' ++ fnl () ++ str "last hyp is" ++ - pr_leconstr_env (pf_env g') (project g') new_term_value_eq - ); - anomaly (Pp.str "cannot compute new term value.") - in - let fun_body = + observe_tac "after_introduction" (fun g' -> + (* We get infos on the equations introduced*) + let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in + (* compute the new value of the body *) + let new_term_value = + match EConstr.kind (project g') new_term_value_eq with + | App(f,[| _;_;args2 |]) -> args2 + | _ -> + observe (str "cannot compute new term value : " ++ pr_gls g' ++ fnl () ++ str "last hyp is" ++ + pr_leconstr_env (pf_env g') (project g') new_term_value_eq + ); + anomaly (Pp.str "cannot compute new term value.") + in + let fun_body = mkLambda(make_annot Anonymous Sorts.Relevant, - pf_unsafe_type_of g' term, - Termops.replace_term (project g') term (mkRel 1) dyn_infos.info - ) - in - let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in - let new_infos = - {dyn_infos with - info = new_body; - eq_hyps = heq_id::dyn_infos.eq_hyps - } - in - clean_goal_with_heq ptes_infos continue_tac new_infos g' - )]) + pf_unsafe_type_of g' term, + Termops.replace_term (project g') term (mkRel 1) dyn_infos.info + ) + in + let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in + let new_infos = + {dyn_infos with + info = new_body; + eq_hyps = heq_id::dyn_infos.eq_hyps + } + in + clean_goal_with_heq ptes_infos continue_tac new_infos g' + )]) ] g @@ -638,29 +638,29 @@ let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = let instantiate_one_hyp hid = my_orelse ( (* we instantiate the hyp if possible *) - fun g -> - let prov_hid = pf_get_new_id hid g in - let c = mkApp(mkVar hid,args) in - let evm, _ = pf_apply Typing.type_of g c in - tclTHENLIST[ + fun g -> + let prov_hid = pf_get_new_id hid g in + let c = mkApp(mkVar hid,args) in + let evm, _ = pf_apply Typing.type_of g c in + tclTHENLIST[ Refiner.tclEVARS evm; - Proofview.V82.of_tactic (pose_proof (Name prov_hid) c); - thin [hid]; - Proofview.V82.of_tactic (rename_hyp [prov_hid,hid]) - ] g + Proofview.V82.of_tactic (pose_proof (Name prov_hid) c); + thin [hid]; + Proofview.V82.of_tactic (rename_hyp [prov_hid,hid]) + ] g ) ( (* - if not then we are in a mutual function block - and this hyp is a recursive hyp on an other function. + if not then we are in a mutual function block + and this hyp is a recursive hyp on an other function. - We are not supposed to use it while proving this - principle so that we can trash it + We are not supposed to use it while proving this + principle so that we can trash it - *) - (fun g -> -(* observe (str "Instantiation: removing hyp " ++ Ppconstr.pr_id hid); *) - thin [hid] g - ) + *) + (fun g -> +(* observe (str "Instantiation: removing hyp " ++ Ppconstr.pr_id hid); *) + thin [hid] g + ) ) in if List.is_empty args_id @@ -672,17 +672,17 @@ let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = else tclTHENLIST [ - tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps; + tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps; tclMAP instantiate_one_hyp hyps; - (fun g -> - let all_g_hyps_id = - List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty - in - let remaining_hyps = - List.filter (fun id -> Id.Set.mem id all_g_hyps_id) hyps - in - do_prove remaining_hyps g - ) + (fun g -> + let all_g_hyps_id = + List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty + in + let remaining_hyps = + List.filter (fun id -> Id.Set.mem id all_g_hyps_id) hyps + in + do_prove remaining_hyps g + ) ] let build_proof @@ -696,152 +696,152 @@ let build_proof let env = pf_env g in let sigma = project g in (* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*) - match EConstr.kind sigma dyn_infos.info with - | Case(ci,ct,t,cb) -> - let do_finalize_t dyn_info' = - fun g -> - let t = dyn_info'.info in - let dyn_infos = {dyn_info' with info = - mkCase(ci,ct,t,cb)} in - let g_nb_prod = nb_prod (project g) (pf_concl g) in - let type_of_term = pf_unsafe_type_of g t in - let term_eq = - make_refl_eq (Lazy.force refl_equal) type_of_term t - in - tclTHENLIST - [ - Proofview.V82.of_tactic (generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps))); - thin dyn_infos.rec_hyps; - Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None); - (fun g -> observe_tac "toto" ( - tclTHENLIST [Proofview.V82.of_tactic (Simple.case t); - (fun g' -> - let g'_nb_prod = nb_prod (project g') (pf_concl g') in + match EConstr.kind sigma dyn_infos.info with + | Case(ci,ct,t,cb) -> + let do_finalize_t dyn_info' = + fun g -> + let t = dyn_info'.info in + let dyn_infos = {dyn_info' with info = + mkCase(ci,ct,t,cb)} in + let g_nb_prod = nb_prod (project g) (pf_concl g) in + let type_of_term = pf_unsafe_type_of g t in + let term_eq = + make_refl_eq (Lazy.force refl_equal) type_of_term t + in + tclTHENLIST + [ + Proofview.V82.of_tactic (generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps))); + thin dyn_infos.rec_hyps; + Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None); + (fun g -> observe_tac "toto" ( + tclTHENLIST [Proofview.V82.of_tactic (Simple.case t); + (fun g' -> + let g'_nb_prod = nb_prod (project g') (pf_concl g') in let nb_instantiate_partial = g'_nb_prod - g_nb_prod in - observe_tac "treat_new_case" - (treat_new_case - ptes_infos + observe_tac "treat_new_case" + (treat_new_case + ptes_infos nb_instantiate_partial (build_proof do_finalize) - t - dyn_infos) - g' - ) - - ]) g - ) - ] - g - in + t + dyn_infos) + g' + ) + + ]) g + ) + ] + g + in build_proof do_finalize_t {dyn_infos with info = t} g | Lambda(n,t,b) -> - begin - match EConstr.kind sigma (pf_concl g) with - | Prod _ -> - tclTHEN - (Proofview.V82.of_tactic intro) - (fun g' -> + begin + match EConstr.kind sigma (pf_concl g) with + | Prod _ -> + tclTHEN + (Proofview.V82.of_tactic intro) + (fun g' -> let open Context.Named.Declaration in - let id = pf_last_hyp g' |> get_id in - let new_term = - pf_nf_betaiota g' - (mkApp(dyn_infos.info,[|mkVar id|])) - in - let new_infos = {dyn_infos with info = new_term} in - let do_prove new_hyps = + let id = pf_last_hyp g' |> get_id in + let new_term = + pf_nf_betaiota g' + (mkApp(dyn_infos.info,[|mkVar id|])) + in + let new_infos = {dyn_infos with info = new_term} in + let do_prove new_hyps = build_proof do_finalize - {new_infos with - rec_hyps = new_hyps; - nb_rec_hyps = List.length new_hyps - } - in -(* observe_tac "Lambda" *) (instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' - (* build_proof do_finalize new_infos g' *) - ) g - | _ -> - do_finalize dyn_infos g - end - | Cast(t,_,_) -> + {new_infos with + rec_hyps = new_hyps; + nb_rec_hyps = List.length new_hyps + } + in +(* observe_tac "Lambda" *) (instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' + (* build_proof do_finalize new_infos g' *) + ) g + | _ -> + do_finalize dyn_infos g + end + | Cast(t,_,_) -> build_proof do_finalize {dyn_infos with info = t} g | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ -> - do_finalize dyn_infos g - | App(_,_) -> - let f,args = decompose_app sigma dyn_infos.info in - begin - match EConstr.kind sigma f with + do_finalize dyn_infos g + | App(_,_) -> + let f,args = decompose_app sigma dyn_infos.info in + begin + match EConstr.kind sigma f with | Int _ -> user_err Pp.(str "integer cannot be applied") - | App _ -> assert false (* we have collected all the app in decompose_app *) - | Proj _ -> assert false (*FIXME*) - | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _ -> - let new_infos = - { dyn_infos with - info = (f,args) - } - in + | App _ -> assert false (* we have collected all the app in decompose_app *) + | Proj _ -> assert false (*FIXME*) + | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _ -> + let new_infos = + { dyn_infos with + info = (f,args) + } + in build_proof_args env sigma do_finalize new_infos g - | Const (c,_) when not (List.mem_f Constant.equal c fnames) -> - let new_infos = - { dyn_infos with - info = (f,args) - } - in -(* Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *) + | Const (c,_) when not (List.mem_f Constant.equal c fnames) -> + let new_infos = + { dyn_infos with + info = (f,args) + } + in +(* Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *) build_proof_args env sigma do_finalize new_infos g - | Const _ -> - do_finalize dyn_infos g - | Lambda _ -> - let new_term = + | Const _ -> + do_finalize dyn_infos g + | Lambda _ -> + let new_term = Reductionops.nf_beta env sigma dyn_infos.info in build_proof do_finalize {dyn_infos with info = new_term} - g - | LetIn _ -> - let new_infos = + g + | LetIn _ -> + let new_infos = { dyn_infos with info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info } - in - - tclTHENLIST - [tclMAP - (fun hyp_id -> - h_reduce_with_zeta (Locusops.onHyp hyp_id)) - dyn_infos.rec_hyps; - h_reduce_with_zeta Locusops.onConcl; + in + + tclTHENLIST + [tclMAP + (fun hyp_id -> + h_reduce_with_zeta (Locusops.onHyp hyp_id)) + dyn_infos.rec_hyps; + h_reduce_with_zeta Locusops.onConcl; build_proof do_finalize new_infos - ] - g - | Cast(b,_,_) -> + ] + g + | Cast(b,_,_) -> build_proof do_finalize {dyn_infos with info = b } g - | Case _ | Fix _ | CoFix _ -> - let new_finalize dyn_infos = - let new_infos = - { dyn_infos with - info = dyn_infos.info,args - } - in + | Case _ | Fix _ | CoFix _ -> + let new_finalize dyn_infos = + let new_infos = + { dyn_infos with + info = dyn_infos.info,args + } + in build_proof_args env sigma do_finalize new_infos - in + in build_proof new_finalize {dyn_infos with info = f } g - end - | Fix _ | CoFix _ -> - user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet")) + end + | Fix _ | CoFix _ -> + user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet")) - | Proj _ -> user_err Pp.(str "Prod") - | Prod _ -> do_finalize dyn_infos g - | LetIn _ -> - let new_infos = - { dyn_infos with + | Proj _ -> user_err Pp.(str "Prod") + | Prod _ -> do_finalize dyn_infos g + | LetIn _ -> + let new_infos = + { dyn_infos with info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info - } - in - - tclTHENLIST - [tclMAP - (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) - dyn_infos.rec_hyps; - h_reduce_with_zeta Locusops.onConcl; + } + in + + tclTHENLIST + [tclMAP + (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) + dyn_infos.rec_hyps; + h_reduce_with_zeta Locusops.onConcl; build_proof do_finalize new_infos - ] g - | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!") + ] g + | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!") and build_proof do_finalize dyn_infos g = (* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *) observe_tac_stream (str "build_proof with " ++ pr_leconstr_env (pf_env g) (project g) dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g @@ -849,33 +849,33 @@ let build_proof fun g -> let (f_args',args) = dyn_infos.info in let tac : tactic = - fun g -> - match args with - | [] -> - do_finalize {dyn_infos with info = f_args'} g - | arg::args -> - (* observe (str "build_proof_args with arg := "++ pr_lconstr_env (pf_env g) arg++ *) - (* fnl () ++ *) - (* pr_goal (Tacmach.sig_it g) *) - (* ); *) - let do_finalize dyn_infos = - let new_arg = dyn_infos.info in - (* tclTRYD *) + fun g -> + match args with + | [] -> + do_finalize {dyn_infos with info = f_args'} g + | arg::args -> + (* observe (str "build_proof_args with arg := "++ pr_lconstr_env (pf_env g) arg++ *) + (* fnl () ++ *) + (* pr_goal (Tacmach.sig_it g) *) + (* ); *) + let do_finalize dyn_infos = + let new_arg = dyn_infos.info in + (* tclTRYD *) (build_proof_args env sigma - do_finalize - {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args} - ) - in + do_finalize + {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args} + ) + in build_proof do_finalize - {dyn_infos with info = arg } - g + {dyn_infos with info = arg } + g in (* observe_tac "build_proof_args" *) (tac ) g in let do_finish_proof dyn_infos = (* tclTRYD *) (clean_goal_with_heq - ptes_infos - finish_proof dyn_infos) + ptes_infos + finish_proof dyn_infos) in (* observe_tac "build_proof" *) fun g -> @@ -899,14 +899,14 @@ type static_fix_info = let prove_rec_hyp_for_struct fix_info = (fun eq_hyps -> tclTHEN - (rewrite_until_var (fix_info.idx) eq_hyps) - (fun g -> - let _,pte_args = destApp (project g) (pf_concl g) in - let rec_hyp_proof = - mkApp(mkVar fix_info.name,array_get_start pte_args) - in - refine rec_hyp_proof g - )) + (rewrite_until_var (fix_info.idx) eq_hyps) + (fun g -> + let _,pte_args = destApp (project g) (pf_concl g) in + let rec_hyp_proof = + mkApp(mkVar fix_info.name,array_get_start pte_args) + in + refine rec_hyp_proof g + )) let prove_rec_hyp fix_info = { proving_tac = prove_rec_hyp_for_struct fix_info @@ -926,8 +926,8 @@ let generalize_non_dep hyp g = let hyp = get_id decl in if Id.List.mem hyp hyps || List.exists (Termops.occur_var_in_decl env (project g) hyp) keep - || Termops.occur_var env (project g) hyp hyp_typ - || Termops.is_section_variable hyp (* should be dangerous *) + || Termops.occur_var env (project g) hyp hyp_typ + || Termops.is_section_variable hyp (* should be dangerous *) then (clear,decl::keep) else (hyp::clear,keep)) ~init:([],[]) (pf_env g) @@ -968,7 +968,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *) let (type_ctxt,type_of_f),evd = let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f - in + in decompose_prod_n_assum evd (nb_params + nb_args) t,evd in @@ -979,14 +979,14 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num let prove_replacement = tclTHENLIST [ - tclDO (nb_params + rec_args_num + 1) (Proofview.V82.of_tactic intro); - observe_tac "" (fun g -> - let rec_id = pf_nth_hyp_id g 1 in - tclTHENLIST - [observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id); - observe_tac "h_case" (Proofview.V82.of_tactic (simplest_case (mkVar rec_id))); - (Proofview.V82.of_tactic intros_reflexivity)] g - ) + tclDO (nb_params + rec_args_num + 1) (Proofview.V82.of_tactic intro); + observe_tac "" (fun g -> + let rec_id = pf_nth_hyp_id g 1 in + tclTHENLIST + [observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id); + observe_tac "h_case" (Proofview.V82.of_tactic (simplest_case (mkVar rec_id))); + (Proofview.V82.of_tactic intros_reflexivity)] g + ) ] in (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *) @@ -1011,28 +1011,28 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a with (Not_found | Option.IsNone as e) -> let f_id = Label.to_id (Constant.label (fst (destConst !evd f))) in (*i The next call to mk_equation_id is valid since we will construct the lemma - Ensures by: obvious - i*) + Ensures by: obvious + i*) let equation_lemma_id = (mk_equation_id f_id) in evd := generate_equation_lemma !evd all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num; let _ = - match e with - | Option.IsNone -> - let finfos = find_Function_infos (fst (destConst !evd f)) in - update_Function - {finfos with - equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with - ConstRef c -> c - | _ -> CErrors.anomaly (Pp.str "Not a constant.") - ) - } - | _ -> () + match e with + | Option.IsNone -> + let finfos = find_Function_infos (fst (destConst !evd f)) in + update_Function + {finfos with + equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with + ConstRef c -> c + | _ -> CErrors.anomaly (Pp.str "Not a constant.") + ) + } + | _ -> () in (* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *) let evd',res = - Evd.fresh_global - (Global.env ()) !evd - (Constrintern.locate_reference (qualid_of_ident equation_lemma_id)) + Evd.fresh_global + (Global.env ()) !evd + (Constrintern.locate_reference (qualid_of_ident equation_lemma_id)) in evd:=evd'; let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd res in @@ -1043,12 +1043,12 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a tclTHEN (tclDO nb_intro_to_do (Proofview.V82.of_tactic intro)) ( - fun g' -> - let just_introduced = nLastDecls nb_intro_to_do g' in + fun g' -> + let just_introduced = nLastDecls nb_intro_to_do g' in let open Context.Named.Declaration in - let just_introduced_id = List.map get_id just_introduced in - tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma)) - (revert just_introduced_id) g' + let just_introduced_id = List.map get_id just_introduced in + tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma)) + (revert just_introduced_id) g' ) g @@ -1062,35 +1062,35 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let fresh_id = let avoid = ref (pf_ids_of_hyps g) in (fun na -> - let new_id = - match na with - Name id -> fresh_id !avoid (Id.to_string id) - | Anonymous -> fresh_id !avoid "H" - in - avoid := new_id :: !avoid; - (Name new_id) + let new_id = + match na with + Name id -> fresh_id !avoid (Id.to_string id) + | Anonymous -> fresh_id !avoid "H" + in + avoid := new_id :: !avoid; + (Name new_id) ) in let fresh_decl = RelDecl.map_name fresh_id in let princ_info : elim_scheme = { princ_info with - params = List.map fresh_decl princ_info.params; - predicates = List.map fresh_decl princ_info.predicates; - branches = List.map fresh_decl princ_info.branches; - args = List.map fresh_decl princ_info.args + params = List.map fresh_decl princ_info.params; + predicates = List.map fresh_decl princ_info.predicates; + branches = List.map fresh_decl princ_info.branches; + args = List.map fresh_decl princ_info.args } in let get_body const = match Global.body_of_constant Library.indirect_accessor const with - | Some (body, _) -> + | Some (body, _) -> let env = Global.env () in let sigma = Evd.from_env env in - Tacred.cbv_norm_flags - (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) + Tacred.cbv_norm_flags + (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) env sigma - (EConstr.of_constr body) - | None -> user_err Pp.(str "Cannot define a principle over an axiom ") + (EConstr.of_constr body) + | None -> user_err Pp.(str "Cannot define a principle over an axiom ") in let fbody = get_body fnames.(fun_num) in let f_ctxt,f_body = decompose_lam (project g) fbody in @@ -1099,37 +1099,37 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let full_params,princ_params,fbody_with_full_params = if diff_params > 0 then - let princ_params,full_params = - list_chop diff_params princ_info.params - in - (full_params, (* real params *) - princ_params, (* the params of the principle which are not params of the function *) + let princ_params,full_params = + list_chop diff_params princ_info.params + in + (full_params, (* real params *) + princ_params, (* the params of the principle which are not params of the function *) substl (* function instantiated with real params *) - (List.map var_of_decl full_params) - f_body - ) + (List.map var_of_decl full_params) + f_body + ) else - let f_ctxt_other,f_ctxt_params = - list_chop (- diff_params) f_ctxt in - let f_body = compose_lam f_ctxt_other f_body in - (princ_info.params, (* real params *) - [],(* all params are full params *) + let f_ctxt_other,f_ctxt_params = + list_chop (- diff_params) f_ctxt in + let f_body = compose_lam f_ctxt_other f_body in + (princ_info.params, (* real params *) + [],(* all params are full params *) substl (* function instantiated with real params *) - (List.map var_of_decl princ_info.params) - f_body - ) + (List.map var_of_decl princ_info.params) + f_body + ) in observe (str "full_params := " ++ - prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id) - full_params - ); + prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id) + full_params + ); observe (str "princ_params := " ++ - prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id) - princ_params - ); + prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id) + princ_params + ); observe (str "fbody_with_full_params := " ++ pr_leconstr_env (Global.env ()) !evd fbody_with_full_params - ); + ); let all_funs_with_full_params = Array.map (fun f -> applist(f, List.rev_map var_of_decl full_params)) all_funs in @@ -1137,232 +1137,232 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let ptes_to_fix,infos = match EConstr.kind (project g) fbody_with_full_params with | Fix((idxs,i),(names,typess,bodies)) -> - let bodies_with_all_params = - Array.map - (fun body -> + let bodies_with_all_params = + Array.map + (fun body -> Reductionops.nf_betaiota (pf_env g) (project g) - (applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body, - List.rev_map var_of_decl princ_params)) - ) - bodies - in - let info_array = - Array.mapi - (fun i types -> - let types = prod_applist (project g) types (List.rev_map var_of_decl princ_params) in - { idx = idxs.(i) - fix_offset; + (applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body, + List.rev_map var_of_decl princ_params)) + ) + bodies + in + let info_array = + Array.mapi + (fun i types -> + let types = prod_applist (project g) types (List.rev_map var_of_decl princ_params) in + { idx = idxs.(i) - fix_offset; name = Nameops.Name.get_id (fresh_id names.(i).binder_name); - types = types; - offset = fix_offset; - nb_realargs = - List.length - (fst (decompose_lam (project g) bodies.(i))) - fix_offset; - body_with_param = bodies_with_all_params.(i); - num_in_block = i - } - ) - typess - in - let pte_to_fix,rev_info = - List.fold_left_i - (fun i (acc_map,acc_info) decl -> - let pte = RelDecl.get_name decl in - let infos = info_array.(i) in - let type_args,_ = decompose_prod (project g) infos.types in - let nargs = List.length type_args in - let f = applist(mkConst fnames.(i), List.rev_map var_of_decl princ_info.params) in - let first_args = Array.init nargs (fun i -> mkRel (nargs -i)) in - let app_f = mkApp(f,first_args) in - let pte_args = (Array.to_list first_args)@[app_f] in - let app_pte = applist(mkVar (Nameops.Name.get_id pte),pte_args) in - let body_with_param,num = - let body = get_body fnames.(i) in - let body_with_full_params = + types = types; + offset = fix_offset; + nb_realargs = + List.length + (fst (decompose_lam (project g) bodies.(i))) - fix_offset; + body_with_param = bodies_with_all_params.(i); + num_in_block = i + } + ) + typess + in + let pte_to_fix,rev_info = + List.fold_left_i + (fun i (acc_map,acc_info) decl -> + let pte = RelDecl.get_name decl in + let infos = info_array.(i) in + let type_args,_ = decompose_prod (project g) infos.types in + let nargs = List.length type_args in + let f = applist(mkConst fnames.(i), List.rev_map var_of_decl princ_info.params) in + let first_args = Array.init nargs (fun i -> mkRel (nargs -i)) in + let app_f = mkApp(f,first_args) in + let pte_args = (Array.to_list first_args)@[app_f] in + let app_pte = applist(mkVar (Nameops.Name.get_id pte),pte_args) in + let body_with_param,num = + let body = get_body fnames.(i) in + let body_with_full_params = Reductionops.nf_betaiota (pf_env g) (project g) ( - applist(body,List.rev_map var_of_decl full_params)) - in - match EConstr.kind (project g) body_with_full_params with + applist(body,List.rev_map var_of_decl full_params)) + in + match EConstr.kind (project g) body_with_full_params with | Fix((_,num),(_,_,bs)) -> Reductionops.nf_betaiota (pf_env g) (project g) ( - (applist - (substl - (List.rev - (Array.to_list all_funs_with_full_params)) - bs.(num), - List.rev_map var_of_decl princ_params)) - ),num - | _ -> user_err Pp.(str "Not a mutual block") - in - let info = - {infos with - types = compose_prod type_args app_pte; - body_with_param = body_with_param; - num_in_block = num - } - in -(* observe (str "binding " ++ Ppconstr.pr_id (Nameops.Name.get_id pte) ++ *) -(* str " to " ++ Ppconstr.pr_id info.name); *) - (Id.Map.add (Nameops.Name.get_id pte) info acc_map,info::acc_info) - ) - 0 - (Id.Map.empty,[]) - (List.rev princ_info.predicates) - in - pte_to_fix,List.rev rev_info - | _ -> - Id.Map.empty,[] + (applist + (substl + (List.rev + (Array.to_list all_funs_with_full_params)) + bs.(num), + List.rev_map var_of_decl princ_params)) + ),num + | _ -> user_err Pp.(str "Not a mutual block") + in + let info = + {infos with + types = compose_prod type_args app_pte; + body_with_param = body_with_param; + num_in_block = num + } + in +(* observe (str "binding " ++ Ppconstr.pr_id (Nameops.Name.get_id pte) ++ *) +(* str " to " ++ Ppconstr.pr_id info.name); *) + (Id.Map.add (Nameops.Name.get_id pte) info acc_map,info::acc_info) + ) + 0 + (Id.Map.empty,[]) + (List.rev princ_info.predicates) + in + pte_to_fix,List.rev rev_info + | _ -> + Id.Map.empty,[] in let mk_fixes : tactic = let pre_info,infos = list_chop fun_num infos in match pre_info,infos with - | _,[] -> tclIDTAC - | _, this_fix_info::others_infos -> - let other_fix_infos = - List.map - (fun fi -> fi.name,fi.idx + 1 ,fi.types) - (pre_info@others_infos) - in - if List.is_empty other_fix_infos - then - if this_fix_info.idx + 1 = 0 - then tclIDTAC (* Someone tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *) - else + | _,[] -> tclIDTAC + | _, this_fix_info::others_infos -> + let other_fix_infos = + List.map + (fun fi -> fi.name,fi.idx + 1 ,fi.types) + (pre_info@others_infos) + in + if List.is_empty other_fix_infos + then + if this_fix_info.idx + 1 = 0 + then tclIDTAC (* Someone tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *) + else observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix this_fix_info.name (this_fix_info.idx +1))) - else - Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1) - other_fix_infos 0) + else + Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1) + other_fix_infos 0) in let first_tac : tactic = (* every operations until fix creations *) tclTHENLIST - [ observe_tac "introducing params" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.params))); - observe_tac "introducing predictes" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.predicates))); - observe_tac "introducing branches" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.branches))); - observe_tac "building fixes" mk_fixes; - ] + [ observe_tac "introducing params" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.params))); + observe_tac "introducing predictes" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.predicates))); + observe_tac "introducing branches" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.branches))); + observe_tac "building fixes" mk_fixes; + ] in let intros_after_fixes : tactic = fun gl -> - let ctxt,pte_app = (decompose_prod_assum (project gl) (pf_concl gl)) in - let pte,pte_args = (decompose_app (project gl) pte_app) in - try - let pte = + let ctxt,pte_app = (decompose_prod_assum (project gl) (pf_concl gl)) in + let pte,pte_args = (decompose_app (project gl) pte_app) in + try + let pte = try destVar (project gl) pte with DestKO -> anomaly (Pp.str "Property is not a variable.") in - let fix_info = Id.Map.find pte ptes_to_fix in - let nb_args = fix_info.nb_realargs in - tclTHENLIST - [ - (* observe_tac ("introducing args") *) (tclDO nb_args (Proofview.V82.of_tactic intro)); - (fun g -> (* replacement of the function by its body *) - let args = nLastDecls nb_args g in - let fix_body = fix_info.body_with_param in -(* observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *) + let fix_info = Id.Map.find pte ptes_to_fix in + let nb_args = fix_info.nb_realargs in + tclTHENLIST + [ + (* observe_tac ("introducing args") *) (tclDO nb_args (Proofview.V82.of_tactic intro)); + (fun g -> (* replacement of the function by its body *) + let args = nLastDecls nb_args g in + let fix_body = fix_info.body_with_param in +(* observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *) let open Context.Named.Declaration in - let args_id = List.map get_id args in - let dyn_infos = - { - nb_rec_hyps = -100; - rec_hyps = []; - info = + let args_id = List.map get_id args in + let dyn_infos = + { + nb_rec_hyps = -100; + rec_hyps = []; + info = Reductionops.nf_betaiota (pf_env g) (project g) - (applist(fix_body,List.rev_map mkVar args_id)); - eq_hyps = [] - } - in - tclTHENLIST - [ - observe_tac "do_replace" - (do_replace evd - full_params - (fix_info.idx + List.length princ_params) - (args_id@(List.map (RelDecl.get_name %> Nameops.Name.get_id) princ_params)) - (all_funs.(fix_info.num_in_block)) - fix_info.num_in_block - all_funs - ); - let do_prove = - build_proof - interactive_proof - (Array.to_list fnames) - (Id.Map.map prove_rec_hyp ptes_to_fix) - in - let prove_tac branches = - let dyn_infos = - {dyn_infos with - rec_hyps = branches; - nb_rec_hyps = List.length branches - } - in - observe_tac "cleaning" (clean_goal_with_heq - (Id.Map.map prove_rec_hyp ptes_to_fix) - do_prove - dyn_infos) - in -(* observe (str "branches := " ++ *) -(* prlist_with_sep spc (fun decl -> Ppconstr.pr_id (id_of_decl decl)) princ_info.branches ++ fnl () ++ *) -(* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *) - -(* ); *) + (applist(fix_body,List.rev_map mkVar args_id)); + eq_hyps = [] + } + in + tclTHENLIST + [ + observe_tac "do_replace" + (do_replace evd + full_params + (fix_info.idx + List.length princ_params) + (args_id@(List.map (RelDecl.get_name %> Nameops.Name.get_id) princ_params)) + (all_funs.(fix_info.num_in_block)) + fix_info.num_in_block + all_funs + ); + let do_prove = + build_proof + interactive_proof + (Array.to_list fnames) + (Id.Map.map prove_rec_hyp ptes_to_fix) + in + let prove_tac branches = + let dyn_infos = + {dyn_infos with + rec_hyps = branches; + nb_rec_hyps = List.length branches + } + in + observe_tac "cleaning" (clean_goal_with_heq + (Id.Map.map prove_rec_hyp ptes_to_fix) + do_prove + dyn_infos) + in +(* observe (str "branches := " ++ *) +(* prlist_with_sep spc (fun decl -> Ppconstr.pr_id (id_of_decl decl)) princ_info.branches ++ fnl () ++ *) +(* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *) + +(* ); *) (* observe_tac "instancing" *) (instantiate_hyps_with_args prove_tac - (List.rev_map id_of_decl princ_info.branches) - (List.rev args_id)) - ] - g - ); - ] gl - with Not_found -> - let nb_args = min (princ_info.nargs) (List.length ctxt) in - tclTHENLIST - [ - tclDO nb_args (Proofview.V82.of_tactic intro); - (fun g -> (* replacement of the function by its body *) - let args = nLastDecls nb_args g in + (List.rev_map id_of_decl princ_info.branches) + (List.rev args_id)) + ] + g + ); + ] gl + with Not_found -> + let nb_args = min (princ_info.nargs) (List.length ctxt) in + tclTHENLIST + [ + tclDO nb_args (Proofview.V82.of_tactic intro); + (fun g -> (* replacement of the function by its body *) + let args = nLastDecls nb_args g in let open Context.Named.Declaration in - let args_id = List.map get_id args in - let dyn_infos = - { - nb_rec_hyps = -100; - rec_hyps = []; - info = + let args_id = List.map get_id args in + let dyn_infos = + { + nb_rec_hyps = -100; + rec_hyps = []; + info = Reductionops.nf_betaiota (pf_env g) (project g) - (applist(fbody_with_full_params, - (List.rev_map var_of_decl princ_params)@ - (List.rev_map mkVar args_id) - )); - eq_hyps = [] - } - in - let fname = destConst (project g) (fst (decompose_app (project g) (List.hd (List.rev pte_args)))) in - tclTHENLIST - [Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]); - let do_prove = - build_proof - interactive_proof - (Array.to_list fnames) - (Id.Map.map prove_rec_hyp ptes_to_fix) - in - let prove_tac branches = - let dyn_infos = - {dyn_infos with - rec_hyps = branches; - nb_rec_hyps = List.length branches - } - in - clean_goal_with_heq - (Id.Map.map prove_rec_hyp ptes_to_fix) - do_prove - dyn_infos - in + (applist(fbody_with_full_params, + (List.rev_map var_of_decl princ_params)@ + (List.rev_map mkVar args_id) + )); + eq_hyps = [] + } + in + let fname = destConst (project g) (fst (decompose_app (project g) (List.hd (List.rev pte_args)))) in + tclTHENLIST + [Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]); + let do_prove = + build_proof + interactive_proof + (Array.to_list fnames) + (Id.Map.map prove_rec_hyp ptes_to_fix) + in + let prove_tac branches = + let dyn_infos = + {dyn_infos with + rec_hyps = branches; + nb_rec_hyps = List.length branches + } + in + clean_goal_with_heq + (Id.Map.map prove_rec_hyp ptes_to_fix) + do_prove + dyn_infos + in instantiate_hyps_with_args prove_tac - (List.rev_map id_of_decl princ_info.branches) - (List.rev args_id) - ] - g - ) - ] - gl + (List.rev_map id_of_decl princ_info.branches) + (List.rev args_id) + ] + g + ) + ] + gl in tclTHEN first_tac @@ -1391,23 +1391,23 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic = match !tcc_lemma_constr with | Undefined -> anomaly (Pp.str "No tcc proof !!") | Value lemma -> - fun gls -> -(* let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *) -(* let ids = hid::pf_ids_of_hyps gls in *) - tclTHENLIST - [ -(* generalize [lemma]; *) -(* h_intro hid; *) -(* Elim.h_decompose_and (mkVar hid); *) - tclTRY(list_rewrite true eqs); -(* (fun g -> *) -(* let ids' = pf_ids_of_hyps g in *) -(* let ids = List.filter (fun id -> not (List.mem id ids)) ids' in *) -(* rewrite *) -(* ) *) - Proofview.V82.of_tactic (Eauto.gen_eauto (false,5) [] (Some [])) - ] - gls + fun gls -> +(* let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *) +(* let ids = hid::pf_ids_of_hyps gls in *) + tclTHENLIST + [ +(* generalize [lemma]; *) +(* h_intro hid; *) +(* Elim.h_decompose_and (mkVar hid); *) + tclTRY(list_rewrite true eqs); +(* (fun g -> *) +(* let ids' = pf_ids_of_hyps g in *) +(* let ids = List.filter (fun id -> not (List.mem id ids)) ids' in *) +(* rewrite *) +(* ) *) + Proofview.V82.of_tactic (Eauto.gen_eauto (false,5) [] (Some [])) + ] + gls | Not_needed -> tclIDTAC let backtrack_eqs_until_hrec hrec eqs : tactic = @@ -1421,10 +1421,10 @@ let backtrack_eqs_until_hrec hrec eqs : tactic = let f = (fst (destApp (project gls) f_app)) in let rec backtrack : tactic = fun g -> - let f_app = Array.last (snd (destApp (project g) (pf_concl g))) in - match EConstr.kind (project g) f_app with - | App(f',_) when eq_constr (project g) f' f -> tclIDTAC g - | _ -> tclTHEN rewrite backtrack g + let f_app = Array.last (snd (destApp (project g) (pf_concl g))) in + match EConstr.kind (project g) f_app with + | App(f',_) when eq_constr (project g) f' f -> tclIDTAC g + | _ -> tclTHEN rewrite backtrack g in backtrack gls @@ -1434,55 +1434,55 @@ let rec rewrite_eqs_in_eqs eqs = | [] -> tclIDTAC | eq::eqs -> - tclTHEN - (tclMAP - (fun id gl -> - observe_tac - (Format.sprintf "rewrite %s in %s " (Id.to_string eq) (Id.to_string id)) - (tclTRY (Proofview.V82.of_tactic (Equality.general_rewrite_in true Locus.AllOccurrences - true (* dep proofs also: *) true id (mkVar eq) false))) - gl - ) - eqs - ) - (rewrite_eqs_in_eqs eqs) + tclTHEN + (tclMAP + (fun id gl -> + observe_tac + (Format.sprintf "rewrite %s in %s " (Id.to_string eq) (Id.to_string id)) + (tclTRY (Proofview.V82.of_tactic (Equality.general_rewrite_in true Locus.AllOccurrences + true (* dep proofs also: *) true id (mkVar eq) false))) + gl + ) + eqs + ) + (rewrite_eqs_in_eqs eqs) let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = fun gls -> (tclTHENLIST [ - backtrack_eqs_until_hrec hrec eqs; - (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *) - (tclTHENS (* We must have exactly ONE subgoal !*) - (Proofview.V82.of_tactic (apply (mkVar hrec))) - [ tclTHENLIST - [ - (Proofview.V82.of_tactic (keep (tcc_hyps@eqs))); - (Proofview.V82.of_tactic (apply (Lazy.force acc_inv))); - (fun g -> - if is_mes - then - Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force ltof_ref))]) g - else tclIDTAC g - ); - observe_tac "rew_and_finish" - (tclTHENLIST - [tclTRY(list_rewrite false (List.map (fun v -> (mkVar v,true)) eqs)); - observe_tac "rewrite_eqs_in_eqs" (rewrite_eqs_in_eqs eqs); - (observe_tac "finishing using" - ( - tclCOMPLETE( - Eauto.eauto_with_bases - (true,5) - [(fun _ sigma -> (sigma, Lazy.force refl_equal))] + backtrack_eqs_until_hrec hrec eqs; + (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *) + (tclTHENS (* We must have exactly ONE subgoal !*) + (Proofview.V82.of_tactic (apply (mkVar hrec))) + [ tclTHENLIST + [ + (Proofview.V82.of_tactic (keep (tcc_hyps@eqs))); + (Proofview.V82.of_tactic (apply (Lazy.force acc_inv))); + (fun g -> + if is_mes + then + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force ltof_ref))]) g + else tclIDTAC g + ); + observe_tac "rew_and_finish" + (tclTHENLIST + [tclTRY(list_rewrite false (List.map (fun v -> (mkVar v,true)) eqs)); + observe_tac "rewrite_eqs_in_eqs" (rewrite_eqs_in_eqs eqs); + (observe_tac "finishing using" + ( + tclCOMPLETE( + Eauto.eauto_with_bases + (true,5) + [(fun _ sigma -> (sigma, Lazy.force refl_equal))] [Hints.Hint_db.empty TransparentState.empty false] - ) - ) - ) - ] - ) - ] - ]) + ) + ) + ) + ] + ) + ] + ]) ]) gls @@ -1502,7 +1502,7 @@ let is_valid_hypothesis sigma predicates_name = is_pte typ || match EConstr.kind sigma typ with | Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ' - | _ -> false + | _ -> false in is_valid_hypothesis @@ -1515,9 +1515,9 @@ let prove_principle_for_gen let avoid = ref (pf_ids_of_hyps gl) in fun na -> let new_id = - match na with - | Name id -> fresh_id !avoid (Id.to_string id) - | Anonymous -> fresh_id !avoid "H" + match na with + | Name id -> fresh_id !avoid (Id.to_string id) + | Anonymous -> fresh_id !avoid "H" in avoid := new_id :: !avoid; Name new_id @@ -1525,10 +1525,10 @@ let prove_principle_for_gen let fresh_decl = map_name fresh_id in let princ_info : elim_scheme = { princ_info with - params = List.map fresh_decl princ_info.params; - predicates = List.map fresh_decl princ_info.predicates; - branches = List.map fresh_decl princ_info.branches; - args = List.map fresh_decl princ_info.args + params = List.map fresh_decl princ_info.params; + predicates = List.map fresh_decl princ_info.predicates; + branches = List.map fresh_decl princ_info.branches; + args = List.map fresh_decl princ_info.args } in let wf_tac = @@ -1545,8 +1545,8 @@ let prove_principle_for_gen (* str "princ_info.nargs := " ++ int princ_info.nargs ++ fnl () ++ *) (* str "rec_arg_num := " ++ int rec_arg_num ++ fnl() ++ *) -(* str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++ *) -(* str "npost_rec_arg := " ++ int npost_rec_arg ); *) +(* str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++ *) +(* str "npost_rec_arg := " ++ int npost_rec_arg ); *) let (post_rec_arg,pre_rec_arg) = Util.List.chop npost_rec_arg princ_info.args in @@ -1569,18 +1569,18 @@ let prove_principle_for_gen let fix_id = Nameops.Name.get_id (fresh_id (Name hrec_id)) in let prove_rec_arg_acc g = ((* observe_tac "prove_rec_arg_acc" *) - (tclCOMPLETE - (tclTHEN - (Proofview.V82.of_tactic (assert_by (Name wf_thm_id) - (mkApp (delayed_force well_founded,[|input_type;relation|])) - (Proofview.V82.tactic (fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g)))) - ( - (* observe_tac *) -(* "apply wf_thm" *) - Proofview.V82.of_tactic (Tactics.Simple.apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|]))) - ) - ) - ) + (tclCOMPLETE + (tclTHEN + (Proofview.V82.of_tactic (assert_by (Name wf_thm_id) + (mkApp (delayed_force well_founded,[|input_type;relation|])) + (Proofview.V82.tactic (fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g)))) + ( + (* observe_tac *) +(* "apply wf_thm" *) + Proofview.V82.of_tactic (Tactics.Simple.apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|]))) + ) + ) + ) ) g in @@ -1605,120 +1605,120 @@ let prove_principle_for_gen let start_tac gls = let hyps = pf_ids_of_hyps gls in let hid = - next_ident_away_in_goal - (Id.of_string "prov") - (Id.Set.of_list hyps) + next_ident_away_in_goal + (Id.of_string "prov") + (Id.Set.of_list hyps) in tclTHENLIST - [ - Proofview.V82.of_tactic (generalize [lemma]); - Proofview.V82.of_tactic (Simple.intro hid); - Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid)); - (fun g -> - let new_hyps = pf_ids_of_hyps g in - tcc_list := List.rev (List.subtract Id.equal new_hyps (hid::hyps)); - if List.is_empty !tcc_list - then - begin - tcc_list := [hid]; - tclIDTAC g - end - else thin [hid] g - ) - ] - gls + [ + Proofview.V82.of_tactic (generalize [lemma]); + Proofview.V82.of_tactic (Simple.intro hid); + Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid)); + (fun g -> + let new_hyps = pf_ids_of_hyps g in + tcc_list := List.rev (List.subtract Id.equal new_hyps (hid::hyps)); + if List.is_empty !tcc_list + then + begin + tcc_list := [hid]; + tclIDTAC g + end + else thin [hid] g + ) + ] + gls in tclTHENLIST [ observe_tac "start_tac" start_tac; h_intros - (List.rev_map (get_name %> Nameops.Name.get_id) - (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params) - ); + (List.rev_map (get_name %> Nameops.Name.get_id) + (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params) + ); (* observe_tac "" *) Proofview.V82.of_tactic (assert_by - (Name acc_rec_arg_id) - (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])) - (Proofview.V82.tactic prove_rec_arg_acc) + (Name acc_rec_arg_id) + (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])) + (Proofview.V82.tactic prove_rec_arg_acc) ); (* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *) -(* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *) +(* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *) (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix fix_id (List.length args_ids + 1))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *) h_intros (List.rev (acc_rec_arg_id::args_ids)); Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref)); (* observe_tac "finish" *) (fun gl' -> - let body = - let _,args = destApp (project gl') (pf_concl gl') in - Array.last args - in - let body_info rec_hyps = - { - nb_rec_hyps = List.length rec_hyps; - rec_hyps = rec_hyps; - eq_hyps = []; - info = body - } - in - let acc_inv = - lazy ( - mkApp ( - delayed_force acc_inv_id, - [|input_type;relation;mkVar rec_arg_id|] - ) - ) - in - let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar acc_rec_arg_id|])) in - let predicates_names = - List.map (get_name %> Nameops.Name.get_id) princ_info.predicates - in - let pte_info = - { proving_tac = - (fun eqs -> -(* msgnl (str "tcc_list := "++ prlist_with_sep spc Ppconstr.pr_id !tcc_list); *) -(* msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.args)); *) -(* msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.params)); *) -(* msgnl (str "acc_rec_arg_id := "++ Ppconstr.pr_id acc_rec_arg_id); *) -(* msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id eqs); *) - - (* observe_tac "new_prove_with_tcc" *) - (new_prove_with_tcc - is_mes acc_inv fix_id - - (!tcc_list@(List.map - (get_name %> Nameops.Name.get_id) - (princ_info.args@princ_info.params) - )@ ([acc_rec_arg_id])) eqs - ) - - ); - is_valid = is_valid_hypothesis (project gl') predicates_names - } - in - let ptes_info : pte_info Id.Map.t = - List.fold_left - (fun map pte_id -> - Id.Map.add pte_id - pte_info - map - ) - Id.Map.empty - predicates_names - in - let make_proof rec_hyps = - build_proof - false - [f_ref] - ptes_info - (body_info rec_hyps) - in + let body = + let _,args = destApp (project gl') (pf_concl gl') in + Array.last args + in + let body_info rec_hyps = + { + nb_rec_hyps = List.length rec_hyps; + rec_hyps = rec_hyps; + eq_hyps = []; + info = body + } + in + let acc_inv = + lazy ( + mkApp ( + delayed_force acc_inv_id, + [|input_type;relation;mkVar rec_arg_id|] + ) + ) + in + let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar acc_rec_arg_id|])) in + let predicates_names = + List.map (get_name %> Nameops.Name.get_id) princ_info.predicates + in + let pte_info = + { proving_tac = + (fun eqs -> +(* msgnl (str "tcc_list := "++ prlist_with_sep spc Ppconstr.pr_id !tcc_list); *) +(* msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.args)); *) +(* msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.params)); *) +(* msgnl (str "acc_rec_arg_id := "++ Ppconstr.pr_id acc_rec_arg_id); *) +(* msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id eqs); *) + + (* observe_tac "new_prove_with_tcc" *) + (new_prove_with_tcc + is_mes acc_inv fix_id + + (!tcc_list@(List.map + (get_name %> Nameops.Name.get_id) + (princ_info.args@princ_info.params) + )@ ([acc_rec_arg_id])) eqs + ) + + ); + is_valid = is_valid_hypothesis (project gl') predicates_names + } + in + let ptes_info : pte_info Id.Map.t = + List.fold_left + (fun map pte_id -> + Id.Map.add pte_id + pte_info + map + ) + Id.Map.empty + predicates_names + in + let make_proof rec_hyps = + build_proof + false + [f_ref] + ptes_info + (body_info rec_hyps) + in (* observe_tac "instantiate_hyps_with_args" *) (instantiate_hyps_with_args - make_proof - (List.map (get_name %> Nameops.Name.get_id) princ_info.branches) - (List.rev args_ids) - ) - gl' + make_proof + (List.map (get_name %> Nameops.Name.get_id) princ_info.branches) + (List.rev args_ids) + ) + gl' ) ] diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 5363dc9a02..8af5dc818b 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -51,16 +51,16 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | [] -> [] | decl :: predicates -> (match Context.Rel.Declaration.get_name decl with - | Name x -> - let id = Namegen.next_ident_away x (Id.Set.of_list avoid) in - Hashtbl.add tbl id x; - RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates - | Anonymous -> anomaly (Pp.str "Anonymous property binder.")) + | Name x -> + let id = Namegen.next_ident_away x (Id.Set.of_list avoid) in + Hashtbl.add tbl id x; + RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates + | Anonymous -> anomaly (Pp.str "Anonymous property binder.")) in let avoid = (Termops.ids_of_context env_with_params ) in let princ_type_info = { princ_type_info with - predicates = change_predicates_names avoid princ_type_info.predicates + predicates = change_predicates_names avoid princ_type_info.predicates } in (* observe (str "starting princ_type := " ++ pr_lconstr_env env princ_type); *) @@ -85,28 +85,28 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let env_with_params_and_predicates = List.fold_right Environ.push_named new_predicates env_with_params in let rel_as_kn = fst (match princ_type_info.indref with - | Some (Globnames.IndRef ind) -> ind - | _ -> user_err Pp.(str "Not a valid predicate") - ) + | Some (Globnames.IndRef ind) -> ind + | _ -> user_err Pp.(str "Not a valid predicate") + ) in let ptes_vars = List.map Context.Named.Declaration.get_id new_predicates in let is_pte = let set = List.fold_right Id.Set.add ptes_vars Id.Set.empty in fun t -> match Constr.kind t with - | Var id -> Id.Set.mem id set - | _ -> false + | Var id -> Id.Set.mem id set + | _ -> false in let pre_princ = let open EConstr in it_mkProd_or_LetIn (it_mkProd_or_LetIn - (Option.fold_right - mkProd_or_LetIn - princ_type_info.indarg - princ_type_info.concl - ) - princ_type_info.args + (Option.fold_right + mkProd_or_LetIn + princ_type_info.indarg + princ_type_info.concl + ) + princ_type_info.args ) princ_type_info.branches in @@ -135,105 +135,105 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let rec compute_new_princ_type remove env pre_princ : types*(constr list) = let (new_princ_type,_) as res = match Constr.kind pre_princ with - | Rel n -> - begin - try match Environ.lookup_rel n env with + | Rel n -> + begin + try match Environ.lookup_rel n env with | LocalAssum (_,t) | LocalDef (_,_,t) when is_dom t -> raise Toberemoved - | _ -> pre_princ,[] - with Not_found -> assert false - end + | _ -> pre_princ,[] + with Not_found -> assert false + end | Prod(x,t,b) -> compute_new_princ_type_for_binder remove mkProd env x t b | Lambda(x,t,b) -> compute_new_princ_type_for_binder remove mkLambda env x t b - | Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved - | App(f,args) when is_dom f -> - let var_to_be_removed = destRel (Array.last args) in - let num = get_fun_num f in - raise (Toberemoved_with_rel (var_to_be_removed,mk_replacement pre_princ num args)) - | App(f,args) -> - let args = - if is_pte f && remove - then array_get_start args - else args - in - let new_args,binders_to_remove = - Array.fold_right (compute_new_princ_type_with_acc remove env) - args - ([],[]) - in - let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in - applistc new_f new_args, - list_union_eq Constr.equal binders_to_remove_from_f binders_to_remove + | Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved + | App(f,args) when is_dom f -> + let var_to_be_removed = destRel (Array.last args) in + let num = get_fun_num f in + raise (Toberemoved_with_rel (var_to_be_removed,mk_replacement pre_princ num args)) + | App(f,args) -> + let args = + if is_pte f && remove + then array_get_start args + else args + in + let new_args,binders_to_remove = + Array.fold_right (compute_new_princ_type_with_acc remove env) + args + ([],[]) + in + let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in + applistc new_f new_args, + list_union_eq Constr.equal binders_to_remove_from_f binders_to_remove | LetIn(x,v,t,b) -> compute_new_princ_type_for_letin remove env x v t b - | _ -> pre_princ,[] + | _ -> pre_princ,[] in (* let _ = match Constr.kind pre_princ with *) -(* | Prod _ -> *) -(* observe(str "compute_new_princ_type for "++ *) -(* pr_lconstr_env env pre_princ ++ *) -(* str" is "++ *) -(* pr_lconstr_env env new_princ_type ++ fnl ()) *) -(* | _ -> () in *) +(* | Prod _ -> *) +(* observe(str "compute_new_princ_type for "++ *) +(* pr_lconstr_env env pre_princ ++ *) +(* str" is "++ *) +(* pr_lconstr_env env new_princ_type ++ fnl ()) *) +(* | _ -> () in *) res and compute_new_princ_type_for_binder remove bind_fun env x t b = begin try - let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in + let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in let new_x = map_annot (get_name (Termops.ids_of_context env)) x in let new_env = Environ.push_rel (LocalAssum (x,t)) env in - let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in - if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b - then (pop new_b), filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b - else - ( + let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in + if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b + then (pop new_b), filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b + else + ( bind_fun(new_x,new_t,new_b), - list_union_eq - Constr.equal - binders_to_remove_from_t - (List.map pop binders_to_remove_from_b) - ) + list_union_eq + Constr.equal + binders_to_remove_from_t + (List.map pop binders_to_remove_from_b) + ) with - | Toberemoved -> -(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) - let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in - new_b, List.map pop binders_to_remove_from_b - | Toberemoved_with_rel (n,c) -> -(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) - let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in - new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b) + | Toberemoved -> +(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) + let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in + new_b, List.map pop binders_to_remove_from_b + | Toberemoved_with_rel (n,c) -> +(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) + let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in + new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b) end and compute_new_princ_type_for_letin remove env x v t b = begin try - let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in - let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in + let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in + let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in let new_x = map_annot (get_name (Termops.ids_of_context env)) x in let new_env = Environ.push_rel (LocalDef (x,v,t)) env in - let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in - if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b - then (pop new_b),filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b - else - ( + let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in + if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b + then (pop new_b),filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b + else + ( mkLetIn(new_x,new_v,new_t,new_b), - list_union_eq - Constr.equal - (list_union_eq Constr.equal binders_to_remove_from_t binders_to_remove_from_v) - (List.map pop binders_to_remove_from_b) - ) + list_union_eq + Constr.equal + (list_union_eq Constr.equal binders_to_remove_from_t binders_to_remove_from_v) + (List.map pop binders_to_remove_from_b) + ) with - | Toberemoved -> -(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) - let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in - new_b, List.map pop binders_to_remove_from_b - | Toberemoved_with_rel (n,c) -> -(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) - let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in - new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b) + | Toberemoved -> +(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) + let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in + new_b, List.map pop binders_to_remove_from_b + | Toberemoved_with_rel (n,c) -> +(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) + let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in + new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b) end and compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc) = let new_e,to_remove_from_e = compute_new_princ_type remove env e @@ -256,7 +256,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = LocalAssum (map_annot (fun id -> Name.mk_name (Hashtbl.find tbl id)) id, b) | Context.Named.Declaration.LocalDef (id,t,b) -> LocalDef (map_annot (fun id -> Name.mk_name (Hashtbl.find tbl id)) id, t, b)) - new_predicates) + new_predicates) ) (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_type_info.params) @@ -281,8 +281,8 @@ let change_property_sort evd toSort princ princName = let init = let nargs = (princ_info.nparams + (List.length princ_info.predicates)) in mkApp(EConstr.Unsafe.to_constr princName_as_constr, - Array.init nargs - (fun i -> mkRel (nargs - i ))) + Array.init nargs + (fun i -> mkRel (nargs - i ))) in evd, it_mkLambda_or_LetIn (it_mkLambda_or_LetIn init @@ -319,10 +319,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in let lemma,_ = Lemmas.by (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)) lemma in (* let _tim2 = System.get_time () in *) - (* begin *) - (* let dur1 = System.time_difference tim1 tim2 in *) - (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) - (* end; *) + (* begin *) + (* let dur1 = System.time_difference tim1 tim2 in *) + (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) + (* end; *) let open Proof_global in let { id; entries; persistence } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in @@ -350,8 +350,8 @@ let generate_functional_principle (evd: Evd.evar_map ref) match new_princ_name with | Some (id) -> id,id | None -> - let id_of_f = Label.to_id (Constant.label (fst f)) in - id_of_f,Indrec.make_elimination_ident id_of_f (Sorts.family type_sort) + let id_of_f = Label.to_id (Constant.label (fst f)) in + id_of_f,Indrec.make_elimination_ident id_of_f (Sorts.family type_sort) in let names = ref [new_princ_name] in let hook = @@ -369,13 +369,13 @@ let generate_functional_principle (evd: Evd.evar_map ref) let univs = Evd.univ_entry ~poly:false evd' in let ce = Declare.definition_entry ~univs value in ignore( - Declare.declare_constant - name - (DefinitionEntry ce, - Decl_kinds.IsDefinition (Decl_kinds.Scheme)) - ); - Declare.definition_message name; - names := name :: !names + Declare.declare_constant + name + (DefinitionEntry ce, + Decl_kinds.IsDefinition (Decl_kinds.Scheme)) + ); + Declare.definition_message name; + names := name :: !names in register_with_sort InProp; register_with_sort InSet @@ -398,31 +398,31 @@ let get_funs_constant mp = let get_funs_constant const e : (Names.Constant.t*int) array = match Constr.kind ((strip_lam e)) with | Fix((_,(na,_,_))) -> - Array.mapi - (fun i na -> + Array.mapi + (fun i na -> match na.binder_name with - | Name id -> + | Name id -> let const = Constant.make2 mp (Label.of_id id) in - const,i - | Anonymous -> - anomaly (Pp.str "Anonymous fix.") - ) - na + const,i + | Anonymous -> + anomaly (Pp.str "Anonymous fix.") + ) + na | _ -> [|const,0|] in function const -> let find_constant_body const = match Global.body_of_constant Library.indirect_accessor const with - | Some (body, _) -> - let body = Tacred.cbv_norm_flags - (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) - (Global.env ()) - (Evd.from_env (Global.env ())) - (EConstr.of_constr body) - in - let body = EConstr.Unsafe.to_constr body in - body - | None -> user_err Pp.(str ( "Cannot define a principle over an axiom ")) + | Some (body, _) -> + let body = Tacred.cbv_norm_flags + (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) + (Global.env ()) + (Evd.from_env (Global.env ())) + (EConstr.of_constr body) + in + let body = EConstr.Unsafe.to_constr body in + body + | None -> user_err Pp.(str ( "Cannot define a principle over an axiom ")) in let f = find_constant_body const in let l_const = get_funs_constant const f in @@ -436,34 +436,34 @@ let get_funs_constant mp = let _check_params = let first_params = List.hd l_params in List.iter - (fun params -> + (fun params -> if not (List.equal (fun (n1, c1) (n2, c2) -> eq_annot Name.equal n1 n2 && Constr.equal c1 c2) first_params params) - then user_err Pp.(str "Not a mutal recursive block") - ) - l_params + then user_err Pp.(str "Not a mutal recursive block") + ) + l_params in (* The bodies has to be very similar *) let _check_bodies = try - let extract_info is_first body = - match Constr.kind body with + let extract_info is_first body = + match Constr.kind body with | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca) - | _ -> - if is_first && Int.equal (List.length l_bodies) 1 - then raise Not_Rec - else user_err Pp.(str "Not a mutal recursive block") - in - let first_infos = extract_info true (List.hd l_bodies) in - let check body = (* Hope this is correct *) + | _ -> + if is_first && Int.equal (List.length l_bodies) 1 + then raise Not_Rec + else user_err Pp.(str "Not a mutal recursive block") + in + let first_infos = extract_info true (List.hd l_bodies) in + let check body = (* Hope this is correct *) let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) = Array.equal Int.equal ia1 ia2 && Array.equal (eq_annot Name.equal) na1 na2 && Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2 - in - if not (eq_infos first_infos (extract_info false body)) - then user_err Pp.(str "Not a mutal recursive block") - in - List.iter check l_bodies + in + if not (eq_infos first_infos (extract_info false body)) + then user_err Pp.(str "Not a mutal recursive block") + in + List.iter check l_bodies with Not_Rec -> () in l_const @@ -493,15 +493,15 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def let ind_list = List.map (fun (idx) -> - let ind = first_fun_kn,idx in - (ind,snd first_fun),true,prop_sort + let ind = first_fun_kn,idx in + (ind,snd first_fun),true,prop_sort ) funs_indexes in - let sigma, schemes = + let sigma, schemes = Indrec.build_mutual_induction_scheme env !evd ind_list in - let _ = evd := sigma in + let _ = evd := sigma in let l_schemes = List.map (EConstr.of_constr %> Typing.unsafe_type_of env sigma %> EConstr.Unsafe.to_constr) schemes in @@ -516,17 +516,17 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def (* We create the first principle by tactic *) let first_type,other_princ_types = match l_schemes with - s::l_schemes -> s,l_schemes + s::l_schemes -> s,l_schemes | _ -> anomaly (Pp.str "") in let ((_,(const,_)),_) = try build_functional_principle evd false - first_type - (Array.of_list sorts) - this_block_funs - 0 - (prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs))) + first_type + (Array.of_list sorts) + this_block_funs + 0 + (prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs))) (fun _ _ _ _ _ -> ()) with e when CErrors.noncritical e -> raise (Defining_principle e) @@ -557,49 +557,49 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def let (idxs,_),(_,ta,_ as decl) = destFix fix in let other_result = List.map (* we can now compute the other principles *) - (fun scheme_type -> - incr i; + (fun scheme_type -> + incr i; observe (Printer.pr_lconstr_env env sigma scheme_type); - let type_concl = (strip_prod_assum scheme_type) in - let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in - let f = fst (decompose_app applied_f) in - try (* we search the number of the function in the fix block (name of the function) *) - Array.iteri - (fun j t -> - let t = (strip_prod_assum t) in - let applied_g = List.hd (List.rev (snd (decompose_app t))) in - let g = fst (decompose_app applied_g) in - if Constr.equal f g - then raise (Found_type j); + let type_concl = (strip_prod_assum scheme_type) in + let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in + let f = fst (decompose_app applied_f) in + try (* we search the number of the function in the fix block (name of the function) *) + Array.iteri + (fun j t -> + let t = (strip_prod_assum t) in + let applied_g = List.hd (List.rev (snd (decompose_app t))) in + let g = fst (decompose_app applied_g) in + if Constr.equal f g + then raise (Found_type j); observe (Printer.pr_lconstr_env env sigma f ++ str " <> " ++ Printer.pr_lconstr_env env sigma g) - ) - ta; - (* If we reach this point, the two principle are not mutually recursive - We fall back to the previous method - *) + ) + ta; + (* If we reach this point, the two principle are not mutually recursive + We fall back to the previous method + *) let ((_,(const,_)),_) = - build_functional_principle - evd - false - (List.nth other_princ_types (!i - 1)) - (Array.of_list sorts) - this_block_funs - !i - (prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs))) + build_functional_principle + evd + false + (List.nth other_princ_types (!i - 1)) + (Array.of_list sorts) + this_block_funs + !i + (prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs))) (fun _ _ _ _ _ -> ()) - in - const - with Found_type i -> - let princ_body = - Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt - in - {const with - const_entry_body = + in + const + with Found_type i -> + let princ_body = + Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt + in + {const with + const_entry_body = (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects)); - const_entry_type = Some scheme_type - } + const_entry_type = Some scheme_type + } ) other_fun_princ_types in @@ -608,16 +608,16 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def let build_scheme fas = let evd = (ref (Evd.from_env (Global.env ()))) in let pconstants = (List.map - (fun (_,f,sort) -> - let f_as_constant = - try - Smartlocate.global_with_alias f - with Not_found -> + (fun (_,f,sort) -> + let f_as_constant = + try + Smartlocate.global_with_alias f + with Not_found -> user_err ~hdr:"FunInd.build_scheme" (str "Cannot find " ++ Libnames.pr_qualid f) - in + in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in - let _ = evd := evd' in + let _ = evd := evd' in let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd f in evd := sigma; let c, u = @@ -627,18 +627,18 @@ let build_scheme fas = in (c, EConstr.EInstance.kind !evd u), sort ) - fas - ) in + fas + ) in let bodies_types = - make_scheme evd pconstants + make_scheme evd pconstants in List.iter2 (fun (princ_id,_,_) def_entry -> ignore - (Declare.declare_constant - princ_id - (DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); + (Declare.declare_constant + princ_id + (DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); Declare.definition_message princ_id ) fas @@ -671,10 +671,10 @@ let build_case_scheme fa = List.assoc_f Constant.equal funs this_block_funs_indexes in let (ind, sf) = - let ind = first_fun_kn,funs_indexes in - (ind,Univ.Instance.empty)(*FIXME*),prop_sort + let ind = first_fun_kn,funs_indexes in + (ind,Univ.Instance.empty)(*FIXME*),prop_sort in - let (sigma, scheme) = + let (sigma, scheme) = Indrec.build_case_analysis_scheme_default env sigma ind sf in let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in @@ -687,8 +687,8 @@ let build_case_scheme fa = let princ_name = (fun (x,_,_) -> x) fa in let _ = (* Pp.msgnl (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ - pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs - ); + pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs + ); *) generate_functional_principle (ref (Evd.from_env (Global.env ()))) @@ -701,5 +701,5 @@ let build_case_scheme fa = (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|funs|]) in () - + diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d710f4490d..ecf953bef1 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -20,7 +20,7 @@ let is_rec_info sigma scheme_info = let test_branche min acc decl = acc || ( let new_branche = - it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum sigma (RelDecl.get_type decl))) in + it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum sigma (RelDecl.get_type decl))) in let free_rels_in_br = Termops.free_rels sigma new_branche in let max = min + scheme_info.Tactics.npredicates in Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br @@ -40,57 +40,57 @@ let functional_induction with_clean c princl pat = let princ,bindings, princ_type,g' = match princl with | None -> (* No principle is given let's find the good one *) - begin - match EConstr.kind sigma f with - | Const (c',u) -> - let princ_option = - let finfo = (* we first try to find out a graph on f *) - try find_Function_infos c' - with Not_found -> - user_err (str "Cannot find induction information on "++ + begin + match EConstr.kind sigma f with + | Const (c',u) -> + let princ_option = + let finfo = (* we first try to find out a graph on f *) + try find_Function_infos c' + with Not_found -> + user_err (str "Cannot find induction information on "++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) - in + in match Tacticals.elimination_sort_of_goal g with | InSProp -> finfo.sprop_lemma - | InProp -> finfo.prop_lemma - | InSet -> finfo.rec_lemma - | InType -> finfo.rect_lemma - in - let princ,g' = (* then we get the principle *) - try - let g',princ = - Tacmach.pf_eapply (Evd.fresh_global) g (Globnames.ConstRef (Option.get princ_option )) in - princ,g' - with Option.IsNone -> - (*i If there is not default lemma defined then, - we cross our finger and try to find a lemma named f_ind - (or f_rec, f_rect) i*) - let princ_name = - Indrec.make_elimination_ident - (Label.to_id (Constant.label c')) - (Tacticals.elimination_sort_of_goal g) - in - try - let princ_ref = const_of_id princ_name in - let (a,b) = Tacmach.pf_eapply (Evd.fresh_global) g princ_ref in - (b,a) - (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *) - with Not_found -> (* This one is neither defined ! *) - user_err (str "Cannot find induction principle for " + | InProp -> finfo.prop_lemma + | InSet -> finfo.rec_lemma + | InType -> finfo.rect_lemma + in + let princ,g' = (* then we get the principle *) + try + let g',princ = + Tacmach.pf_eapply (Evd.fresh_global) g (Globnames.ConstRef (Option.get princ_option )) in + princ,g' + with Option.IsNone -> + (*i If there is not default lemma defined then, + we cross our finger and try to find a lemma named f_ind + (or f_rec, f_rect) i*) + let princ_name = + Indrec.make_elimination_ident + (Label.to_id (Constant.label c')) + (Tacticals.elimination_sort_of_goal g) + in + try + let princ_ref = const_of_id princ_name in + let (a,b) = Tacmach.pf_eapply (Evd.fresh_global) g princ_ref in + (b,a) + (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *) + with Not_found -> (* This one is neither defined ! *) + user_err (str "Cannot find induction principle for " ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) - in + in (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g') - | _ -> raise (UserError(None,str "functional induction must be used with a function" )) - end + | _ -> raise (UserError(None,str "functional induction must be used with a function" )) + end | Some ((princ,binding)) -> - princ,binding,Tacmach.pf_unsafe_type_of g princ,g + princ,binding,Tacmach.pf_unsafe_type_of g princ,g in let sigma = Tacmach.project g' in let princ_infos = Tactics.compute_elim_sig (Tacmach.project g') princ_type in let args_as_induction_constr = let c_list = - if princ_infos.Tactics.farg_in_concl - then [c] else [] + if princ_infos.Tactics.farg_in_concl + then [c] else [] in if List.length args + List.length c_list = 0 then user_err Pp.(str "Cannot recognize a valid functional scheme" ); @@ -109,35 +109,35 @@ let functional_induction with_clean c princl pat = let princ' = Some (princ,bindings) in let princ_vars = List.fold_right - (fun a acc -> try Id.Set.add (destVar sigma a) acc with DestKO -> acc) - args - Id.Set.empty + (fun a acc -> try Id.Set.add (destVar sigma a) acc with DestKO -> acc) + args + Id.Set.empty in let old_idl = List.fold_right Id.Set.add (Tacmach.pf_ids_of_hyps g) Id.Set.empty in let old_idl = Id.Set.diff old_idl princ_vars in let subst_and_reduce g = if with_clean then - let idl = - List.filter (fun id -> not (Id.Set.mem id old_idl)) - (Tacmach.pf_ids_of_hyps g) - in - let flag = - Genredexpr.Cbv - {Redops.all_flags - with Genredexpr.rDelta = false; - } - in - Tacticals.tclTHEN - (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Proofview.V82.of_tactic (Equality.subst_gen (do_rewrite_dependent ()) [id]))) idl ) - (Proofview.V82.of_tactic (Tactics.reduce flag Locusops.allHypsAndConcl)) - g + let idl = + List.filter (fun id -> not (Id.Set.mem id old_idl)) + (Tacmach.pf_ids_of_hyps g) + in + let flag = + Genredexpr.Cbv + {Redops.all_flags + with Genredexpr.rDelta = false; + } + in + Tacticals.tclTHEN + (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Proofview.V82.of_tactic (Equality.subst_gen (do_rewrite_dependent ()) [id]))) idl ) + (Proofview.V82.of_tactic (Tactics.reduce flag Locusops.allHypsAndConcl)) + g else Tacticals.tclIDTAC g in Tacticals.tclTHEN (Proofview.V82.of_tactic (choose_dest_or_ind - princ_infos - (args_as_induction_constr,princ'))) + princ_infos + (args_as_induction_constr,princ'))) subst_and_reduce g' in res @@ -185,13 +185,13 @@ let build_newrecursive in recdef,rec_impls -let build_newrecursive l = - let l' = List.map - (fun ((fixna,_,bll,ar,body_opt),lnot) -> - match body_opt with - | Some body -> - (fixna,bll,ar,body) - | None -> user_err ~hdr:"Function" (str "Body of Function must be given") +let build_newrecursive l = + let l' = List.map + (fun ((fixna,_,bll,ar,body_opt),lnot) -> + match body_opt with + | Some body -> + (fixna,bll,ar,body) + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") ) l in build_newrecursive l' @@ -208,23 +208,23 @@ let is_rec names = | GCast(b,_) -> lookup names b | GRec _ -> error "GRec not handled" | GIf(b,_,lhs,rhs) -> - (lookup names b) || (lookup names lhs) || (lookup names rhs) + (lookup names b) || (lookup names lhs) || (lookup names rhs) | GProd(na,_,t,b) | GLambda(na,_,t,b) -> - lookup names t || lookup (Nameops.Name.fold_right Id.Set.remove na names) b + lookup names t || lookup (Nameops.Name.fold_right Id.Set.remove na names) b | GLetIn(na,b,t,c) -> - lookup names b || Option.cata (lookup names) true t || lookup (Nameops.Name.fold_right Id.Set.remove na names) c + lookup names b || Option.cata (lookup names) true t || lookup (Nameops.Name.fold_right Id.Set.remove na names) c | GLetTuple(nal,_,t,b) -> lookup names t || - lookup - (List.fold_left - (fun acc na -> Nameops.Name.fold_right Id.Set.remove na acc) - names - nal - ) - b + lookup + (List.fold_left + (fun acc na -> Nameops.Name.fold_right Id.Set.remove na acc) + names + nal + ) + b | GApp(f,args) -> List.exists (lookup names) (f::args) | GCases(_,_,el,brl) -> - List.exists (fun (e,_) -> lookup names e) el || - List.exists (lookup_br names) brl + List.exists (fun (e,_) -> lookup names e) el || + List.exists (lookup_br names) brl and lookup_br names {CAst.v=(idl,_,rt)} = let new_names = List.fold_right Id.Set.remove idl names in lookup new_names rt @@ -254,19 +254,19 @@ let warn_funind_cannot_build_inversion = let derive_inversion fix_names = try - let evd' = Evd.from_env (Global.env ()) in + let evd' = Evd.from_env (Global.env ()) in (* we first transform the fix_names identifier into their corresponding constant *) let evd',fix_names_as_constant = List.fold_right - (fun id (evd,l) -> - let evd,c = - Evd.fresh_global - (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident id)) in + (fun id (evd,l) -> + let evd,c = + Evd.fresh_global + (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident id)) in let (cst, u) = destConst evd c in - evd, (cst, EInstance.kind evd u) :: l - ) - fix_names - (evd',[]) + evd, (cst, EInstance.kind evd u) :: l + ) + fix_names + (evd',[]) in (* Then we check that the graphs have been defined @@ -276,22 +276,22 @@ let derive_inversion fix_names = List.iter (fun c -> ignore (find_Function_infos (fst c))) fix_names_as_constant ; try let evd', lind = - List.fold_right - (fun id (evd,l) -> - let evd,id = - Evd.fresh_global - (Global.env ()) evd - (Constrintern.locate_reference (Libnames.qualid_of_ident (mk_rel_id id))) - in + List.fold_right + (fun id (evd,l) -> + let evd,id = + Evd.fresh_global + (Global.env ()) evd + (Constrintern.locate_reference (Libnames.qualid_of_ident (mk_rel_id id))) + in evd,(fst (destInd evd id))::l - ) - fix_names - (evd',[]) + ) + fix_names + (evd',[]) in Invfun.derive_correctness - Functional_principles_types.make_scheme - fix_names_as_constant - lind; + Functional_principles_types.make_scheme + fix_names_as_constant + lind; with e when CErrors.noncritical e -> let e' = process_vernac_interp_error e in warn_funind_cannot_build_inversion e' @@ -313,15 +313,15 @@ let warning_error names e = let e = process_vernac_interp_error e in let e_explain e = match e with - | ToShow e -> - let e = process_vernac_interp_error e in - spc () ++ CErrors.print e - | _ -> - if do_observe () - then - let e = process_vernac_interp_error e in - (spc () ++ CErrors.print e) - else mt () + | ToShow e -> + let e = process_vernac_interp_error e in + spc () ++ CErrors.print e + | _ -> + if do_observe () + then + let e = process_vernac_interp_error e in + (spc () ++ CErrors.print e) + else mt () in match e with | Building_graph e -> @@ -341,10 +341,10 @@ let error_error names e = in match e with | Building_graph e -> - user_err - (str "Cannot define graph(s) for " ++ - h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ - e_explain e) + user_err + (str "Cannot define graph(s) for " ++ + h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ + e_explain e) | _ -> raise e let generate_principle (evd:Evd.evar_map ref) pconstants on_error @@ -361,51 +361,51 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error if do_built then begin - (*i The next call to mk_rel_id is valid since we have just construct the graph - Ensures by : do_built - i*) + (*i The next call to mk_rel_id is valid since we have just construct the graph + Ensures by : do_built + i*) let f_R_mut = qualid_of_ident @@ mk_rel_id (List.nth names 0) in - let ind_kn = - fst (locate_with_msg + let ind_kn = + fst (locate_with_msg (pr_qualid f_R_mut++str ": Not an inductive type!") - locate_ind - f_R_mut) - in - let fname_kn (((fname,_),_,_,_,_),_) = + locate_ind + f_R_mut) + in + let fname_kn (((fname,_),_,_,_,_),_) = let f_ref = qualid_of_ident ?loc:fname.CAst.loc fname.CAst.v in locate_with_msg (pr_qualid f_ref++str ": Not an inductive type!") - locate_constant - f_ref - in - let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in - let _ = - List.map_i - (fun i x -> + locate_constant + f_ref + in + let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in + let _ = + List.map_i + (fun i x -> let env = Global.env () in let princ = Indrec.lookup_eliminator env (ind_kn,i) (InProp) in - let evd = ref (Evd.from_env env) in - let evd',uprinc = Evd.fresh_global env !evd princ in - let _ = evd := evd' in + let evd = ref (Evd.from_env env) in + let evd',uprinc = Evd.fresh_global env !evd princ in + let _ = evd := evd' in let sigma, princ_type = Typing.type_of ~refresh:true env !evd uprinc in evd := sigma; - let princ_type = EConstr.Unsafe.to_constr princ_type in - Functional_principles_types.generate_functional_principle - evd - interactive_proof - princ_type - None - None - (Array.of_list pconstants) - (* funs_kn *) - i - (continue_proof 0 [|funs_kn.(i)|]) - ) - 0 - fix_rec_l - in - Array.iter (add_Function is_general) funs_kn; - () + let princ_type = EConstr.Unsafe.to_constr princ_type in + Functional_principles_types.generate_functional_principle + evd + interactive_proof + princ_type + None + None + (Array.of_list pconstants) + (* funs_kn *) + i + (continue_proof 0 [|funs_kn.(i)|]) + ) + 0 + fix_rec_l + in + Array.iter (add_Function is_general) funs_kn; + () end with e when CErrors.noncritical e -> on_error names e @@ -413,40 +413,40 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = match fixpoint_exprl with | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec -> - let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in ComDefinition.do_definition ~program_mode:false - fname + fname Decl_kinds.(Global ImportDefaultBehavior,false,Definition) pl bl None body (Some ret_type); let evd,rev_pconstants = - List.fold_left + List.fold_left (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> - let evd,c = - Evd.fresh_global - (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in + let evd,c = + Evd.fresh_global + (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in let (cst, u) = destConst evd c in let u = EInstance.kind evd u in evd,((cst, u) :: l) - ) - (Evd.from_env (Global.env ()),[]) - fixpoint_exprl + ) + (Evd.from_env (Global.env ()),[]) + fixpoint_exprl in None, evd,List.rev rev_pconstants | _ -> ComFixpoint.do_fixpoint (Global ImportDefaultBehavior) false fixpoint_exprl; let evd,rev_pconstants = - List.fold_left + List.fold_left (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> - let evd,c = - Evd.fresh_global - (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in + let evd,c = + Evd.fresh_global + (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in let (cst, u) = destConst evd c in let u = EInstance.kind evd u in evd,((cst, u) :: l) - ) - (Evd.from_env (Global.env ()),[]) - fixpoint_exprl + ) + (Evd.from_env (Global.env ()),[]) + fixpoint_exprl in None,evd,List.rev rev_pconstants @@ -467,34 +467,34 @@ let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf let names = List.map CAst.(with_val (fun x -> x)) - (Constrexpr_ops.names_of_local_assums args) + (Constrexpr_ops.names_of_local_assums args) in - List.index Name.equal (Name wf_arg) names + List.index Name.equal (Name wf_arg) names in let unbounded_eq = let f_app_args = CAst.make @@ Constrexpr.CAppExpl( (None,qualid_of_ident fname,None) , - (List.map - (function + (List.map + (function | {CAst.v=Anonymous} -> assert false | {CAst.v=Name e} -> (Constrexpr_ops.mkIdentC e) - ) - (Constrexpr_ops.names_of_local_assums args) - ) - ) + ) + (Constrexpr_ops.names_of_local_assums args) + ) + ) in CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (qualid_of_string "Logic.eq")), - [(f_app_args,None);(body,None)]) + [(f_app_args,None);(body,None)]) in let eq = Constrexpr_ops.mkCProdN args unbounded_eq in let hook ((f_ref,_) as fconst) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type nb_args relation = try pre_hook [fconst] - (generate_correction_proof_wf f_ref tcc_lemma_ref is_mes - functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation - ); + (generate_correction_proof_wf f_ref tcc_lemma_ref is_mes + functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation + ); derive_inversion [fname] with e when CErrors.noncritical e -> (* No proof done *) @@ -514,124 +514,124 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w let wf_arg_type,wf_arg = match wf_arg with | None -> - begin - match args with + begin + match args with | [Constrexpr.CLocalAssum ([{CAst.v=Name x}],k,t)] -> t,x - | _ -> error "Recursive argument must be specified" - end + | _ -> error "Recursive argument must be specified" + end | Some wf_args -> - try - match - List.find - (function - | Constrexpr.CLocalAssum(l,k,t) -> - List.exists + try + match + List.find + (function + | Constrexpr.CLocalAssum(l,k,t) -> + List.exists (function {CAst.v=Name id} -> Id.equal id wf_args | _ -> false) - l - | _ -> false - ) - args - with - | Constrexpr.CLocalAssum(_,k,t) -> t,wf_args - | _ -> assert false - with Not_found -> assert false + l + | _ -> false + ) + args + with + | Constrexpr.CLocalAssum(_,k,t) -> t,wf_args + | _ -> assert false + with Not_found -> assert false in - let wf_rel_from_mes,is_mes = - match wf_rel_expr_opt with + let wf_rel_from_mes,is_mes = + match wf_rel_expr_opt with | None -> - let ltof = - let make_dir l = DirPath.make (List.rev_map Id.of_string l) in + let ltof = + let make_dir l = DirPath.make (List.rev_map Id.of_string l) in Libnames.qualid_of_path (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof")) in - let fun_from_mes = - let applied_mes = - Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in + let fun_from_mes = + let applied_mes = + Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in Constrexpr_ops.mkLambdaC ([CAst.make @@ Name wf_arg],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes) - in - let wf_rel_from_mes = - Constrexpr_ops.mkAppC(Constrexpr_ops.mkRefC ltof,[wf_arg_type;fun_from_mes]) - in - wf_rel_from_mes,true - | Some wf_rel_expr -> - let wf_rel_with_mes = - let a = Names.Id.of_string "___a" in - let b = Names.Id.of_string "___b" in - Constrexpr_ops.mkLambdaC( + in + let wf_rel_from_mes = + Constrexpr_ops.mkAppC(Constrexpr_ops.mkRefC ltof,[wf_arg_type;fun_from_mes]) + in + wf_rel_from_mes,true + | Some wf_rel_expr -> + let wf_rel_with_mes = + let a = Names.Id.of_string "___a" in + let b = Names.Id.of_string "___b" in + Constrexpr_ops.mkLambdaC( [CAst.make @@ Name a; CAst.make @@ Name b], - Constrexpr.Default Explicit, - wf_arg_type, - Constrexpr_ops.mkAppC(wf_rel_expr, - [ - Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC a]); - Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC b]) - ]) - ) - in - wf_rel_with_mes,false - in + Constrexpr.Default Explicit, + wf_arg_type, + Constrexpr_ops.mkAppC(wf_rel_expr, + [ + Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC a]); + Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC b]) + ]) + ) + in + wf_rel_with_mes,false + in register_wf interactive_proof ~is_mes:is_mes fname rec_impls wf_rel_from_mes wf_arg using_lemmas args ret_type body -let map_option f = function - | None -> None +let map_option f = function + | None -> None | Some v -> Some (f v) open Constrexpr let rec rebuild_bl aux bl typ = - match bl,typ with - | [], _ -> List.rev aux,typ - | (CLocalAssum(nal,bk,_))::bl',typ -> - rebuild_nal aux bk bl' nal typ - | (CLocalDef(na,_,_))::bl',{ CAst.v = CLetIn(_,nat,ty,typ') } -> - rebuild_bl (Constrexpr.CLocalDef(na,nat,ty)::aux) - bl' typ' - | _ -> assert false + match bl,typ with + | [], _ -> List.rev aux,typ + | (CLocalAssum(nal,bk,_))::bl',typ -> + rebuild_nal aux bk bl' nal typ + | (CLocalDef(na,_,_))::bl',{ CAst.v = CLetIn(_,nat,ty,typ') } -> + rebuild_bl (Constrexpr.CLocalDef(na,nat,ty)::aux) + bl' typ' + | _ -> assert false and rebuild_nal aux bk bl' nal typ = - match nal,typ with - | _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ - | [], _ -> rebuild_bl aux bl' typ + match nal,typ with + | _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ + | [], _ -> rebuild_bl aux bl' typ | na::nal,{ CAst.v = CProdN(CLocalAssum(na'::nal',bk',nal't)::rest,typ') } -> if Name.equal (na.CAst.v) (na'.CAst.v) || Name.is_anonymous (na'.CAst.v) - then - let assum = CLocalAssum([na],bk,nal't) in + then + let assum = CLocalAssum([na],bk,nal't) in let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in - rebuild_nal - (assum::aux) - bk - bl' - nal - (CAst.make @@ CProdN(new_rest,typ')) - else - let assum = CLocalAssum([na'],bk,nal't) in + rebuild_nal + (assum::aux) + bk + bl' + nal + (CAst.make @@ CProdN(new_rest,typ')) + else + let assum = CLocalAssum([na'],bk,nal't) in let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in - rebuild_nal - (assum::aux) - bk - bl' - (na::nal) - (CAst.make @@ CProdN(new_rest,typ')) - | _ -> - assert false + rebuild_nal + (assum::aux) + bk + bl' + (na::nal) + (CAst.make @@ CProdN(new_rest,typ')) + | _ -> + assert false let rebuild_bl aux bl typ = rebuild_bl aux bl typ -let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = +let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = let fixl,ntns = ComFixpoint.extract_fixpoint_components ~structonly:false fixpoint_exprl in let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in let constr_expr_typel = with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in - let fixpoint_exprl_with_new_bl = + let fixpoint_exprl_with_new_bl = List.map2 (fun ((lna,rec_order_opt,bl,ret_typ,opt_body),notation_list) fix_typ -> - - let new_bl',new_ret_type = rebuild_bl [] bl fix_typ in + + let new_bl',new_ret_type = rebuild_bl [] bl fix_typ in (((lna,rec_order_opt,new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) ) - fixpoint_exprl constr_expr_typel - in + fixpoint_exprl constr_expr_typel + in fixpoint_exprl_with_new_bl - + let do_generate_principle_aux pconstants on_error register_built interactive_proof (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Lemmas.t option = @@ -640,84 +640,84 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro match fixpoint_exprl with | [((_,Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)},_,_,_),_) as fixpoint_expr] -> let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr = - match recompute_binder_list [fixpoint_expr] with - | [e] -> e - | _ -> assert false - in - let fixpoint_exprl = [fixpoint_expr] in - let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - let recdefs,rec_impls = build_newrecursive fixpoint_exprl in - let using_lemmas = [] in - let pre_hook pconstants = - generate_principle - (ref (Evd.from_env (Global.env ()))) - pconstants - on_error - true - register_built - fixpoint_exprl - recdefs - true - in - if register_built + match recompute_binder_list [fixpoint_expr] with + | [e] -> e + | _ -> assert false + in + let fixpoint_exprl = [fixpoint_expr] in + let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let using_lemmas = [] in + let pre_hook pconstants = + generate_principle + (ref (Evd.from_env (Global.env ()))) + pconstants + on_error + true + register_built + fixpoint_exprl + recdefs + true + in + if register_built then register_wf interactive_proof name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false else None, false |[((_,Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)},_,_,_),_) as fixpoint_expr] -> let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr = - match recompute_binder_list [fixpoint_expr] with - | [e] -> e - | _ -> assert false - in - let fixpoint_exprl = [fixpoint_expr] in - let recdefs,rec_impls = build_newrecursive fixpoint_exprl in - let using_lemmas = [] in - let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - let pre_hook pconstants = - generate_principle - (ref (Evd.from_env (Global.env ()))) - pconstants - on_error - true - register_built - fixpoint_exprl - recdefs - true - in - if register_built + match recompute_binder_list [fixpoint_expr] with + | [e] -> e + | _ -> assert false + in + let fixpoint_exprl = [fixpoint_expr] in + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let using_lemmas = [] in + let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in + let pre_hook pconstants = + generate_principle + (ref (Evd.from_env (Global.env ()))) + pconstants + on_error + true + register_built + fixpoint_exprl + recdefs + true + in + if register_built then register_mes interactive_proof name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true else None, true | _ -> List.iter (function ((_na,ord,_args,_body,_type),_not) -> - match ord with + match ord with | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _) } -> - error - ("Cannot use mutual definition with well-founded recursion or measure") - | _ -> () - ) - fixpoint_exprl; - let fixpoint_exprl = recompute_binder_list fixpoint_exprl in - let fix_names = + error + ("Cannot use mutual definition with well-founded recursion or measure") + | _ -> () + ) + fixpoint_exprl; + let fixpoint_exprl = recompute_binder_list fixpoint_exprl in + let fix_names = List.map (function ((({CAst.v=name},_),_,_,_,_),_) -> name) fixpoint_exprl - in - (* ok all the expressions are structural *) - let recdefs,rec_impls = build_newrecursive fixpoint_exprl in - let is_rec = List.exists (is_rec fix_names) recdefs in + in + (* ok all the expressions are structural *) + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let is_rec = List.exists (is_rec fix_names) recdefs in let lemma,evd,pconstants = - if register_built + if register_built then register_struct is_rec fixpoint_exprl else None, Evd.from_env (Global.env ()), pconstants - in - let evd = ref evd in - generate_principle - (ref !evd) - pconstants - on_error - false - register_built - fixpoint_exprl - recdefs - interactive_proof - (Functional_principles_proofs.prove_princ_for_struct evd interactive_proof); + in + let evd = ref evd in + generate_principle + (ref !evd) + pconstants + on_error + false + register_built + fixpoint_exprl + recdefs + interactive_proof + (Functional_principles_proofs.prove_princ_for_struct evd interactive_proof); if register_built then begin derive_inversion fix_names; end; lemma, true @@ -734,12 +734,12 @@ let rec add_args id new_args = CAst.map (function CProdN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2) | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t) | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal, - add_args id new_args b1) + add_args id new_args b1) | CLambdaN(nal,b1) -> CLambdaN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2) | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t) | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal, - add_args id new_args b1) + add_args id new_args b1) | CLetIn(na,b1,t,b2) -> CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) | CAppExpl((pf,qid,us),exprl) -> @@ -748,26 +748,26 @@ let rec add_args id new_args = CAst.map (function else CAppExpl((pf,qid,us),List.map (add_args id new_args) exprl) | CApp((pf,b),bl) -> CApp((pf,add_args id new_args b), - List.map (fun (e,o) -> add_args id new_args e,o) bl) + List.map (fun (e,o) -> add_args id new_args e,o) bl) | CCases(sty,b_option,cel,cal) -> CCases(sty,Option.map (add_args id new_args) b_option, - List.map (fun (b,na,b_option) -> - add_args id new_args b, - na, b_option) cel, + List.map (fun (b,na,b_option) -> + add_args id new_args b, + na, b_option) cel, List.map CAst.(map (fun (cpl,e) -> (cpl,add_args id new_args e))) cal - ) + ) | CLetTuple(nal,(na,b_option),b1,b2) -> CLetTuple(nal,(na,Option.map (add_args id new_args) b_option), - add_args id new_args b1, - add_args id new_args b2 - ) + add_args id new_args b1, + add_args id new_args b2 + ) | CIf(b1,(na,b_option),b2,b3) -> CIf(add_args id new_args b1, - (na,Option.map (add_args id new_args) b_option), - add_args id new_args b2, - add_args id new_args b3 - ) + (na,Option.map (add_args id new_args) b_option), + add_args id new_args b2, + add_args id new_args b3 + ) | CHole _ | CPatVar _ | CEvar _ @@ -794,35 +794,35 @@ let rec chop_n_arrow n t = else (* If not we check the form of [t] *) match t.CAst.v with | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, two results are possible : - either we need to discard more than the number of arrows contained - in this product declaration then we just recall [chop_n_arrow] on - the remaining number of arrow to chop and [t'] we discard it and - recall [chop_n_arrow], either this product contains more arrows - than the number we need to chop and then we return the new type - *) - begin - try - let new_n = - let rec aux (n:int) = function - [] -> n + either we need to discard more than the number of arrows contained + in this product declaration then we just recall [chop_n_arrow] on + the remaining number of arrow to chop and [t'] we discard it and + recall [chop_n_arrow], either this product contains more arrows + than the number we need to chop and then we return the new type + *) + begin + try + let new_n = + let rec aux (n:int) = function + [] -> n | CLocalAssum(nal,k,t'')::nal_ta' -> - let nal_l = List.length nal in - if n >= nal_l - then - aux (n - nal_l) nal_ta' - else - let new_t' = CAst.make @@ - Constrexpr.CProdN( + let nal_l = List.length nal in + if n >= nal_l + then + aux (n - nal_l) nal_ta' + else + let new_t' = CAst.make @@ + Constrexpr.CProdN( CLocalAssum((snd (List.chop n nal)),k,t'')::nal_ta',t') - in - raise (Stop new_t') + in + raise (Stop new_t') | _ -> anomaly (Pp.str "Not enough products.") - in - aux n nal_ta' - in - chop_n_arrow new_n t' - with Stop t -> t - end + in + aux n nal_ta' + in + chop_n_arrow new_n t' + with Stop t -> t + end | _ -> anomaly (Pp.str "Not enough products.") @@ -830,11 +830,11 @@ let rec get_args b t : Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr = match b.CAst.v with | Constrexpr.CLambdaN (CLocalAssum(nal,k,ta) as d::rest, b') -> - begin + begin let n = List.length nal in let nal_tas,b'',t'' = get_args (CAst.make ?loc:b.CAst.loc @@ Constrexpr.CLambdaN (rest,b')) (chop_n_arrow n t) in d :: nal_tas, b'',t'' - end + end | Constrexpr.CLambdaN ([], b) -> [],b,t | _ -> [],b,t @@ -855,15 +855,15 @@ let make_graph (f_ref : GlobRef.t) = | None -> error "Cannot build a graph over an axiom!" | Some (body, _) -> let env = Global.env () in - let extern_body,extern_type = - with_full_print (fun () -> - (Constrextern.extern_constr false env sigma (EConstr.of_constr body), - Constrextern.extern_type false env sigma + let extern_body,extern_type = + with_full_print (fun () -> + (Constrextern.extern_constr false env sigma (EConstr.of_constr body), + Constrextern.extern_type false env sigma (EConstr.of_constr (*FIXME*) c_body.const_type) - ) - ) - () - in + ) + ) + () + in let (nal_tas,b,t) = get_args extern_body extern_type in let expr_list = match b.CAst.v with @@ -897,15 +897,15 @@ let make_graph (f_ref : GlobRef.t) = fixexprl in l - | _ -> - let id = Label.to_id (Constant.label c) in + | _ -> + let id = Label.to_id (Constant.label c) in [((CAst.make id,None),None,nal_tas,t,Some b),[]] - in + in let mp = Constant.modpath c in let pstate = do_generate_principle_aux [c,Univ.Instance.empty] error_error false false expr_list in assert (Option.is_empty pstate); - (* We register the infos *) - List.iter + (* We register the infos *) + List.iter (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id))) expr_list) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 6d9690096f..7683ce1757 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -49,10 +49,10 @@ let filter_map filter f = let rec it = function | [] -> [] | e::l -> - if filter e - then - (f e) :: it l - else it l + if filter e + then + (f e) :: it l + else it l in it @@ -62,12 +62,12 @@ let chop_rlambda_n = if n == 0 then List.rev acc,rt else - match DAst.get rt with - | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b - | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b - | _ -> - raise (CErrors.UserError(Some "chop_rlambda_n", - str "chop_rlambda_n: Not enough Lambdas")) + match DAst.get rt with + | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b + | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b + | _ -> + raise (CErrors.UserError(Some "chop_rlambda_n", + str "chop_rlambda_n: Not enough Lambdas")) in chop_lambda_n [] @@ -76,9 +76,9 @@ let chop_rprod_n = if n == 0 then List.rev acc,rt else - match DAst.get rt with - | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b - | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products")) + match DAst.get rt with + | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b + | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products")) in chop_prod_n [] @@ -129,8 +129,8 @@ let save id const ?hook uctx (locality,_,kind) = let r = match locality with | Discharge -> let k = Kindops.logical_kind_of_goal_kind kind in - let c = SectionLocalDef const in - let _ = declare_variable id (Lib.cwd(), c, k) in + let c = SectionLocalDef const in + let _ = declare_variable id (Lib.cwd(), c, k) in VarRef id | Global local -> let k = Kindops.logical_kind_of_goal_kind kind in @@ -166,14 +166,14 @@ let with_full_print f a = res with | reraise -> - Impargs.make_implicit_args old_implicit_args; - Impargs.make_strict_implicit_args old_strict_implicit_args; - Impargs.make_contextual_implicit_args old_contextual_implicit_args; - Flags.raw_print := old_rawprint; - Constrextern.print_universes := old_printuniverses; + Impargs.make_implicit_args old_implicit_args; + Impargs.make_strict_implicit_args old_strict_implicit_args; + Impargs.make_contextual_implicit_args old_contextual_implicit_args; + Flags.raw_print := old_rawprint; + Constrextern.print_universes := old_printuniverses; Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; - Dumpglob.continue (); - raise reraise + Dumpglob.continue (); + raise reraise @@ -213,8 +213,8 @@ let rec do_cache_info finfo = function else if finfo'.function_constant = finfo.function_constant then finfo::finfos else - let res = do_cache_info finfo finfos in - if res == finfos then l else finfo'::l + let res = do_cache_info finfo finfos in + if res == finfos then l else finfo'::l let cache_Function (_,(finfos)) = @@ -318,7 +318,7 @@ let find_Function_of_graph ind = let update_Function finfo = (* Pp.msgnl (pr_info finfo); *) Lib.add_anonymous_leaf (in_Function finfo) - + let add_Function is_general f = let f_id = Label.to_id (Constant.label f) in @@ -356,7 +356,7 @@ let functional_induction_rewrite_dependent_proofs = ref true let function_debug = ref false open Goptions -let functional_induction_rewrite_dependent_proofs_sig = +let functional_induction_rewrite_dependent_proofs_sig = { optdepr = false; optname = "Functional Induction Rewrite Dependent"; @@ -380,7 +380,7 @@ let function_debug_sig = let () = declare_bool_option function_debug_sig -let do_observe () = !function_debug +let do_observe () = !function_debug diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 857b7df96f..376e1cb2cc 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -56,7 +56,7 @@ let do_observe_tac s tac g = let reraise = CErrors.push reraise in let e = ExplainErr.process_vernac_interp_error reraise in observe (hov 0 (str "observation "++ s++str " raised exception " ++ - CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal )); + CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal )); iraise reraise;; let observe_tac s tac g = @@ -115,8 +115,8 @@ let generate_type evd g_to_f f graph i = in (*i We need to name the vars [res] and [fv] i*) let filter = fun decl -> match RelDecl.get_name decl with - | Name id -> Some id - | Anonymous -> None + | Name id -> Some id + | Anonymous -> None in let named_ctxt = Id.Set.of_list (List.map_filter filter fun_ctxt) in let res_id = Namegen.next_ident_away_in_goal (Id.of_string "_res") named_ctxt in @@ -232,12 +232,12 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i (* and built the intro pattern for each of them *) let intro_pats = List.map - (fun decl -> - List.map + (fun decl -> + List.map (fun id -> CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) - (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl))))) - ) - branches + (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl))))) + ) + branches in (* before building the full intro pattern for the principle *) let eq_ind = make_eq () in @@ -249,113 +249,113 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i let prove_branche i g = (* We get the identifiers of this branch *) let pre_args = - List.fold_right + List.fold_right (fun {CAst.v=pat} acc -> - match pat with + match pat with | IntroNaming (Namegen.IntroIdentifier id) -> id::acc - | _ -> anomaly (Pp.str "Not an identifier.") - ) - (List.nth intro_pats (pred i)) - [] + | _ -> anomaly (Pp.str "Not an identifier.") + ) + (List.nth intro_pats (pred i)) + [] in (* and get the real args of the branch by unfolding the defined constant *) (* - We can then recompute the arguments of the constructor. - For each [hid] introduced by this branch, if [hid] has type - $forall res, res=fv -> graph.(j)\ x_1\ x_n res$ the corresponding arguments of the constructor are - [ fv (hid fv (refl_equal fv)) ]. - If [hid] has another type the corresponding argument of the constructor is [hid] + We can then recompute the arguments of the constructor. + For each [hid] introduced by this branch, if [hid] has type + $forall res, res=fv -> graph.(j)\ x_1\ x_n res$ the corresponding arguments of the constructor are + [ fv (hid fv (refl_equal fv)) ]. + If [hid] has another type the corresponding argument of the constructor is [hid] *) let constructor_args g = - List.fold_right - (fun hid acc -> - let type_of_hid = pf_unsafe_type_of g (mkVar hid) in - let sigma = project g in - match EConstr.kind sigma type_of_hid with + List.fold_right + (fun hid acc -> + let type_of_hid = pf_unsafe_type_of g (mkVar hid) in + let sigma = project g in + match EConstr.kind sigma type_of_hid with | Prod(_,_,t') -> - begin - match EConstr.kind sigma t' with + begin + match EConstr.kind sigma t' with | Prod(_,t'',t''') -> - begin - match EConstr.kind sigma t'',EConstr.kind sigma t''' with - | App(eq,args), App(graph',_) - when - (EConstr.eq_constr sigma eq eq_ind) && - Array.exists (EConstr.eq_constr_nounivs sigma graph') graphs_constr -> - (args.(2)::(mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|])) - ::acc) - | _ -> mkVar hid :: acc - end - | _ -> mkVar hid :: acc - end - | _ -> mkVar hid :: acc - ) pre_args [] + begin + match EConstr.kind sigma t'',EConstr.kind sigma t''' with + | App(eq,args), App(graph',_) + when + (EConstr.eq_constr sigma eq eq_ind) && + Array.exists (EConstr.eq_constr_nounivs sigma graph') graphs_constr -> + (args.(2)::(mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|])) + ::acc) + | _ -> mkVar hid :: acc + end + | _ -> mkVar hid :: acc + end + | _ -> mkVar hid :: acc + ) pre_args [] in (* in fact we must also add the parameters to the constructor args *) let constructor_args g = - let params_id = fst (List.chop princ_infos.nparams args_names) in - (List.map mkVar params_id)@((constructor_args g)) + let params_id = fst (List.chop princ_infos.nparams args_names) in + (List.map mkVar params_id)@((constructor_args g)) in (* We then get the constructor corresponding to this branch and - modifies the references has needed i.e. - if the constructor is the last one of the current inductive then - add one the number of the inductive to take and add the number of constructor of the previous - graph to the minimal constructor number + modifies the references has needed i.e. + if the constructor is the last one of the current inductive then + add one the number of the inductive to take and add the number of constructor of the previous + graph to the minimal constructor number *) let constructor = - let constructor_num = i - !min_constr_number in - let length = Array.length (mib.Declarations.mind_packets.(!ind_number).Declarations.mind_consnames) in - if constructor_num <= length - then - begin - (kn,!ind_number),constructor_num - end - else - begin - incr ind_number; - min_constr_number := !min_constr_number + length ; - (kn,!ind_number),1 - end + let constructor_num = i - !min_constr_number in + let length = Array.length (mib.Declarations.mind_packets.(!ind_number).Declarations.mind_consnames) in + if constructor_num <= length + then + begin + (kn,!ind_number),constructor_num + end + else + begin + incr ind_number; + min_constr_number := !min_constr_number + length ; + (kn,!ind_number),1 + end in (* we can then build the final proof term *) let app_constructor g = applist((mkConstructU(constructor,u)),constructor_args g) in (* an apply the tactic *) let res,hres = - match generate_fresh_id (Id.of_string "z") (ids(* @this_branche_ids *)) 2 with - | [res;hres] -> res,hres - | _ -> assert false + match generate_fresh_id (Id.of_string "z") (ids(* @this_branche_ids *)) 2 with + | [res;hres] -> res,hres + | _ -> assert false in (* observe (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor); *) ( - tclTHENLIST - [ - observe_tac("h_intro_patterns ") (let l = (List.nth intro_pats (pred i)) in - match l with - | [] -> tclIDTAC - | _ -> Proofview.V82.of_tactic (intro_patterns false l)); - (* unfolding of all the defined variables introduced by this branch *) - (* observe_tac "unfolding" pre_tac; *) - (* $zeta$ normalizing of the conclusion *) - Proofview.V82.of_tactic (reduce - (Genredexpr.Cbv - { Redops.all_flags with - Genredexpr.rDelta = false ; - Genredexpr.rConst = [] - } - ) - Locusops.onConcl); - observe_tac ("toto ") tclIDTAC; - + tclTHENLIST + [ + observe_tac("h_intro_patterns ") (let l = (List.nth intro_pats (pred i)) in + match l with + | [] -> tclIDTAC + | _ -> Proofview.V82.of_tactic (intro_patterns false l)); + (* unfolding of all the defined variables introduced by this branch *) + (* observe_tac "unfolding" pre_tac; *) + (* $zeta$ normalizing of the conclusion *) + Proofview.V82.of_tactic (reduce + (Genredexpr.Cbv + { Redops.all_flags with + Genredexpr.rDelta = false ; + Genredexpr.rConst = [] + } + ) + Locusops.onConcl); + observe_tac ("toto ") tclIDTAC; + (* introducing the result of the graph and the equality hypothesis *) - observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]); - (* replacing [res] with its value *) - observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres))); - (* Conclusion *) - observe_tac "exact" (fun g -> - Proofview.V82.of_tactic (exact_check (app_constructor g)) g) - ] + observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]); + (* replacing [res] with its value *) + observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres))); + (* Conclusion *) + observe_tac "exact" (fun g -> + Proofview.V82.of_tactic (exact_check (app_constructor g)) g) + ] ) - g + g in (* end of branche proof *) let lemmas = @@ -379,44 +379,44 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i *) let bindings = let params_bindings,avoid = - List.fold_left2 - (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in - p::bindings,id::avoid - ) - ([],pf_ids_of_hyps g) - princ_infos.params - (List.rev params) + List.fold_left2 + (fun (bindings,avoid) decl p -> + let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in + p::bindings,id::avoid + ) + ([],pf_ids_of_hyps g) + princ_infos.params + (List.rev params) in let lemmas_bindings = - List.rev (fst (List.fold_left2 - (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in + List.rev (fst (List.fold_left2 + (fun (bindings,avoid) decl p -> + let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in (Reductionops.nf_zeta (pf_env g) (project g) p)::bindings,id::avoid) - ([],avoid) - princ_infos.predicates - (lemmas))) + ([],avoid) + princ_infos.predicates + (lemmas))) in (params_bindings@lemmas_bindings) in tclTHENLIST - [ - observe_tac "principle" (Proofview.V82.of_tactic (assert_by - (Name principle_id) - princ_type - (exact_check f_principle))); - observe_tac "intro args_names" (tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) args_names); - (* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty ((mkApp (mkVar principle_id,Array.of_list bindings))))); *) - observe_tac "idtac" tclIDTAC; - tclTHEN_i - (observe_tac - "functional_induction" ( - (fun gl -> - let term = mkApp (mkVar principle_id,Array.of_list bindings) in - let gl', _ty = pf_eapply (Typing.type_of ~refresh:true) gl term in - Proofview.V82.of_tactic (apply term) gl') - )) - (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g ) + [ + observe_tac "principle" (Proofview.V82.of_tactic (assert_by + (Name principle_id) + princ_type + (exact_check f_principle))); + observe_tac "intro args_names" (tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) args_names); + (* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty ((mkApp (mkVar principle_id,Array.of_list bindings))))); *) + observe_tac "idtac" tclIDTAC; + tclTHEN_i + (observe_tac + "functional_induction" ( + (fun gl -> + let term = mkApp (mkVar principle_id,Array.of_list bindings) in + let gl', _ty = pf_eapply (Typing.type_of ~refresh:true) gl term in + Proofview.V82.of_tactic (apply term) gl') + )) + (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g ) ] g @@ -431,7 +431,7 @@ let generalize_dependent_of x hyp g = tclMAP (function | LocalAssum ({binder_name=id},t) when not (Id.equal id hyp) && - (Termops.occur_var (pf_env g) (project g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id]) + (Termops.occur_var (pf_env g) (project g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id]) | _ -> tclIDTAC ) (pf_hyps g) @@ -458,99 +458,99 @@ and intros_with_rewrite_aux : Tacmach.tactic = let sigma = project g in match EConstr.kind sigma (pf_concl g) with | Prod(_,t,t') -> - begin - match EConstr.kind sigma t with - | App(eq,args) when (EConstr.eq_constr sigma eq eq_ind) -> - if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2) - then - let id = pf_get_new_id (Id.of_string "y") g in - tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g - else if isVar sigma args.(1) && (Environ.evaluable_named (destVar sigma args.(1)) (pf_env g)) - then tclTHENLIST[ - Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))]); - tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))] ((destVar sigma args.(1)),Locus.InHyp) ))) - (pf_ids_of_hyps g); - intros_with_rewrite - ] g - else if isVar sigma args.(2) && (Environ.evaluable_named (destVar sigma args.(2)) (pf_env g)) - then tclTHENLIST[ - Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))]); - tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))] ((destVar sigma args.(2)),Locus.InHyp) ))) - (pf_ids_of_hyps g); - intros_with_rewrite - ] g - else if isVar sigma args.(1) - then - let id = pf_get_new_id (Id.of_string "y") g in - tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id); - generalize_dependent_of (destVar sigma args.(1)) id; - tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id))); - intros_with_rewrite - ] - g - else if isVar sigma args.(2) - then - let id = pf_get_new_id (Id.of_string "y") g in - tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id); - generalize_dependent_of (destVar sigma args.(2)) id; - tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id))); - intros_with_rewrite - ] - g - else - begin - let id = pf_get_new_id (Id.of_string "y") g in - tclTHENLIST[ - Proofview.V82.of_tactic (Simple.intro id); - tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id))); - intros_with_rewrite - ] g - end + begin + match EConstr.kind sigma t with + | App(eq,args) when (EConstr.eq_constr sigma eq eq_ind) -> + if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2) + then + let id = pf_get_new_id (Id.of_string "y") g in + tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g + else if isVar sigma args.(1) && (Environ.evaluable_named (destVar sigma args.(1)) (pf_env g)) + then tclTHENLIST[ + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))]); + tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))] ((destVar sigma args.(1)),Locus.InHyp) ))) + (pf_ids_of_hyps g); + intros_with_rewrite + ] g + else if isVar sigma args.(2) && (Environ.evaluable_named (destVar sigma args.(2)) (pf_env g)) + then tclTHENLIST[ + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))]); + tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))] ((destVar sigma args.(2)),Locus.InHyp) ))) + (pf_ids_of_hyps g); + intros_with_rewrite + ] g + else if isVar sigma args.(1) + then + let id = pf_get_new_id (Id.of_string "y") g in + tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id); + generalize_dependent_of (destVar sigma args.(1)) id; + tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id))); + intros_with_rewrite + ] + g + else if isVar sigma args.(2) + then + let id = pf_get_new_id (Id.of_string "y") g in + tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id); + generalize_dependent_of (destVar sigma args.(2)) id; + tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id))); + intros_with_rewrite + ] + g + else + begin + let id = pf_get_new_id (Id.of_string "y") g in + tclTHENLIST[ + Proofview.V82.of_tactic (Simple.intro id); + tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id))); + intros_with_rewrite + ] g + end | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) -> - Proofview.V82.of_tactic tauto g - | Case(_,_,v,_) -> - tclTHENLIST[ - Proofview.V82.of_tactic (simplest_case v); - intros_with_rewrite - ] g - | LetIn _ -> - tclTHENLIST[ - Proofview.V82.of_tactic (reduce - (Genredexpr.Cbv - {Redops.all_flags - with Genredexpr.rDelta = false; - }) - Locusops.onConcl) - ; - intros_with_rewrite - ] g - | _ -> - let id = pf_get_new_id (Id.of_string "y") g in - tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id);intros_with_rewrite] g - end - | LetIn _ -> - tclTHENLIST[ - Proofview.V82.of_tactic (reduce - (Genredexpr.Cbv - {Redops.all_flags - with Genredexpr.rDelta = false; - }) - Locusops.onConcl) - ; - intros_with_rewrite - ] g - | _ -> tclIDTAC g + Proofview.V82.of_tactic tauto g + | Case(_,_,v,_) -> + tclTHENLIST[ + Proofview.V82.of_tactic (simplest_case v); + intros_with_rewrite + ] g + | LetIn _ -> + tclTHENLIST[ + Proofview.V82.of_tactic (reduce + (Genredexpr.Cbv + {Redops.all_flags + with Genredexpr.rDelta = false; + }) + Locusops.onConcl) + ; + intros_with_rewrite + ] g + | _ -> + let id = pf_get_new_id (Id.of_string "y") g in + tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id);intros_with_rewrite] g + end + | LetIn _ -> + tclTHENLIST[ + Proofview.V82.of_tactic (reduce + (Genredexpr.Cbv + {Redops.all_flags + with Genredexpr.rDelta = false; + }) + Locusops.onConcl) + ; + intros_with_rewrite + ] g + | _ -> tclIDTAC g let rec reflexivity_with_destruct_cases g = let destruct_case () = try match EConstr.kind (project g) (snd (destApp (project g) (pf_concl g))).(2) with - | Case(_,_,v,_) -> - tclTHENLIST[ - Proofview.V82.of_tactic (simplest_case v); - Proofview.V82.of_tactic intros; - observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases - ] + | Case(_,_,v,_) -> + tclTHENLIST[ + Proofview.V82.of_tactic (simplest_case v); + Proofview.V82.of_tactic intros; + observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases + ] | _ -> Proofview.V82.of_tactic reflexivity with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity in @@ -563,27 +563,27 @@ let rec reflexivity_with_destruct_cases g = let discr_inject = Tacticals.onAllHypsAndConcl ( fun sc g -> - match sc with - None -> tclIDTAC g - | Some id -> - match EConstr.kind (project g) (pf_unsafe_type_of g (mkVar id)) with - | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind -> - if Equality.discriminable (pf_env g) (project g) t1 t2 - then Proofview.V82.of_tactic (Equality.discrHyp id) g - else if Equality.injectable (pf_env g) (project g) ~keep_proofs:None t1 t2 - then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp my_inj_flags None id);thin [id];intros_with_rewrite] g - else tclIDTAC g - | _ -> tclIDTAC g + match sc with + None -> tclIDTAC g + | Some id -> + match EConstr.kind (project g) (pf_unsafe_type_of g (mkVar id)) with + | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind -> + if Equality.discriminable (pf_env g) (project g) t1 t2 + then Proofview.V82.of_tactic (Equality.discrHyp id) g + else if Equality.injectable (pf_env g) (project g) ~keep_proofs:None t1 t2 + then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp my_inj_flags None id);thin [id];intros_with_rewrite] g + else tclIDTAC g + | _ -> tclIDTAC g ) in (tclFIRST [ observe_tac "reflexivity_with_destruct_cases : reflexivity" (Proofview.V82.of_tactic reflexivity); observe_tac "reflexivity_with_destruct_cases : destruct_case" ((destruct_case ())); (* We reach this point ONLY if - the same value is matched (at least) two times - along binding path. - In this case, either we have a discriminable hypothesis and we are done, - either at least an injectable one and we do the injection before continuing + the same value is matched (at least) two times + along binding path. + In this case, either we have a discriminable hypothesis and we are done, + either at least an injectable one and we do the injection before continuing *) observe_tac "reflexivity_with_destruct_cases : others" (tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases) ]) @@ -626,7 +626,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti let lemmas = Array.map (fun (_,(ctxt,concl)) -> Reductionops.nf_zeta (pf_env g) (project g) (EConstr.it_mkLambda_or_LetIn concl ctxt)) - lemmas_types_infos + lemmas_types_infos in (* We get the constant and the principle corresponding to this lemma *) let f = funcs.(i) in @@ -642,8 +642,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti (* and fresh names for res H and the principle (cf bug bug #1174) *) let res,hres,graph_principle_id = match generate_fresh_id (Id.of_string "z") ids 3 with - | [res;hres;graph_principle_id] -> res,hres,graph_principle_id - | _ -> assert false + | [res;hres;graph_principle_id] -> res,hres,graph_principle_id + | _ -> assert false in let ids = res::hres::graph_principle_id::ids in (* we also compute fresh names for each hyptohesis of each branch @@ -651,12 +651,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti let branches = List.rev princ_infos.branches in let intro_pats = List.map - (fun decl -> - List.map - (fun id -> id) - (generate_fresh_id (Id.of_string "y") ids (nb_prod (project g) (RelDecl.get_type decl))) - ) - branches + (fun decl -> + List.map + (fun id -> id) + (generate_fresh_id (Id.of_string "y") ids (nb_prod (project g) (RelDecl.get_type decl))) + ) + branches in (* We will need to change the function by its body using [f_equation] if it is recursive (that is the graph is infinite @@ -671,25 +671,25 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti if infos.is_general || Rtree.is_infinite Declareops.eq_recarg graph_def.mind_recargs then - let eq_lemma = - try Option.get (infos).equation_lemma - with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma.") - in - tclTHENLIST[ - tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids; - Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma)); - (* Don't forget to $\zeta$ normlize the term since the principles + let eq_lemma = + try Option.get (infos).equation_lemma + with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma.") + in + tclTHENLIST[ + tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids; + Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma)); + (* Don't forget to $\zeta$ normlize the term since the principles have been $\zeta$-normalized *) - Proofview.V82.of_tactic (reduce - (Genredexpr.Cbv - {Redops.all_flags - with Genredexpr.rDelta = false; - }) - Locusops.onConcl) - ; - Proofview.V82.of_tactic (generalize (List.map mkVar ids)); - thin ids - ] + Proofview.V82.of_tactic (reduce + (Genredexpr.Cbv + {Redops.all_flags + with Genredexpr.rDelta = false; + }) + Locusops.onConcl) + ; + Proofview.V82.of_tactic (generalize (List.map mkVar ids)); + thin ids + ] else Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst (project g) f)))]) in @@ -699,39 +699,39 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti let prove_branche i g = (* we fist compute the inductive corresponding to the branch *) let this_ind_number = - let constructor_num = i - !min_constr_number in - let length = Array.length (graphs.(!ind_number).Declarations.mind_consnames) in - if constructor_num <= length - then !ind_number - else - begin - incr ind_number; - min_constr_number := !min_constr_number + length; - !ind_number - end + let constructor_num = i - !min_constr_number in + let length = Array.length (graphs.(!ind_number).Declarations.mind_consnames) in + if constructor_num <= length + then !ind_number + else + begin + incr ind_number; + min_constr_number := !min_constr_number + length; + !ind_number + end in let this_branche_ids = List.nth intro_pats (pred i) in tclTHENLIST[ - (* we expand the definition of the function *) + (* we expand the definition of the function *) observe_tac "rewrite_tac" (rewrite_tac this_ind_number this_branche_ids); - (* introduce hypothesis with some rewrite *) + (* introduce hypothesis with some rewrite *) observe_tac "intros_with_rewrite (all)" intros_with_rewrite; - (* The proof is (almost) complete *) + (* The proof is (almost) complete *) observe_tac "reflexivity" (reflexivity_with_destruct_cases) ] - g + g in let params_names = fst (List.chop princ_infos.nparams args_names) in let open EConstr in let params = List.map mkVar params_names in tclTHENLIST [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]); - observe_tac "h_generalize" - (Proofview.V82.of_tactic (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)])); - Proofview.V82.of_tactic (Simple.intro graph_principle_id); - observe_tac "" (tclTHEN_i - (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings))))) - (fun i g -> observe_tac "prove_branche" (prove_branche i) g )) + observe_tac "h_generalize" + (Proofview.V82.of_tactic (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)])); + Proofview.V82.of_tactic (Simple.intro graph_principle_id); + observe_tac "" (tclTHEN_i + (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings))))) + (fun i g -> observe_tac "prove_branche" (prove_branche i) g )) ] g @@ -752,105 +752,105 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list funind_purify (fun () -> let env = Global.env () in - let evd = ref (Evd.from_env env) in + let evd = ref (Evd.from_env env) in let graphs_constr = Array.map mkInd graphs in let lemmas_types_infos = Util.Array.map2_i - (fun i f_constr graph -> - (* let const_of_f,u = destConst f_constr in *) - let (type_of_lemma_ctxt,type_of_lemma_concl,graph) = - generate_type evd false f_constr graph i - in - let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in - graphs_constr.(i) <- graph; - let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in + (fun i f_constr graph -> + (* let const_of_f,u = destConst f_constr in *) + let (type_of_lemma_ctxt,type_of_lemma_concl,graph) = + generate_type evd false f_constr graph i + in + let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in + graphs_constr.(i) <- graph; + let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in evd := sigma; let type_of_lemma = Reductionops.nf_zeta (Global.env ()) !evd type_of_lemma in - observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma); - type_of_lemma,type_info - ) - funs_constr - graphs_constr + observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma); + type_of_lemma,type_info + ) + funs_constr + graphs_constr in let schemes = (* The functional induction schemes are computed and not saved if there is more that one function - if the block contains only one function we can safely reuse [f_rect] + if the block contains only one function we can safely reuse [f_rect] *) try - if not (Int.equal (Array.length funs_constr) 1) then raise Not_found; - [| find_induction_principle evd funs_constr.(0) |] + if not (Int.equal (Array.length funs_constr) 1) then raise Not_found; + [| find_induction_principle evd funs_constr.(0) |] with Not_found -> - ( - - Array.of_list - (List.map - (fun entry -> - (EConstr.of_constr (fst (fst(Future.force entry.Entries.const_entry_body))), EConstr.of_constr (Option.get entry.Entries.const_entry_type )) - ) - (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs)) - ) - ) + ( + + Array.of_list + (List.map + (fun entry -> + (EConstr.of_constr (fst (fst(Future.force entry.Entries.const_entry_body))), EConstr.of_constr (Option.get entry.Entries.const_entry_type )) + ) + (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs)) + ) + ) in let proving_tac = prove_fun_correct !evd funs_constr graphs_constr schemes lemmas_types_infos in Array.iteri (fun i f_as_constant -> - let f_id = Label.to_id (Constant.label (fst f_as_constant)) in - (*i The next call to mk_correct_id is valid since we are constructing the lemma - Ensures by: obvious - i*) - let lem_id = mk_correct_id f_id in + let f_id = Label.to_id (Constant.label (fst f_as_constant)) in + (*i The next call to mk_correct_id is valid since we are constructing the lemma + Ensures by: obvious + i*) + let lem_id = mk_correct_id f_id in let (typ,_) = lemmas_types_infos.(i) in let lemma = Lemmas.start_lemma - lem_id + lem_id Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) !evd typ in let lemma = fst @@ Lemmas.by - (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") + (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i))) lemma in let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in - let finfo = find_Function_infos (fst f_as_constant) in - (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *) - let _,lem_cst_constr = Evd.fresh_global - (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in + let finfo = find_Function_infos (fst f_as_constant) in + (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *) + let _,lem_cst_constr = Evd.fresh_global + (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in let (lem_cst,_) = destConst !evd lem_cst_constr in - update_Function {finfo with correctness_lemma = Some lem_cst}; + update_Function {finfo with correctness_lemma = Some lem_cst}; ) funs; let lemmas_types_infos = Util.Array.map2_i - (fun i f_constr graph -> - let (type_of_lemma_ctxt,type_of_lemma_concl,graph) = - generate_type evd true f_constr graph i - in - let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in - graphs_constr.(i) <- graph; - let type_of_lemma = - EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt - in + (fun i f_constr graph -> + let (type_of_lemma_ctxt,type_of_lemma_concl,graph) = + generate_type evd true f_constr graph i + in + let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in + graphs_constr.(i) <- graph; + let type_of_lemma = + EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt + in let type_of_lemma = Reductionops.nf_zeta env !evd type_of_lemma in observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma); - type_of_lemma,type_info - ) - funs_constr - graphs_constr + type_of_lemma,type_info + ) + funs_constr + graphs_constr in let (kn,_) as graph_ind,u = (destInd !evd graphs_constr.(0)) in let mib,mip = Global.lookup_inductive graph_ind in - let sigma, scheme = - (Indrec.build_mutual_induction_scheme (Global.env ()) !evd - (Array.to_list - (Array.mapi - (fun i _ -> ((kn,i), EInstance.kind !evd u),true,InType) - mib.Declarations.mind_packets - ) - ) - ) + let sigma, scheme = + (Indrec.build_mutual_induction_scheme (Global.env ()) !evd + (Array.to_list + (Array.mapi + (fun i _ -> ((kn,i), EInstance.kind !evd u),true,InType) + mib.Declarations.mind_packets + ) + ) + ) in let schemes = Array.of_list scheme @@ -860,23 +860,23 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list in Array.iteri (fun i f_as_constant -> - let f_id = Label.to_id (Constant.label (fst f_as_constant)) in - (*i The next call to mk_complete_id is valid since we are constructing the lemma - Ensures by: obvious - i*) - let lem_id = mk_complete_id f_id in + let f_id = Label.to_id (Constant.label (fst f_as_constant)) in + (*i The next call to mk_complete_id is valid since we are constructing the lemma + Ensures by: obvious + i*) + let lem_id = mk_complete_id f_id in let lemma = Lemmas.start_lemma lem_id Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma (fst lemmas_types_infos.(i)) in let lemma = fst (Lemmas.by - (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") + (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i))) lemma) in let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in - let finfo = find_Function_infos (fst f_as_constant) in - let _,lem_cst_constr = Evd.fresh_global - (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in + let finfo = find_Function_infos (fst f_as_constant) in + let _,lem_cst_constr = Evd.fresh_global + (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in let (lem_cst,_) = destConst !evd lem_cst_constr in - update_Function {finfo with completeness_lemma = Some lem_cst} + update_Function {finfo with completeness_lemma = Some lem_cst} ) funs) () @@ -894,31 +894,31 @@ let revert_graph kn post_tac hid g = let typ = pf_unsafe_type_of g (mkVar hid) in match EConstr.kind sigma typ with | App(i,args) when isInd sigma i -> - let ((kn',num) as ind'),u = destInd sigma i in - if MutInd.equal kn kn' - then (* We have generated a graph hypothesis so that we must change it if we can *) - let info = - try find_Function_of_graph ind' - with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*) - anomaly (Pp.str "Cannot retrieve infos about a mutual block.") - in - (* if we can find a completeness lemma for this function - then we can come back to the functional form. If not, we do nothing - *) - match info.completeness_lemma with - | None -> tclIDTAC g - | Some f_complete -> - let f_args,res = Array.chop (Array.length args - 1) args in - tclTHENLIST - [ - Proofview.V82.of_tactic (generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]); - thin [hid]; - Proofview.V82.of_tactic (Simple.intro hid); - post_tac hid - ] - g - - else tclIDTAC g + let ((kn',num) as ind'),u = destInd sigma i in + if MutInd.equal kn kn' + then (* We have generated a graph hypothesis so that we must change it if we can *) + let info = + try find_Function_of_graph ind' + with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*) + anomaly (Pp.str "Cannot retrieve infos about a mutual block.") + in + (* if we can find a completeness lemma for this function + then we can come back to the functional form. If not, we do nothing + *) + match info.completeness_lemma with + | None -> tclIDTAC g + | Some f_complete -> + let f_args,res = Array.chop (Array.length args - 1) args in + tclTHENLIST + [ + Proofview.V82.of_tactic (generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]); + thin [hid]; + Proofview.V82.of_tactic (Simple.intro hid); + post_tac hid + ] + g + + else tclIDTAC g | _ -> tclIDTAC g @@ -946,25 +946,25 @@ let functional_inversion kn hid fconst f_correct : Tacmach.tactic = let type_of_h = pf_unsafe_type_of g (mkVar hid) in match EConstr.kind sigma type_of_h with | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) -> - let pre_tac,f_args,res = - match EConstr.kind sigma args.(1),EConstr.kind sigma args.(2) with - | App(f,f_args),_ when EConstr.eq_constr sigma f fconst -> - ((fun hid -> Proofview.V82.of_tactic (intros_symmetry (Locusops.onHyp hid))),f_args,args.(2)) - |_,App(f,f_args) when EConstr.eq_constr sigma f fconst -> - ((fun hid -> tclIDTAC),f_args,args.(1)) - | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2) - in - tclTHENLIST [ - pre_tac hid; - Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]); - thin [hid]; - Proofview.V82.of_tactic (Simple.intro hid); + let pre_tac,f_args,res = + match EConstr.kind sigma args.(1),EConstr.kind sigma args.(2) with + | App(f,f_args),_ when EConstr.eq_constr sigma f fconst -> + ((fun hid -> Proofview.V82.of_tactic (intros_symmetry (Locusops.onHyp hid))),f_args,args.(2)) + |_,App(f,f_args) when EConstr.eq_constr sigma f fconst -> + ((fun hid -> tclIDTAC),f_args,args.(1)) + | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2) + in + tclTHENLIST [ + pre_tac hid; + Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]); + thin [hid]; + Proofview.V82.of_tactic (Simple.intro hid); Proofview.V82.of_tactic (Inv.inv Inv.FullInversion None (NamedHyp hid)); - (fun g -> - let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in - tclMAP (revert_graph kn pre_tac) (hid::new_ids) g - ); - ] g + (fun g -> + let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in + tclMAP (revert_graph kn pre_tac) (hid::new_ids) g + ); + ] g | _ -> tclFAIL 1 (mt ()) g @@ -994,46 +994,46 @@ let invfun qhyp f g = | Some f -> invfun qhyp f g | None -> Proofview.V82.of_tactic begin - Tactics.try_intros_until - (fun hid -> Proofview.V82.tactic begin fun g -> + Tactics.try_intros_until + (fun hid -> Proofview.V82.tactic begin fun g -> let sigma = project g in - let hyp_typ = pf_unsafe_type_of g (mkVar hid) in - match EConstr.kind sigma hyp_typ with - | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) -> - begin - let f1,_ = decompose_app sigma args.(1) in - try - if not (isConst sigma f1) then raise NoFunction; - let finfos = find_Function_infos (fst (destConst sigma f1)) in - let f_correct = mkConst(Option.get finfos.correctness_lemma) - and kn = fst finfos.graph_ind - in - functional_inversion kn hid f1 f_correct g - with | NoFunction | Option.IsNone | Not_found -> - try - let f2,_ = decompose_app sigma args.(2) in - if not (isConst sigma f2) then raise NoFunction; - let finfos = find_Function_infos (fst (destConst sigma f2)) in - let f_correct = mkConst(Option.get finfos.correctness_lemma) - and kn = fst finfos.graph_ind - in - functional_inversion kn hid f2 f_correct g - with - | NoFunction -> - user_err (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function") - | Option.IsNone -> - if do_observe () - then - error "Cannot use equivalence with graph for any side of the equality" - else user_err (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) - | Not_found -> - if do_observe () - then - error "No graph found for any side of equality" - else user_err (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) - end - | _ -> user_err (Ppconstr.pr_id hid ++ str " must be an equality ") - end) - qhyp + let hyp_typ = pf_unsafe_type_of g (mkVar hid) in + match EConstr.kind sigma hyp_typ with + | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) -> + begin + let f1,_ = decompose_app sigma args.(1) in + try + if not (isConst sigma f1) then raise NoFunction; + let finfos = find_Function_infos (fst (destConst sigma f1)) in + let f_correct = mkConst(Option.get finfos.correctness_lemma) + and kn = fst finfos.graph_ind + in + functional_inversion kn hid f1 f_correct g + with | NoFunction | Option.IsNone | Not_found -> + try + let f2,_ = decompose_app sigma args.(2) in + if not (isConst sigma f2) then raise NoFunction; + let finfos = find_Function_infos (fst (destConst sigma f2)) in + let f_correct = mkConst(Option.get finfos.correctness_lemma) + and kn = fst finfos.graph_ind + in + functional_inversion kn hid f2 f_correct g + with + | NoFunction -> + user_err (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function") + | Option.IsNone -> + if do_observe () + then + error "Cannot use equivalence with graph for any side of the equality" + else user_err (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) + | Not_found -> + if do_observe () + then + error "No graph found for any side of equality" + else user_err (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) + end + | _ -> user_err (Ppconstr.pr_id hid ++ str " must be an equality ") + end) + qhyp end - g + g diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 17d962f30f..2b5c0a01db 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -79,10 +79,10 @@ let def_of_const t = Const sp -> (try (match constant_opt_value_in (Global.env ()) sp with | Some c -> c - | _ -> raise Not_found) + | _ -> raise Not_found) with Not_found -> - anomaly (str "Cannot find definition of constant " ++ - (Id.print (Label.to_id (Constant.label (fst sp)))) ++ str ".") + anomaly (str "Cannot find definition of constant " ++ + (Id.print (Label.to_id (Constant.label (fst sp)))) ++ str ".") ) |_ -> assert false @@ -129,8 +129,8 @@ let lt = function () -> (coq_init_constant "lt") let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le") let ex = function () -> (coq_init_constant "ex") let nat = function () -> (coq_init_constant "nat") -let iter_ref () = - try find_reference ["Recdef"] "iter" +let iter_ref () = + try find_reference ["Recdef"] "iter" with Not_found -> user_err Pp.(str "module Recdef not loaded") let iter_rd = function () -> (constr_of_monomorphic_global (delayed_force iter_ref)) let eq = function () -> (coq_init_constant "eq") @@ -169,13 +169,13 @@ let (value_f: Constr.t list -> GlobRef.t -> Constr.t) = fun al fterm -> let rev_x_id_l = ( - List.fold_left - (fun x_id_l _ -> - let x_id = next_ident_away_in_goal x_id x_id_l in - x_id::x_id_l - ) - [] - al + List.fold_left + (fun x_id_l _ -> + let x_id = next_ident_away_in_goal x_id x_id_l in + x_id::x_id_l + ) + [] + al ) in let context = List.map @@ -185,13 +185,13 @@ let (value_f: Constr.t list -> GlobRef.t -> Constr.t) = let glob_body = DAst.make @@ GCases - (RegularStyle,None, - [DAst.make @@ GApp(DAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> DAst.make @@ GVar x_id) rev_x_id_l), - (Anonymous,None)], + (RegularStyle,None, + [DAst.make @@ GApp(DAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> DAst.make @@ GVar x_id) rev_x_id_l), + (Anonymous,None)], [CAst.make ([v_id], [DAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), - [DAst.make @@ PatVar(Name v_id); DAst.make @@ PatVar Anonymous], + [DAst.make @@ PatVar(Name v_id); DAst.make @@ PatVar Anonymous], Anonymous)], - DAst.make @@ GVar v_id)]) + DAst.make @@ GVar v_id)]) in let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in let body = EConstr.Unsafe.to_constr body in @@ -206,17 +206,17 @@ let (declare_f : Id.t -> logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t (* Debugging mechanism *) let debug_queue = Stack.create () -let print_debug_queue b e = - if not (Stack.is_empty debug_queue) +let print_debug_queue b e = + if not (Stack.is_empty debug_queue) then begin - let lmsg,goal = Stack.pop debug_queue in - if b then - Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal)) + let lmsg,goal = Stack.pop debug_queue in + if b then + Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal)) else - begin - Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal)); - end; + begin + Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal)); + end; (* print_debug_queue false e; *) end @@ -226,14 +226,14 @@ let observe strm = else () -let do_observe_tac s tac g = +let do_observe_tac s tac g = let goal = Printer.pr_goal g in let s = s (pf_env g) (project g) in - let lmsg = (str "recdef : ") ++ s in + let lmsg = (str "recdef : ") ++ s in observe (s++fnl()); Stack.push (lmsg,goal) debug_queue; - try - let v = tac g in + try + let v = tac g in ignore(Stack.pop debug_queue); v with reraise -> @@ -258,7 +258,7 @@ let observe_tclTHENLIST s tacl = in aux 0 tacl else tclTHENLIST tacl - + (* Conclusion tactics *) (* The boolean value is_mes expresses that the termination is expressed @@ -275,10 +275,10 @@ let tclUSER tac is_mes l g = if is_mes then observe_tclTHENLIST (fun _ _ -> str "tclUSER2") [ - Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force Indfun_common.ltof_ref))]); tac - ] + ] else tac ] g @@ -290,19 +290,19 @@ let tclUSER_if_not_mes concl_tac is_mes names_to_suppress = - + (* Traveling term. - Both definitions of [f_terminate] and [f_equation] use the same generic + Both definitions of [f_terminate] and [f_equation] use the same generic traveling mechanism. *) -(* [check_not_nested forbidden e] checks that [e] does not contains any variable +(* [check_not_nested forbidden e] checks that [e] does not contains any variable of [forbidden] *) let check_not_nested env sigma forbidden e = - let rec check_not_nested e = - match EConstr.kind sigma e with + let rec check_not_nested e = + match EConstr.kind sigma e with | Rel _ -> () | Int _ -> () | Var x -> @@ -319,18 +319,18 @@ let check_not_nested env sigma forbidden e = | Const _ -> () | Ind _ -> () | Construct _ -> () - | Case(_,t,e,a) -> - check_not_nested t;check_not_nested e;Array.iter check_not_nested a + | Case(_,t,e,a) -> + check_not_nested t;check_not_nested e;Array.iter check_not_nested a | Fix _ -> user_err Pp.(str "check_not_nested : Fix") | CoFix _ -> user_err Pp.(str "check_not_nested : Fix") in - try - check_not_nested e - with UserError(_,p) -> + try + check_not_nested e + with UserError(_,p) -> user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr_env env sigma e ++ str " " ++ p) (* ['a info] contains the local information for traveling *) -type 'a infos = +type 'a infos = { nb_arg : int; (* function number of arguments *) concl_tac : tactic; (* final tactic to finish proofs *) rec_arg_id : Id.t; (*name of the declared recursive argument *) @@ -343,8 +343,8 @@ type 'a infos = info : 'a; is_main_branch : bool; (* on the main branch or on a matched expression *) is_final : bool; (* final first order term or not *) - values_and_bounds : (Id.t*Id.t) list; - eqs : Id.t list; + values_and_bounds : (Id.t*Id.t) list; + eqs : Id.t list; forbidden_ids : Id.t list; acc_inv : constr lazy_t; acc_id : Id.t; @@ -352,166 +352,166 @@ type 'a infos = } -type ('a,'b) journey_info_tac = +type ('a,'b) journey_info_tac = 'a -> (* the arguments of the constructor *) 'b infos -> (* infos of the caller *) ('b infos -> tactic) -> (* the continuation tactic of the caller *) 'b infos -> (* argument of the tactic *) tactic - + (* journey_info : specifies the actions to do on the different term constructors during the traveling of the term *) -type journey_info = +type journey_info = { letiN : ((Name.t*constr*types*constr),constr) journey_info_tac; lambdA : ((Name.t*types*constr),constr) journey_info_tac; - casE : ((constr infos -> tactic) -> constr infos -> tactic) -> - ((case_info * constr * constr * constr array),constr) journey_info_tac; + casE : ((constr infos -> tactic) -> constr infos -> tactic) -> + ((case_info * constr * constr * constr array),constr) journey_info_tac; otherS : (unit,constr) journey_info_tac; apP : (constr*(constr list),constr) journey_info_tac; app_reC : (constr*(constr list),constr) journey_info_tac; message : string } - -let add_vars sigma forbidden e = + +let add_vars sigma forbidden e = let rec aux forbidden e = - match EConstr.kind sigma e with - | Var x -> x::forbidden + match EConstr.kind sigma e with + | Var x -> x::forbidden | _ -> EConstr.fold sigma aux forbidden e in aux forbidden e -let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = - fun g -> +let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = + fun g -> let rev_context,b = decompose_lam_n (project g) nb_lam e in let ids = List.fold_left (fun acc (na,_) -> - let pre_id = + let pre_id = match na.binder_name with - | Name x -> x - | Anonymous -> ano_id + | Name x -> x + | Anonymous -> ano_id in pre_id::acc - ) [] rev_context in - let rev_ids = pf_get_new_ids (List.rev ids) g in - let new_b = substl (List.map mkVar rev_ids) b in + ) [] rev_context in + let rev_ids = pf_get_new_ids (List.rev ids) g in + let new_b = substl (List.map mkVar rev_ids) b in observe_tclTHENLIST (fun _ _ -> str "treat_case1") [ - h_intros (List.rev rev_ids); - Proofview.V82.of_tactic (intro_using teq_id); - onLastHypId (fun heq -> + h_intros (List.rev rev_ids); + Proofview.V82.of_tactic (intro_using teq_id); + onLastHypId (fun heq -> observe_tclTHENLIST (fun _ _ -> str "treat_case2")[ - Proofview.V82.of_tactic (clear to_intros); - h_intros to_intros; - (fun g' -> - let ty_teq = pf_unsafe_type_of g' (mkVar heq) in - let teq_lhs,teq_rhs = - let _,args = try destApp (project g') ty_teq with DestKO -> assert false in - args.(1),args.(2) - in - let new_b' = Termops.replace_term (project g') teq_lhs teq_rhs new_b in - let new_infos = { - infos with - info = new_b'; - eqs = heq::infos.eqs; - forbidden_ids = - if forbid_new_ids - then add_vars (project g') infos.forbidden_ids new_b' - else infos.forbidden_ids - } in - finalize_tac new_infos g' - ) - ] - ) + Proofview.V82.of_tactic (clear to_intros); + h_intros to_intros; + (fun g' -> + let ty_teq = pf_unsafe_type_of g' (mkVar heq) in + let teq_lhs,teq_rhs = + let _,args = try destApp (project g') ty_teq with DestKO -> assert false in + args.(1),args.(2) + in + let new_b' = Termops.replace_term (project g') teq_lhs teq_rhs new_b in + let new_infos = { + infos with + info = new_b'; + eqs = heq::infos.eqs; + forbidden_ids = + if forbid_new_ids + then add_vars (project g') infos.forbidden_ids new_b' + else infos.forbidden_ids + } in + finalize_tac new_infos g' + ) + ] + ) ] g let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = let sigma = project g in let env = pf_env g in - match EConstr.kind sigma expr_info.info with + match EConstr.kind sigma expr_info.info with | CoFix _ | Fix _ -> user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint") | Proj _ -> user_err Pp.(str "Function cannot treat projections") | LetIn(na,b,t,e) -> begin - let new_continuation_tac = + let new_continuation_tac = jinfo.letiN (na.binder_name,b,t,e) expr_info continuation_tac - in - travel jinfo new_continuation_tac - {expr_info with info = b; is_final=false} g + in + travel jinfo new_continuation_tac + {expr_info with info = b; is_final=false} g end | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!") - | Prod _ -> + | Prod _ -> begin - try + try check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; - jinfo.otherS () expr_info continuation_tac expr_info g - with e when CErrors.noncritical e -> + jinfo.otherS () expr_info continuation_tac expr_info g + with e when CErrors.noncritical e -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env env sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) end | Lambda(n,t,b) -> begin - try + try check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; - jinfo.otherS () expr_info continuation_tac expr_info g - with e when CErrors.noncritical e -> + jinfo.otherS () expr_info continuation_tac expr_info g + with e when CErrors.noncritical e -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env env sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) end - | Case(ci,t,a,l) -> + | Case(ci,t,a,l) -> begin - let continuation_tac_a = - jinfo.casE - (travel jinfo) (ci,t,a,l) - expr_info continuation_tac in - travel - jinfo continuation_tac_a - {expr_info with info = a; is_main_branch = false; - is_final = false} g + let continuation_tac_a = + jinfo.casE + (travel jinfo) (ci,t,a,l) + expr_info continuation_tac in + travel + jinfo continuation_tac_a + {expr_info with info = a; is_main_branch = false; + is_final = false} g end - | App _ -> - let f,args = decompose_app sigma expr_info.info in - if EConstr.eq_constr sigma f (expr_info.f_constr) + | App _ -> + let f,args = decompose_app sigma expr_info.info in + if EConstr.eq_constr sigma f (expr_info.f_constr) then jinfo.app_reC (f,args) expr_info continuation_tac expr_info g else begin - match EConstr.kind sigma f with - | App _ -> assert false (* f is coming from a decompose_app *) - | Const _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ - | Sort _ | Prod _ | Var _ -> - let new_infos = {expr_info with info=(f,args)} in - let new_continuation_tac = - jinfo.apP (f,args) expr_info continuation_tac in - travel_args jinfo - expr_info.is_main_branch new_continuation_tac new_infos g + match EConstr.kind sigma f with + | App _ -> assert false (* f is coming from a decompose_app *) + | Const _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ + | Sort _ | Prod _ | Var _ -> + let new_infos = {expr_info with info=(f,args)} in + let new_continuation_tac = + jinfo.apP (f,args) expr_info continuation_tac in + travel_args jinfo + expr_info.is_main_branch new_continuation_tac new_infos g | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env env sigma expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env env sigma expr_info.info ++ Pp.str ".") end | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ -> - let new_continuation_tac = - jinfo.otherS () expr_info continuation_tac in + let new_continuation_tac = + jinfo.otherS () expr_info continuation_tac in new_continuation_tac expr_info g -and travel_args jinfo is_final continuation_tac infos = - let (f_args',args) = infos.info in - match args with - | [] -> +and travel_args jinfo is_final continuation_tac infos = + let (f_args',args) = infos.info in + match args with + | [] -> continuation_tac {infos with info = f_args'; is_final = is_final} - | arg::args' -> - let new_continuation_tac new_infos = - let new_arg = new_infos.info in - travel_args jinfo is_final - continuation_tac - {new_infos with info = (mkApp(f_args',[|new_arg|]),args')} + | arg::args' -> + let new_continuation_tac new_infos = + let new_arg = new_infos.info in + travel_args jinfo is_final + continuation_tac + {new_infos with info = (mkApp(f_args',[|new_arg|]),args')} in - travel jinfo new_continuation_tac - {infos with info=arg;is_final=false} + travel jinfo new_continuation_tac + {infos with info=arg;is_final=false} and travel jinfo continuation_tac expr_info = observe_tac (fun env sigma -> str jinfo.message ++ Printer.pr_leconstr_env env sigma expr_info.info) (travel_aux jinfo continuation_tac expr_info) -(* Termination proof *) +(* Termination proof *) -let rec prove_lt hyple g = +let rec prove_lt hyple g = let sigma = project g in begin try @@ -520,125 +520,125 @@ let rec prove_lt hyple g = | _ -> assert false in let h = - List.find (fun id -> + List.find (fun id -> match decompose_app sigma (pf_unsafe_type_of g (mkVar id)) with | _, t::_ -> EConstr.eq_constr sigma t varx | _ -> false - ) hyple + ) hyple in let y = - List.hd (List.tl (snd (decompose_app sigma (pf_unsafe_type_of g (mkVar h))))) in + List.hd (List.tl (snd (decompose_app sigma (pf_unsafe_type_of g (mkVar h))))) in observe_tclTHENLIST (fun _ _ -> str "prove_lt1")[ - Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]))); + Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]))); observe_tac (fun _ _ -> str "prove_lt") (prove_lt hyple) ] - with Not_found -> + with Not_found -> ( - ( + ( observe_tclTHENLIST (fun _ _ -> str "prove_lt2")[ - Proofview.V82.of_tactic (apply (delayed_force lt_S_n)); + Proofview.V82.of_tactic (apply (delayed_force lt_S_n)); (observe_tac (fun _ _ -> str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic assumption)) - ]) + ]) ) end g -let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = - match lbounds with - | [] -> - let ids = pf_ids_of_hyps g in - let s_max = mkApp(delayed_force coq_S, [|bound|]) in +let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = + match lbounds with + | [] -> + let ids = pf_ids_of_hyps g in + let s_max = mkApp(delayed_force coq_S, [|bound|]) in let k = next_ident_away_in_goal k_id ids in let ids = k::ids in let h' = next_ident_away_in_goal (h'_id) ids in let ids = h'::ids in let def = next_ident_away_in_goal def_id ids in observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux1")[ - Proofview.V82.of_tactic (split (ImplicitBindings [s_max])); - Proofview.V82.of_tactic (intro_then - (fun id -> + Proofview.V82.of_tactic (split (ImplicitBindings [s_max])); + Proofview.V82.of_tactic (intro_then + (fun id -> Proofview.V82.tactic begin observe_tac (fun _ _ -> str "destruct_bounds_aux") - (tclTHENS (Proofview.V82.of_tactic (simplest_case (mkVar id))) - [ + (tclTHENS (Proofview.V82.of_tactic (simplest_case (mkVar id))) + [ observe_tclTHENLIST (fun _ _ -> str "")[Proofview.V82.of_tactic (intro_using h_id); - Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|]))); - Proofview.V82.of_tactic default_full_auto]; + Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|]))); + Proofview.V82.of_tactic default_full_auto]; observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux2")[ observe_tac (fun _ _ -> str "clearing k ") (Proofview.V82.of_tactic (clear [id])); - h_intros [k;h';def]; + h_intros [k;h';def]; observe_tac (fun _ _ -> str "simple_iter") (Proofview.V82.of_tactic (simpl_iter Locusops.onConcl)); observe_tac (fun _ _ -> str "unfold functional") - (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1], - evaluable_of_global_reference infos.func)])); - ( + (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1], + evaluable_of_global_reference infos.func)])); + ( observe_tclTHENLIST (fun _ _ -> str "test")[ - list_rewrite true - (List.fold_right - (fun e acc -> (mkVar e,true)::acc) - infos.eqs - (List.map (fun e -> (e,true)) rechyps) - ); - (* list_rewrite true *) - (* (List.map (fun e -> (mkVar e,true)) infos.eqs) *) - (* ; *) - + list_rewrite true + (List.fold_right + (fun e acc -> (mkVar e,true)::acc) + infos.eqs + (List.map (fun e -> (e,true)) rechyps) + ); + (* list_rewrite true *) + (* (List.map (fun e -> (mkVar e,true)) infos.eqs) *) + (* ; *) + (observe_tac (fun _ _ -> str "finishing") - (tclORELSE - (Proofview.V82.of_tactic intros_reflexivity) + (tclORELSE + (Proofview.V82.of_tactic intros_reflexivity) (observe_tac (fun _ _ -> str "calling prove_lt") (prove_lt hyple))))]) - ] - ] - )end)) - ] g - | (_,v_bound)::l -> + ] + ] + )end)) + ] g + | (_,v_bound)::l -> observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux3")[ - Proofview.V82.of_tactic (simplest_elim (mkVar v_bound)); - Proofview.V82.of_tactic (clear [v_bound]); - tclDO 2 (Proofview.V82.of_tactic intro); - onNthHypId 1 - (fun p_hyp -> - (onNthHypId 2 - (fun p -> + Proofview.V82.of_tactic (simplest_elim (mkVar v_bound)); + Proofview.V82.of_tactic (clear [v_bound]); + tclDO 2 (Proofview.V82.of_tactic intro); + onNthHypId 1 + (fun p_hyp -> + (onNthHypId 2 + (fun p -> observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux4")[ - Proofview.V82.of_tactic (simplest_elim - (mkApp(delayed_force max_constr, [| bound; mkVar p|]))); - tclDO 3 (Proofview.V82.of_tactic intro); - onNLastHypsId 3 (fun lids -> - match lids with - [hle2;hle1;pmax] -> - destruct_bounds_aux infos - ((mkVar pmax), - hle1::hle2::hyple,(mkVar p_hyp)::rechyps) - l - | _ -> assert false) ; - ] - ) - ) - ) + Proofview.V82.of_tactic (simplest_elim + (mkApp(delayed_force max_constr, [| bound; mkVar p|]))); + tclDO 3 (Proofview.V82.of_tactic intro); + onNLastHypsId 3 (fun lids -> + match lids with + [hle2;hle1;pmax] -> + destruct_bounds_aux infos + ((mkVar pmax), + hle1::hle2::hyple,(mkVar p_hyp)::rechyps) + l + | _ -> assert false) ; + ] + ) + ) + ) ] g -let destruct_bounds infos = +let destruct_bounds infos = destruct_bounds_aux infos (delayed_force coq_O,[],[]) infos.values_and_bounds -let terminate_app f_and_args expr_info continuation_tac infos = - if expr_info.is_final && expr_info.is_main_branch - then +let terminate_app f_and_args expr_info continuation_tac infos = + if expr_info.is_final && expr_info.is_main_branch + then observe_tclTHENLIST (fun _ _ -> str "terminate_app1")[ - continuation_tac infos; + continuation_tac infos; observe_tac (fun _ _ -> str "first split") - (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info]))); + (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info]))); observe_tac (fun _ _ -> str "destruct_bounds (1)") (destruct_bounds infos) ] else continuation_tac infos -let terminate_others _ expr_info continuation_tac infos = - if expr_info.is_final && expr_info.is_main_branch - then +let terminate_others _ expr_info continuation_tac infos = + if expr_info.is_final && expr_info.is_main_branch + then observe_tclTHENLIST (fun _ _ -> str "terminate_others")[ - continuation_tac infos; + continuation_tac infos; observe_tac (fun _ _ -> str "first split") - (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info]))); + (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info]))); observe_tac (fun _ _ -> str "destruct_bounds") (destruct_bounds infos) ] else continuation_tac infos @@ -646,24 +646,24 @@ let terminate_others _ expr_info continuation_tac infos = let terminate_letin (na,b,t,e) expr_info continuation_tac info g = let sigma = project g in let env = pf_env g in - let new_e = subst1 info.info e in - let new_forbidden = - let forbid = - try + let new_e = subst1 info.info e in + let new_forbidden = + let forbid = + try check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids) b; - true + true with e when CErrors.noncritical e -> false in - if forbid - then + if forbid + then match na with - | Anonymous -> info.forbidden_ids - | Name id -> id::info.forbidden_ids - else info.forbidden_ids + | Anonymous -> info.forbidden_ids + | Name id -> id::info.forbidden_ids + else info.forbidden_ids in continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} g -let pf_type c tac gl = +let pf_type c tac gl = let evars, ty = Typing.type_of (pf_env gl) (project gl) c in tclTHEN (Refiner.tclEVARS evars) (tac ty) gl @@ -704,7 +704,6 @@ let mkDestructEq : Proofview.V82.of_tactic (change_in_concl ~check:true None changefun) g2); Proofview.V82.of_tactic (simplest_case expr)]), to_revert - let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = let sigma = project g in let env = pf_env g in @@ -721,104 +720,104 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = info = mkCase(ci,t,a',l); is_main_branch = expr_info.is_main_branch; is_final = expr_info.is_final} in - let destruct_tac,rev_to_thin_intro = - mkDestructEq [expr_info.rec_arg_id] a' g in - let to_thin_intro = List.rev rev_to_thin_intro in + let destruct_tac,rev_to_thin_intro = + mkDestructEq [expr_info.rec_arg_id] a' g in + let to_thin_intro = List.rev rev_to_thin_intro in observe_tac (fun _ _ -> str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a') (try (tclTHENS - destruct_tac + destruct_tac (List.map_i (fun i e -> observe_tac (fun _ _ -> str "do treat case") (treat_case f_is_present to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l) - )) - with - | UserError(Some "Refiner.thensn_tac3",_) + )) + with + | UserError(Some "Refiner.thensn_tac3",_) | UserError(Some "Refiner.tclFAIL_s",_) -> (observe_tac (fun _ _ -> str "is computable " ++ Printer.pr_leconstr_env env sigma new_info.info) (next_step continuation_tac {new_info with info = Reductionops.nf_betaiotazeta (pf_env g) sigma new_info.info} ) - )) + )) g - + let terminate_app_rec (f,args) expr_info continuation_tac _ g = let sigma = project g in let env = pf_env g in List.iter (check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids)) args; begin - try + try let v = List.assoc_f (List.equal (EConstr.eq_constr sigma)) args expr_info.args_assoc in - let new_infos = {expr_info with info = v} in + let new_infos = {expr_info with info = v} in observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec")[ - continuation_tac new_infos; - if expr_info.is_final && expr_info.is_main_branch - then + continuation_tac new_infos; + if expr_info.is_final && expr_info.is_main_branch + then observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec1")[ observe_tac (fun _ _ -> str "first split") - (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info]))); + (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info]))); observe_tac (fun _ _ -> str "destruct_bounds (3)") - (destruct_bounds new_infos) - ] - else - tclIDTAC + (destruct_bounds new_infos) + ] + else + tclIDTAC ] g - with Not_found -> + with Not_found -> observe_tac (fun _ _ -> str "terminate_app_rec not found") (tclTHENS - (Proofview.V82.of_tactic (simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args)))) - [ + (Proofview.V82.of_tactic (simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args)))) + [ observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec2")[ - Proofview.V82.of_tactic (intro_using rec_res_id); - Proofview.V82.of_tactic intro; - onNthHypId 1 - (fun v_bound -> - (onNthHypId 2 - (fun v -> - let new_infos = { expr_info with - info = (mkVar v); - values_and_bounds = - (v,v_bound)::expr_info.values_and_bounds; - args_assoc=(args,mkVar v)::expr_info.args_assoc - } in + Proofview.V82.of_tactic (intro_using rec_res_id); + Proofview.V82.of_tactic intro; + onNthHypId 1 + (fun v_bound -> + (onNthHypId 2 + (fun v -> + let new_infos = { expr_info with + info = (mkVar v); + values_and_bounds = + (v,v_bound)::expr_info.values_and_bounds; + args_assoc=(args,mkVar v)::expr_info.args_assoc + } in observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec3")[ - continuation_tac new_infos; - if expr_info.is_final && expr_info.is_main_branch - then + continuation_tac new_infos; + if expr_info.is_final && expr_info.is_main_branch + then observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec4")[ observe_tac (fun _ _ -> str "first split") - (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info]))); + (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info]))); observe_tac (fun _ _ -> str "destruct_bounds (2)") - (destruct_bounds new_infos) - ] - else - tclIDTAC - ] - ) - ) - ) - ]; + (destruct_bounds new_infos) + ] + else + tclIDTAC + ] + ) + ) + ) + ]; observe_tac (fun _ _ -> str "proving decreasing") ( - tclTHENS (* proof of args < formal args *) - (Proofview.V82.of_tactic (apply (Lazy.force expr_info.acc_inv))) - [ + tclTHENS (* proof of args < formal args *) + (Proofview.V82.of_tactic (apply (Lazy.force expr_info.acc_inv))) + [ observe_tac (fun _ _ -> str "assumption") (Proofview.V82.of_tactic assumption); observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec5") - [ - tclTRY(list_rewrite true - (List.map - (fun e -> mkVar e,true) - expr_info.eqs - ) - ); - tclUSER expr_info.concl_tac true - (Some ( - expr_info.ih::expr_info.acc_id:: - (fun (x,y) -> y) - (List.split expr_info.values_and_bounds) - ) - ); - ] - ]) - ]) g + [ + tclTRY(list_rewrite true + (List.map + (fun e -> mkVar e,true) + expr_info.eqs + ) + ); + tclUSER expr_info.concl_tac true + (Some ( + expr_info.ih::expr_info.acc_id:: + (fun (x,y) -> y) + (List.split expr_info.values_and_bounds) + ) + ); + ] + ]) + ]) g end -let terminate_info = +let terminate_info = { message = "prove_terminate with term "; letiN = terminate_letin; lambdA = (fun _ _ _ _ -> assert false); @@ -833,15 +832,15 @@ let prove_terminate = travel terminate_info (* Equation proof *) -let equation_case next_step (ci,a,t,l) expr_info continuation_tac infos = +let equation_case next_step (ci,a,t,l) expr_info continuation_tac infos = observe_tac (fun _ _ -> str "equation case") (terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos) -let rec prove_le g = +let rec prove_le g = let sigma = project g in - let x,z = - let _,args = decompose_app sigma (pf_concl g) in + let x,z = + let _,args = decompose_app sigma (pf_concl g) in (List.hd args,List.hd (List.tl args)) - in + in tclFIRST[ Proofview.V82.of_tactic assumption; Proofview.V82.of_tactic (apply (delayed_force le_n)); @@ -856,151 +855,151 @@ let rec prove_le g = in let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in let h = h.binder_name in - let y = - let _,args = decompose_app sigma t in - List.hd (List.tl args) - in + let y = + let _,args = decompose_app sigma t in + List.hd (List.tl args) + in observe_tclTHENLIST (fun _ _ -> str "prove_le")[ - Proofview.V82.of_tactic (apply(mkApp(le_trans (),[|x;y;z;mkVar h|]))); + Proofview.V82.of_tactic (apply(mkApp(le_trans (),[|x;y;z;mkVar h|]))); observe_tac (fun _ _ -> str "prove_le (rec)") (prove_le) - ] + ] with Not_found -> tclFAIL 0 (mt()) end; ] g -let rec make_rewrite_list expr_info max = function +let rec make_rewrite_list expr_info max = function | [] -> tclIDTAC - | (_,p,hp)::l -> + | (_,p,hp)::l -> observe_tac (fun _ _ -> str "make_rewrite_list") (tclTHENS (observe_tac (fun _ _ -> str "rewrite heq on " ++ Id.print p ) ( - (fun g -> + (fun g -> let sigma = project g in - let t_eq = compute_renamed_type g (mkVar hp) in - let k,def = + let t_eq = compute_renamed_type g (mkVar hp) in + let k,def = let k_na,_,t = destProd sigma t_eq in let _,_,t = destProd sigma t in let def_na,_,_ = destProd sigma t in Nameops.Name.get_id k_na.binder_name,Nameops.Name.get_id def_na.binder_name - in - Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences - true (* dep proofs also: *) true - (mkVar hp, + in + Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences + true (* dep proofs also: *) true + (mkVar hp, ExplicitBindings[CAst.make @@ (NamedHyp def, expr_info.f_constr); CAst.make @@ (NamedHyp k, f_S max)]) false) g) ) ) [make_rewrite_list expr_info max l; observe_tclTHENLIST (fun _ _ -> str "make_rewrite_list")[ (* x < S max proof *) - Proofview.V82.of_tactic (apply (delayed_force le_lt_n_Sm)); + Proofview.V82.of_tactic (apply (delayed_force le_lt_n_Sm)); observe_tac (fun _ _ -> str "prove_le(2)") prove_le ] ] ) -let make_rewrite expr_info l hp max = +let make_rewrite expr_info l hp max = tclTHENFIRST (observe_tac (fun _ _ -> str "make_rewrite") (make_rewrite_list expr_info max l)) (observe_tac (fun _ _ -> str "make_rewrite") (tclTHENS - (fun g -> + (fun g -> let sigma = project g in - let t_eq = compute_renamed_type g (mkVar hp) in - let k,def = + let t_eq = compute_renamed_type g (mkVar hp) in + let k,def = let k_na,_,t = destProd sigma t_eq in let _,_,t = destProd sigma t in let def_na,_,_ = destProd sigma t in Nameops.Name.get_id k_na.binder_name,Nameops.Name.get_id def_na.binder_name - in + in observe_tac (fun _ _ -> str "general_rewrite_bindings") - (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences - true (* dep proofs also: *) true - (mkVar hp, + (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences + true (* dep proofs also: *) true + (mkVar hp, ExplicitBindings[CAst.make @@ (NamedHyp def, expr_info.f_constr); CAst.make @@ (NamedHyp k, f_S (f_S max))]) false)) g) [observe_tac(fun _ _ -> str "make_rewrite finalize") ( - (* tclORELSE( h_reflexivity) *) + (* tclORELSE( h_reflexivity) *) (observe_tclTHENLIST (fun _ _ -> str "make_rewrite")[ - Proofview.V82.of_tactic (simpl_iter Locusops.onConcl); + Proofview.V82.of_tactic (simpl_iter Locusops.onConcl); observe_tac (fun _ _ -> str "unfold functional") - (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1], - evaluable_of_global_reference expr_info.func)])); - - (list_rewrite true - (List.map (fun e -> mkVar e,true) expr_info.eqs)); + (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1], + evaluable_of_global_reference expr_info.func)])); + + (list_rewrite true + (List.map (fun e -> mkVar e,true) expr_info.eqs)); (observe_tac (fun _ _ -> str "h_reflexivity") - (Proofview.V82.of_tactic intros_reflexivity) - ) - ])) + (Proofview.V82.of_tactic intros_reflexivity) + ) + ])) ; observe_tclTHENLIST (fun _ _ -> str "make_rewrite1")[ (* x < S (S max) proof *) - Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force le_lt_SS))); + Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force le_lt_SS))); observe_tac (fun _ _ -> str "prove_le (3)") prove_le - ] - ]) + ] + ]) ) -let rec compute_max rew_tac max l = - match l with +let rec compute_max rew_tac max l = + match l with | [] -> rew_tac max - | (_,p,_)::l -> + | (_,p,_)::l -> observe_tclTHENLIST (fun _ _ -> str "compute_max")[ - Proofview.V82.of_tactic (simplest_elim - (mkApp(delayed_force max_constr, [| max; mkVar p|]))); - tclDO 3 (Proofview.V82.of_tactic intro); - onNLastHypsId 3 (fun lids -> - match lids with - | [hle2;hle1;pmax] -> compute_max rew_tac (mkVar pmax) l - | _ -> assert false - )] - -let rec destruct_hex expr_info acc l = - match l with - | [] -> + Proofview.V82.of_tactic (simplest_elim + (mkApp(delayed_force max_constr, [| max; mkVar p|]))); + tclDO 3 (Proofview.V82.of_tactic intro); + onNLastHypsId 3 (fun lids -> + match lids with + | [hle2;hle1;pmax] -> compute_max rew_tac (mkVar pmax) l + | _ -> assert false + )] + +let rec destruct_hex expr_info acc l = + match l with + | [] -> begin - match List.rev acc with - | [] -> tclIDTAC - | (_,p,hp)::tl -> + match List.rev acc with + | [] -> tclIDTAC + | (_,p,hp)::tl -> observe_tac (fun _ _ -> str "compute max ") (compute_max (make_rewrite expr_info tl hp) (mkVar p) tl) end - | (v,hex)::l -> + | (v,hex)::l -> observe_tclTHENLIST (fun _ _ -> str "destruct_hex")[ - Proofview.V82.of_tactic (simplest_case (mkVar hex)); - Proofview.V82.of_tactic (clear [hex]); - tclDO 2 (Proofview.V82.of_tactic intro); - onNthHypId 1 (fun hp -> - onNthHypId 2 (fun p -> - observe_tac + Proofview.V82.of_tactic (simplest_case (mkVar hex)); + Proofview.V82.of_tactic (clear [hex]); + tclDO 2 (Proofview.V82.of_tactic intro); + onNthHypId 1 (fun hp -> + onNthHypId 2 (fun p -> + observe_tac (fun _ _ -> str "destruct_hex after " ++ Id.print hp ++ spc () ++ Id.print p) - (destruct_hex expr_info ((v,p,hp)::acc) l) - ) - ) + (destruct_hex expr_info ((v,p,hp)::acc) l) + ) + ) ] - -let rec intros_values_eq expr_info acc = + +let rec intros_values_eq expr_info acc = tclORELSE( observe_tclTHENLIST (fun _ _ -> str "intros_values_eq")[ tclDO 2 (Proofview.V82.of_tactic intro); - onNthHypId 1 (fun hex -> - (onNthHypId 2 (fun v -> intros_values_eq expr_info ((v,hex)::acc))) + onNthHypId 1 (fun hex -> + (onNthHypId 2 (fun v -> intros_values_eq expr_info ((v,hex)::acc))) ) ]) (tclCOMPLETE ( destruct_hex expr_info [] acc )) -let equation_others _ expr_info continuation_tac infos = - if expr_info.is_final && expr_info.is_main_branch +let equation_others _ expr_info continuation_tac infos = + if expr_info.is_final && expr_info.is_main_branch then observe_tac (fun env sigma -> str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr_env env sigma expr_info.info) - (tclTHEN - (continuation_tac infos) + (tclTHEN + (continuation_tac infos) (observe_tac (fun env sigma -> str "intros_values_eq equation_others " ++ Printer.pr_leconstr_env env sigma expr_info.info) (intros_values_eq expr_info []))) else observe_tac (fun env sigma -> str "equation_others (cont_tac) " ++ Printer.pr_leconstr_env env sigma expr_info.info) (continuation_tac infos) -let equation_app f_and_args expr_info continuation_tac infos = - if expr_info.is_final && expr_info.is_main_branch +let equation_app f_and_args expr_info continuation_tac infos = + if expr_info.is_final && expr_info.is_main_branch then ((observe_tac (fun _ _ -> str "intros_values_eq equation_app") (intros_values_eq expr_info []))) else continuation_tac infos - -let equation_app_rec (f,args) expr_info continuation_tac info g = + +let equation_app_rec (f,args) expr_info continuation_tac info g = let sigma = project g in begin try @@ -1008,21 +1007,21 @@ let equation_app_rec (f,args) expr_info continuation_tac info g = let new_infos = {expr_info with info = v} in observe_tac (fun _ _ -> str "app_rec found") (continuation_tac new_infos) g with Not_found -> - if expr_info.is_final && expr_info.is_main_branch - then + if expr_info.is_final && expr_info.is_main_branch + then observe_tclTHENLIST (fun _ _ -> str "equation_app_rec") - [ Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args))); - continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc}; + [ Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args))); + continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc}; observe_tac (fun _ _ -> str "app_rec intros_values_eq") (intros_values_eq expr_info []) - ] g - else + ] g + else observe_tclTHENLIST (fun _ _ -> str "equation_app_rec1")[ - Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args))); + Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args))); observe_tac (fun _ _ -> str "app_rec not_found") (continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc}) - ] g + ] g end -let equation_info = +let equation_info = {message = "prove_equation with term "; letiN = (fun _ -> assert false); lambdA = (fun _ _ _ _ -> assert false); @@ -1031,7 +1030,7 @@ let equation_info = apP = equation_app; app_reC = equation_app_rec } - + let prove_eq = travel equation_info (* wrappers *) @@ -1045,12 +1044,12 @@ let compute_terminate_type nb_args func = let rev_args,b = decompose_prod_n nb_args a_arrow_b in let left = mkApp(delayed_force iter_rd, - Array.of_list - (lift 5 a_arrow_b:: mkRel 3:: + Array.of_list + (lift 5 a_arrow_b:: mkRel 3:: constr_of_monomorphic_global func::mkRel 1:: - List.rev (List.map_i (fun i _ -> mkRel (6+i)) 0 rev_args) - ) - ) + List.rev (List.map_i (fun i _ -> mkRel (6+i)) 0 rev_args) + ) + ) in let right = mkRel 5 in let delayed_force c = EConstr.Unsafe.to_constr (delayed_force c) in @@ -1059,14 +1058,14 @@ let compute_terminate_type nb_args func = let cond = mkApp(delayed_force lt, [|(mkRel 2); (mkRel 1)|]) in let nb_iter = mkApp(delayed_force ex, - [|delayed_force nat; - (mkLambda + [|delayed_force nat; + (mkLambda (make_annot (Name p_id) Sorts.Relevant, - delayed_force nat, + delayed_force nat, (mkProd (make_annot (Name k_id) Sorts.Relevant, delayed_force nat, mkArrow cond Sorts.Relevant result))))|])in let value = mkApp(constr_of_monomorphic_global (Util.delayed_force coq_sig_ref), - [|b; + [|b; (mkLambda (make_annot (Name v_id) Sorts.Relevant, b, nb_iter))|]) in compose_prod rev_args value @@ -1077,74 +1076,74 @@ let termination_proof_header is_mes input_type ids args_id relation fun g -> let nargs = List.length args_id in let pre_rec_args = - List.rev_map - mkVar (fst (List.chop (rec_arg_num - 1) args_id)) + List.rev_map + mkVar (fst (List.chop (rec_arg_num - 1) args_id)) in let relation = substl pre_rec_args relation in let input_type = substl pre_rec_args input_type in let wf_thm = next_ident_away_in_goal (Id.of_string ("wf_R")) ids in let wf_rec_arg = - next_ident_away_in_goal - (Id.of_string ("Acc_"^(Id.to_string rec_arg_id))) - (wf_thm::ids) + next_ident_away_in_goal + (Id.of_string ("Acc_"^(Id.to_string rec_arg_id))) + (wf_thm::ids) in let hrec = next_ident_away_in_goal hrec_id - (wf_rec_arg::wf_thm::ids) in + (wf_rec_arg::wf_thm::ids) in let acc_inv = - lazy ( - mkApp ( - delayed_force acc_inv_id, - [|input_type;relation;mkVar rec_arg_id|] - ) - ) + lazy ( + mkApp ( + delayed_force acc_inv_id, + [|input_type;relation;mkVar rec_arg_id|] + ) + ) in tclTHEN - (h_intros args_id) - (tclTHENS - (observe_tac + (h_intros args_id) + (tclTHENS + (observe_tac (fun _ _ -> str "first assert") - (Proofview.V82.of_tactic (assert_before - (Name wf_rec_arg) - (mkApp (delayed_force acc_rel, - [|input_type;relation;mkVar rec_arg_id|]) - ) - )) - ) - [ - (* accesibility proof *) - tclTHENS - (observe_tac + (Proofview.V82.of_tactic (assert_before + (Name wf_rec_arg) + (mkApp (delayed_force acc_rel, + [|input_type;relation;mkVar rec_arg_id|]) + ) + )) + ) + [ + (* accesibility proof *) + tclTHENS + (observe_tac (fun _ _ -> str "second assert") - (Proofview.V82.of_tactic (assert_before - (Name wf_thm) - (mkApp (delayed_force well_founded,[|input_type;relation|])) - )) - ) - [ - (* interactive proof that the relation is well_founded *) + (Proofview.V82.of_tactic (assert_before + (Name wf_thm) + (mkApp (delayed_force well_founded,[|input_type;relation|])) + )) + ) + [ + (* interactive proof that the relation is well_founded *) observe_tac (fun _ _ -> str "wf_tac") (wf_tac is_mes (Some args_id)); - (* this gives the accessibility argument *) - observe_tac + (* this gives the accessibility argument *) + observe_tac (fun _ _ -> str "apply wf_thm") - (Proofview.V82.of_tactic (Simple.apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|]))) - ) - ] - ; - (* rest of the proof *) + (Proofview.V82.of_tactic (Simple.apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|]))) + ) + ] + ; + (* rest of the proof *) observe_tclTHENLIST (fun _ _ -> str "rest of proof") [observe_tac (fun _ _ -> str "generalize") - (onNLastHypsId (nargs+1) - (tclMAP (fun id -> - tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id]))) - )) - ; + (onNLastHypsId (nargs+1) + (tclMAP (fun id -> + tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id]))) + )) + ; observe_tac (fun _ _ -> str "fix") (Proofview.V82.of_tactic (fix hrec (nargs+1))); - h_intros args_id; - Proofview.V82.of_tactic (Simple.intro wf_rec_arg); + h_intros args_id; + Proofview.V82.of_tactic (Simple.intro wf_rec_arg); observe_tac (fun _ _ -> str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv) - ] - ] - ) g + ] + ] + ) g end @@ -1166,58 +1165,58 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a let (f_name, _, body1) = destLambda sigma func_body in let f_id = match f_name.binder_name with - | Name f_id -> next_ident_away_in_goal f_id ids - | Anonymous -> anomaly (Pp.str "Anonymous function.") + | Name f_id -> next_ident_away_in_goal f_id ids + | Anonymous -> anomaly (Pp.str "Anonymous function.") in let n_names_types,_ = decompose_lam_n sigma nb_args body1 in let n_ids,ids = - List.fold_left + List.fold_left (fun (n_ids,ids) (n_name,_) -> match n_name.binder_name with - | Name id -> - let n_id = next_ident_away_in_goal id ids in - n_id::n_ids,n_id::ids - | _ -> anomaly (Pp.str "anonymous argument.") - ) - ([],(f_id::ids)) - n_names_types + | Name id -> + let n_id = next_ident_away_in_goal id ids in + n_id::n_ids,n_id::ids + | _ -> anomaly (Pp.str "anonymous argument.") + ) + ([],(f_id::ids)) + n_names_types in let rec_arg_id = List.nth n_ids (rec_arg_num - 1) in let expr = instantiate_lambda sigma func_body (mkVar f_id::(List.map mkVar n_ids)) in termination_proof_header - is_mes - input_type - ids - n_ids - relation - rec_arg_num - rec_arg_id - (fun rec_arg_id hrec acc_id acc_inv g -> - (prove_terminate (fun infos -> tclIDTAC) - { is_main_branch = true; (* we are on the main branche (i.e. still on a match ... with .... end *) - is_final = true; (* and on leaf (more or less) *) - f_terminate = delayed_force coq_O; - nb_arg = nb_args; - concl_tac = concl_tac; - rec_arg_id = rec_arg_id; - is_mes = is_mes; - ih = hrec; - f_id = f_id; - f_constr = mkVar f_id; - func = func; - info = expr; - acc_inv = acc_inv; - acc_id = acc_id; - values_and_bounds = []; - eqs = []; - forbidden_ids = []; - args_assoc = [] - } - ) - g - ) - (tclUSER_if_not_mes concl_tac) - g + is_mes + input_type + ids + n_ids + relation + rec_arg_num + rec_arg_id + (fun rec_arg_id hrec acc_id acc_inv g -> + (prove_terminate (fun infos -> tclIDTAC) + { is_main_branch = true; (* we are on the main branche (i.e. still on a match ... with .... end *) + is_final = true; (* and on leaf (more or less) *) + f_terminate = delayed_force coq_O; + nb_arg = nb_args; + concl_tac = concl_tac; + rec_arg_id = rec_arg_id; + is_mes = is_mes; + ih = hrec; + f_id = f_id; + f_constr = mkVar f_id; + func = func; + info = expr; + acc_inv = acc_inv; + acc_id = acc_id; + values_and_bounds = []; + eqs = []; + forbidden_ids = []; + args_assoc = [] + } + ) + g + ) + (tclUSER_if_not_mes concl_tac) + g end let get_current_subgoals_types pstate = @@ -1231,32 +1230,32 @@ let build_and_l sigma l = let conj_constr = Coqlib.build_coq_conj () in let mk_and p1 p2 = mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in - let rec is_well_founded t = - match EConstr.kind sigma t with + let rec is_well_founded t = + match EConstr.kind sigma t with | Prod(_,_,t') -> is_well_founded t' - | App(_,_) -> - let (f,_) = decompose_app sigma t in - EConstr.eq_constr sigma f (well_founded ()) - | _ -> - false + | App(_,_) -> + let (f,_) = decompose_app sigma t in + EConstr.eq_constr sigma f (well_founded ()) + | _ -> + false in - let compare t1 t2 = - let b1,b2= is_well_founded t1,is_well_founded t2 in + let compare t1 t2 = + let b1,b2= is_well_founded t1,is_well_founded t2 in if (b1&&b2) || not (b1 || b2) then 0 else if b1 && not b2 then 1 else -1 in - let l = List.sort compare l in + let l = List.sort compare l in let rec f = function | [] -> raise EmptySubgoals | [p] -> p,tclIDTAC,1 | p1::pl -> - let c,tac,nb = f pl in - mk_and p1 c, - tclTHENS + let c,tac,nb = f pl in + mk_and p1 c, + tclTHENS (Proofview.V82.of_tactic (apply (EConstr.of_constr (constr_of_monomorphic_global conj_constr)))) - [tclIDTAC; - tac - ],nb+1 + [tclIDTAC; + tac + ],nb+1 in f l @@ -1266,15 +1265,15 @@ let is_rec_res id = try String.equal (String.sub id_name 0 (String.length rec_res_name)) rec_res_name with Invalid_argument _ -> false - + let clear_goals sigma = let rec clear_goal t = match EConstr.kind sigma t with | Prod({binder_name=Name id} as na,t',b) -> - let b' = clear_goal b in - if noccurn sigma 1 b' && (is_rec_res id) - then Vars.lift (-1) b' - else if b' == b then t + let b' = clear_goal b in + if noccurn sigma 1 b' && (is_rec_res id) + then Vars.lift (-1) b' + else if b' == b then t else mkProd(na,t',b') | _ -> EConstr.map sigma clear_goal t in @@ -1303,8 +1302,8 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type let name = match goal_name with | Some s -> s | None -> - try add_suffix current_proof_name "_subproof" - with e when CErrors.noncritical e -> + try add_suffix current_proof_name "_subproof" + with e when CErrors.noncritical e -> anomaly (Pp.str "open_new_goal with an unnamed theorem.") in let na = next_global_ident_away name Id.Set.empty in @@ -1315,8 +1314,8 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type let na_ref = qualid_of_ident na in let na_global = Smartlocate.global_with_alias na_ref in match na_global with - ConstRef c -> is_opaque_constant c - | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant.") + ConstRef c -> is_opaque_constant c + | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant.") in let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in ref_ := Value (EConstr.Unsafe.to_constr lemma); @@ -1325,47 +1324,47 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type let env = Global.env () in let lemma = build_proof env (Evd.from_env env) ( fun gls -> - let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in + let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in observe_tclTHENLIST (fun _ _ -> str "") - [ - Proofview.V82.of_tactic (generalize [lemma]); - Proofview.V82.of_tactic (Simple.intro hid); - (fun g -> - let ids = pf_ids_of_hyps g in - tclTHEN - (Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid))) - (fun g -> - let ids' = pf_ids_of_hyps g in - lid := List.rev (List.subtract Id.equal ids' ids); - if List.is_empty !lid then lid := [hid]; - tclIDTAC g - ) - g - ); - ] gls) + [ + Proofview.V82.of_tactic (generalize [lemma]); + Proofview.V82.of_tactic (Simple.intro hid); + (fun g -> + let ids = pf_ids_of_hyps g in + tclTHEN + (Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid))) + (fun g -> + let ids' = pf_ids_of_hyps g in + lid := List.rev (List.subtract Id.equal ids' ids); + if List.is_empty !lid then lid := [hid]; + tclIDTAC g + ) + g + ); + ] gls) (fun g -> let sigma = project g in - match EConstr.kind sigma (pf_concl g) with - | App(f,_) when EConstr.eq_constr sigma f (well_founded ()) -> - Proofview.V82.of_tactic (Auto.h_auto None [] (Some [])) g - | _ -> - incr h_num; + match EConstr.kind sigma (pf_concl g) with + | App(f,_) when EConstr.eq_constr sigma f (well_founded ()) -> + Proofview.V82.of_tactic (Auto.h_auto None [] (Some [])) g + | _ -> + incr h_num; (observe_tac (fun _ _ -> str "finishing using") - ( - tclCOMPLETE( - tclFIRST[ - tclTHEN - (Proofview.V82.of_tactic (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))) - (Proofview.V82.of_tactic e_assumption); - Eauto.eauto_with_bases - (true,5) - [(fun _ sigma -> (sigma, (Lazy.force refl_equal)))] + ( + tclCOMPLETE( + tclFIRST[ + tclTHEN + (Proofview.V82.of_tactic (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))) + (Proofview.V82.of_tactic e_assumption); + Eauto.eauto_with_bases + (true,5) + [(fun _ sigma -> (sigma, (Lazy.force refl_equal)))] [Hints.Hint_db.empty TransparentState.empty false] - ] - ) - ) - ) - g) + ] + ) + ) + ) + g) in Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None in @@ -1376,23 +1375,23 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type let lemma = if Indfun_common.is_strict_tcc () then fst @@ Lemmas.by (Proofview.V82.tactic (tclIDTAC)) lemma - else + else fst @@ Lemmas.by (Proofview.V82.tactic begin - fun g -> - tclTHEN - (decompose_and_tac) - (tclORELSE - (tclFIRST - (List.map - (fun c -> - Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST - [intros; + fun g -> + tclTHEN + (decompose_and_tac) + (tclORELSE + (tclFIRST + (List.map + (fun c -> + Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST + [intros; Simple.apply (fst (interp_constr (Global.env()) Evd.empty c)) (*FIXME*); - Tacticals.New.tclCOMPLETE Auto.default_auto - ]) - ) - using_lemmas) - ) tclIDTAC) + Tacticals.New.tclCOMPLETE Auto.default_auto + ]) + ) + using_lemmas) + ) tclIDTAC) g end) lemma in if Lemmas.(pf_fold Proof_global.get_open_goals) lemma = 0 then (defined lemma; None) else Some lemma @@ -1451,8 +1450,8 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation let open CVars in let opacity = match terminate_ref with - | ConstRef c -> is_opaque_constant c - | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") + | ConstRef c -> is_opaque_constant c + | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in let evd = Evd.from_ctx uctx in let f_constr = constr_of_monomorphic_global f_ref in @@ -1461,31 +1460,31 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation (EConstr.of_constr equation_lemma_type) in let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (start_equation f_ref terminate_ref - (fun x -> - prove_eq (fun _ -> tclIDTAC) - {nb_arg=nb_arg; + (fun x -> + prove_eq (fun _ -> tclIDTAC) + {nb_arg=nb_arg; f_terminate = EConstr.of_constr (constr_of_monomorphic_global terminate_ref); - f_constr = EConstr.of_constr f_constr; - concl_tac = tclIDTAC; - func=functional_ref; - info=(instantiate_lambda Evd.empty + f_constr = EConstr.of_constr f_constr; + concl_tac = tclIDTAC; + func=functional_ref; + info=(instantiate_lambda Evd.empty (EConstr.of_constr (def_of_const (constr_of_monomorphic_global functional_ref))) - (EConstr.of_constr f_constr::List.map mkVar x) - ); - is_main_branch = true; - is_final = true; - values_and_bounds = []; - eqs = []; - forbidden_ids = []; - acc_inv = lazy (assert false); - acc_id = Id.of_string "____"; - args_assoc = []; - f_id = Id.of_string "______"; - rec_arg_id = Id.of_string "______"; - is_mes = false; - ih = Id.of_string "______"; - } - ) + (EConstr.of_constr f_constr::List.map mkVar x) + ); + is_main_branch = true; + is_final = true; + values_and_bounds = []; + eqs = []; + forbidden_ids = []; + acc_inv = lazy (assert false); + acc_id = Id.of_string "____"; + args_assoc = []; + f_id = Id.of_string "______"; + rec_arg_id = Id.of_string "______"; + is_mes = false; + ih = Id.of_string "______"; + } + ) )) lemma in let _ = Flags.silently (fun () -> Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None) () in () @@ -1554,15 +1553,15 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type com_eqn sign uctx (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); false with e when CErrors.noncritical e -> - begin - if do_observe () - then Feedback.msg_debug (str "Cannot create equation Lemma " ++ CErrors.print e) - else CErrors.user_err ~hdr:"Cannot create equation Lemma" - (str "Cannot create equation lemma." ++ spc () ++ + begin + if do_observe () + then Feedback.msg_debug (str "Cannot create equation Lemma " ++ CErrors.print e) + else CErrors.user_err ~hdr:"Cannot create equation Lemma" + (str "Cannot create equation lemma." ++ spc () ++ str "This may be because the function is nested-recursive.") - ; - true - end + ; + true + end in if not stop then @@ -1576,9 +1575,9 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type (nb_prod evd (EConstr.of_constr res)) relation; Flags.if_verbose msgnl (h 1 (Ppconstr.pr_id function_name ++ - spc () ++ str"is defined" )++ fnl () ++ - h 1 (Ppconstr.pr_id equation_id ++ - spc () ++ str"is defined" ) + spc () ++ str"is defined" )++ fnl () ++ + h 1 (Ppconstr.pr_id equation_id ++ + spc () ++ str"is defined" ) ) in (* XXX STATE Why do we need this... why is the toplevel protection not enough *) |