summaryrefslogtreecommitdiff
path: root/contrib/funind
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/funind')
-rw-r--r--contrib/funind/functional_principles_proofs.ml1538
-rw-r--r--contrib/funind/functional_principles_proofs.mli20
-rw-r--r--contrib/funind/functional_principles_types.ml562
-rw-r--r--contrib/funind/functional_principles_types.mli31
-rw-r--r--contrib/funind/indfun.ml281
-rw-r--r--contrib/funind/indfun_main.ml4160
-rw-r--r--contrib/funind/invfun.ml13
-rw-r--r--contrib/funind/new_arg_principle.ml1770
-rw-r--r--contrib/funind/new_arg_principle.mli34
-rw-r--r--contrib/funind/rawterm_to_relation.ml247
-rw-r--r--contrib/funind/rawtermops.ml60
-rw-r--r--contrib/funind/rawtermops.mli5
-rw-r--r--contrib/funind/tacinv.ml420
13 files changed, 2688 insertions, 2053 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
new file mode 100644
index 00000000..f0e986fb
--- /dev/null
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -0,0 +1,1538 @@
+open Printer
+open Util
+open Term
+open Termops
+open Names
+open Declarations
+open Pp
+open Entries
+open Hiddentac
+open Evd
+open Tacmach
+open Proof_type
+open Tacticals
+open Tactics
+open Indfun_common
+open Libnames
+
+let msgnl = Pp.msgnl
+
+let do_observe () =
+ Tacinterp.get_debug () <> Tactic_debug.DebugOff
+
+
+let observe strm =
+ if do_observe ()
+ then Pp.msgnl strm
+ else ()
+
+let observennl strm =
+ if do_observe ()
+ then begin Pp.msg strm;Pp.pp_flush () end
+ else ()
+
+
+
+
+let do_observe_tac s tac g =
+ try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v
+ with e ->
+ let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in
+ msgnl (str "observation "++ s++str " raised exception " ++
+ Cerrors.explain_exn e ++ str " on goal " ++ goal );
+ raise e;;
+
+
+let observe_tac s tac g =
+ if do_observe ()
+ then do_observe_tac (str s) tac g
+ else tac g
+
+
+let tclTRYD tac =
+ if !Options.debug || do_observe ()
+ then (fun g -> try (* do_observe_tac "" *)tac g with _ -> tclIDTAC g)
+ else tac
+
+
+let list_chop ?(msg="") n l =
+ try
+ list_chop n l
+ with Failure (msg') ->
+ failwith (msg ^ msg')
+
+
+let make_refl_eq type_of_t t =
+ let refl_equal_term = Lazy.force refl_equal in
+ mkApp(refl_equal_term,[|type_of_t;t|])
+
+
+type pte_info =
+ {
+ proving_tac : (identifier list -> Tacmach.tactic);
+ is_valid : constr -> bool
+ }
+
+type ptes_info = pte_info Idmap.t
+
+type 'a dynamic_info =
+ {
+ nb_rec_hyps : int;
+ rec_hyps : identifier list ;
+ eq_hyps : identifier list;
+ info : 'a
+ }
+
+type body_info = constr dynamic_info
+
+
+let finish_proof dynamic_infos g =
+ observe_tac "finish"
+ ( h_assumption)
+ g
+
+
+let refine c =
+ Tacmach.refine_no_check c
+
+let thin l =
+ Tacmach.thin_no_check l
+
+
+let cut_replacing id t tac :tactic=
+ tclTHENS (cut t)
+ [ tclTHEN (thin_no_check [id]) (introduction_no_check id);
+ tac
+ ]
+
+let intro_erasing id = tclTHEN (thin [id]) (introduction id)
+
+
+
+let rec_hyp_id = id_of_string "rec_hyp"
+
+let is_trivial_eq t =
+ match kind_of_term t with
+ | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) ->
+ eq_constr t1 t2
+ | _ -> false
+
+
+let rec incompatible_constructor_terms t1 t2 =
+ let c1,arg1 = decompose_app t1
+ and c2,arg2 = decompose_app t2
+ in
+ (not (eq_constr t1 t2)) &&
+ isConstruct c1 && isConstruct c2 &&
+ (
+ not (eq_constr c1 c2) ||
+ List.exists2 incompatible_constructor_terms arg1 arg2
+ )
+
+let is_incompatible_eq t =
+ match kind_of_term t with
+ | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) ->
+ incompatible_constructor_terms t1 t2
+ | _ -> false
+
+let change_hyp_with_using msg hyp_id t tac : tactic =
+ fun g ->
+ let prov_id = pf_get_new_id hyp_id g in
+ tclTHENS
+ (observe_tac msg (forward (Some (tclCOMPLETE tac)) (Genarg.IntroIdentifier prov_id) t))
+ [tclTHENLIST
+ [
+ observe_tac "change_hyp_with_using thin" (thin [hyp_id]);
+ observe_tac "change_hyp_with_using rename " (h_rename prov_id hyp_id)
+ ]] g
+
+exception TOREMOVE
+
+
+let prove_trivial_eq h_id context (type_of_term,term) =
+ let nb_intros = List.length context in
+ tclTHENLIST
+ [
+ tclDO nb_intros 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(Lazy.force refl_equal,[|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 isAppConstruct t =
+ if isApp t
+ then isConstruct (fst (destApp t))
+ else false
+
+
+let nf_betaiotazeta = Reductionops.local_strong Reductionops.whd_betaiotazeta
+
+
+let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type =
+ let nochange msg =
+ begin
+(* observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t ); *)
+ failwith "NoChange";
+ end
+ in
+ if not (noccurn 1 end_of_type)
+ then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *)
+ if not (isApp t) then nochange "not an equality";
+ let f_eq,args = destApp t in
+ if not (eq_constr f_eq (Lazy.force eq)) then nochange "not an equality";
+ let t1 = args.(1)
+ and t2 = args.(2)
+ and t1_typ = args.(0)
+ in
+ if not (closed0 t1) then nochange "not a closed lhs";
+ let rec compute_substitution sub t1 t2 =
+ if isRel t2
+ then
+ let t2 = destRel t2 in
+ begin
+ try
+ let t1' = Intmap.find t2 sub in
+ if not (eq_constr t1 t1') then nochange "twice bound variable";
+ sub
+ with Not_found ->
+ assert (closed0 t1);
+ Intmap.add t2 t1 sub
+ end
+ else if isAppConstruct t1 && isAppConstruct t2
+ then
+ begin
+ let c1,args1 = destApp t1
+ and c2,args2 = destApp t2
+ in
+ if not (eq_constr c1 c2) then anomaly "deconstructing equation";
+ array_fold_left2 compute_substitution sub args1 args2
+ end
+ else
+ if (eq_constr t1 t2) then sub else nochange "cannot solve"
+ in
+ let sub = compute_substitution Intmap.empty t1 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
+ *)
+ let sub' = Intmap.fold (fun i t acc -> (i,t)::acc) sub [] in
+ let sub'' = List.sort (fun (x,_) (y,_) -> Pervasives.compare x y) sub' in
+ List.fold_left (fun end_of_type (i,t) -> lift 1 (substnl [t] (i-1) end_of_type))
+ end_of_type_with_pop
+ sub''
+ in
+ (* let new_end_of_type = *)
+ (* Intmap.fold *)
+ (* (fun i t end_of_type -> lift 1 (substnl [t] (i-1) end_of_type)) *)
+ (* sub *)
+ (* end_of_type_with_pop *)
+ (* in *)
+ let old_context_length = List.length context + 1 in
+ let witness_fun =
+ mkLetIn(Anonymous,make_refl_eq t1_typ t1,t,
+ 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) ((x',b',t') as decl) ->
+ try
+ let witness = Intmap.find i sub in
+ if b' <> None then anomaly "can not redefine a rel!";
+ (pop end_of_type,ctxt_size,mkLetIn(x',witness,t',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
+ in
+ let new_type_of_hyp = Reductionops.nf_betaiota new_type_of_hyp in
+ let new_ctxt,new_end_of_type =
+ Sign.decompose_prod_n_assum ctxt_size new_type_of_hyp
+ in
+ let prove_new_hyp : tactic =
+ tclTHEN
+ (tclDO ctxt_size 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
+ 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 () *)
+(* ); *)
+ new_ctxt,new_end_of_type,simpl_eq_tac
+
+
+let is_property ptes_info t_x full_type_of_hyp =
+ if isApp t_x
+ then
+ let pte,args = destApp t_x in
+ if isVar pte && array_for_all closed0 args
+ then
+ try
+ let info = Idmap.find (destVar pte) ptes_info in
+ info.is_valid full_type_of_hyp
+ with Not_found -> false
+ else false
+ else false
+
+let isLetIn t =
+ match kind_of_term t with
+ | LetIn _ -> true
+ | _ -> false
+
+
+let h_reduce_with_zeta =
+ h_reduce
+ (Rawterm.Cbv
+ {Rawterm.all_flags
+ with Rawterm.rDelta = false;
+ })
+
+
+
+let rewrite_until_var arg_num eq_ids : tactic =
+ let test_var g =
+ let _,args = destApp (pf_concl g) in
+ not (isConstruct args.(arg_num))
+ in
+ let rec do_rewrite eq_ids g =
+ if test_var g
+ then tclIDTAC g
+ else
+ match eq_ids with
+ | [] -> anomaly "Cannot find a way to prove recursive property";
+ | eq_id::eq_ids ->
+ tclTHEN
+ (tclTRY (Equality.rewriteRL (mkVar eq_id)))
+ (do_rewrite eq_ids)
+ g
+ in
+ do_rewrite eq_ids
+
+
+let rec_pte_id = id_of_string "Hrec"
+let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
+ let coq_False = Coqlib.build_coq_False () in
+ let coq_True = Coqlib.build_coq_True () in
+ let coq_I = Coqlib.build_coq_I () in
+ let rec scan_type context type_of_hyp : tactic =
+ if isLetIn type_of_hyp then
+ let real_type_of_hyp = it_mkProd_or_LetIn ~init:type_of_hyp context in
+ let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in
+ (* length of context didn't change ? *)
+ let new_context,new_typ_of_hyp =
+ Sign.decompose_prod_n_assum (List.length context) reduced_type_of_hyp
+ in
+ tclTHENLIST
+ [
+ h_reduce_with_zeta
+ (Tacticals.onHyp hyp_id)
+ ;
+ scan_type new_context new_typ_of_hyp
+
+ ]
+ else if isProd type_of_hyp
+ then
+ begin
+ let (x,t_x,t') = destProd type_of_hyp in
+ let actual_real_type_of_hyp = it_mkProd_or_LetIn ~init:t' context in
+ if is_property ptes_infos t_x actual_real_type_of_hyp then
+ begin
+ let pte,pte_args = (destApp t_x) in
+ let (* fix_info *) prove_rec_hyp = (Idmap.find (destVar pte) ptes_infos).proving_tac in
+ let popped_t' = pop t' in
+ let real_type_of_hyp = it_mkProd_or_LetIn ~init:popped_t' context in
+ let prove_new_type_of_hyp =
+ let context_length = List.length context in
+ tclTHENLIST
+ [
+ tclDO context_length 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
+ (assert_as true (Genarg.IntroIdentifier 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 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 t_x then raise TOREMOVE (* t_x := C1 ... = C2 ... *)
+ else if eq_constr 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 ~init:popped_t' context
+ in
+ let prove_trivial =
+ let nb_intro = List.length context in
+ tclTHENLIST [
+ tclDO nb_intro 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 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 ~init:popped_t' context
+ in
+ let _,args = destApp t_x 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 (args.(0),args.(1))));
+ 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 Failure "NoChange" ->
+ (* Last thing todo : push the rel in the context and continue *)
+ scan_type ((x,None,t_x)::context) t'
+ end
+ end
+ else
+ tclIDTAC
+ in
+ try
+ scan_type [] (Typing.type_of env sigma (mkVar hyp_id)), [hyp_id]
+ with TOREMOVE ->
+ thin [hyp_id],[]
+
+
+let clean_goal_with_heq ptes_infos continue_tac dyn_infos =
+ fun g ->
+ let env = pf_env g
+ and sigma = project g
+ 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
+ )
+ (tclIDTAC,[])
+ dyn_infos.rec_hyps
+ in
+ let new_infos =
+ { dyn_infos with
+ rec_hyps = new_hyps;
+ nb_rec_hyps = List.length new_hyps
+ }
+ in
+ tclTHENLIST
+ [
+ tac ;
+ (continue_tac new_infos)
+ ]
+ g
+
+let heq_id = id_of_string "Heq"
+
+let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
+ fun g ->
+ let heq_id = pf_get_new_id heq_id g in
+ let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in
+ tclTHENLIST
+ [
+ (* We first introduce the variables *)
+ tclDO nb_first_intro (intro_avoiding dyn_infos.rec_hyps);
+ (* Then the equation itself *)
+ introduction_no_check heq_id;
+ (* Then the new hypothesis *)
+ tclMAP introduction_no_check dyn_infos.rec_hyps;
+ observe_tac "after_introduction" (fun g' ->
+ (* We get infos on the equations introduced*)
+ let new_term_value_eq = pf_type_of g' (mkVar heq_id) in
+ (* compute the new value of the body *)
+ let new_term_value =
+ match kind_of_term 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_lconstr_env (pf_env g') new_term_value_eq
+ );
+ anomaly "cannot compute new term value"
+ in
+ let fun_body =
+ mkLambda(Anonymous,
+ pf_type_of g' term,
+ replace_term 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
+
+
+let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id =
+ let args = Array.of_list (List.map mkVar args_id) in
+ let instanciate_one_hyp hid =
+ tclORELSE
+ ( (* we instanciate the hyp if possible *)
+ fun g ->
+ let prov_hid = pf_get_new_id hid g in
+ tclTHENLIST[
+ forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
+ thin [hid];
+ h_rename 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.
+
+ We are not supposed to use it while proving this
+ principle so that we can trash it
+
+ *)
+ (fun g ->
+(* observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid); *)
+ thin [hid] g
+ )
+ )
+ in
+ if args_id = []
+ then
+ tclTHENLIST [
+ tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps;
+ do_prove hyps
+ ]
+ else
+ tclTHENLIST
+ [
+ tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps;
+ tclMAP instanciate_one_hyp hyps;
+ (fun g ->
+ let all_g_hyps_id =
+ List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty
+ in
+ let remaining_hyps =
+ List.filter (fun id -> Idset.mem id all_g_hyps_id) hyps
+ in
+ do_prove remaining_hyps g
+ )
+ ]
+
+let build_proof
+ (interactive_proof:bool)
+ (fnames:constant list)
+ ptes_infos
+ dyn_infos
+ : tactic =
+ let rec build_proof_aux do_finalize dyn_infos : tactic =
+ fun g ->
+
+(* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
+ match kind_of_term dyn_infos.info with
+ | Case(_,_,t,_) ->
+ let g_nb_prod = nb_prod (pf_concl g) in
+ let type_of_term = pf_type_of g t in
+ let term_eq =
+ make_refl_eq type_of_term t
+ in
+ tclTHENSEQ
+ [
+ h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
+ thin dyn_infos.rec_hyps;
+ pattern_option [[-1],t] None;
+ h_simplest_case t;
+ (fun g' ->
+ let g'_nb_prod = nb_prod (pf_concl g') in
+ let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
+ observe_tac "treat_new_case"
+ (treat_new_case
+ ptes_infos
+ nb_instanciate_partial
+ (build_proof do_finalize)
+ t
+ dyn_infos)
+ g'
+ )
+
+ ] g
+ | Lambda(n,t,b) ->
+ begin
+ match kind_of_term( pf_concl g) with
+ | Prod _ ->
+ tclTHEN
+ intro
+ (fun g' ->
+ let (id,_,_) = pf_last_hyp g' 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" (instanciate_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 _ ->
+ do_finalize dyn_infos g
+ | App(_,_) ->
+ let f,args = decompose_app dyn_infos.info in
+ begin
+ match kind_of_term f with
+ | App _ -> assert false (* we have collected all the app in decompose_app *)
+ | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _ ->
+ let new_infos =
+ { dyn_infos with
+ info = (f,args)
+ }
+ in
+ build_proof_args do_finalize new_infos g
+ | Const c when not (List.mem 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 do_finalize new_infos g
+ | Const _ ->
+ do_finalize dyn_infos g
+ | Lambda _ ->
+ let new_term = Reductionops.nf_beta dyn_infos.info in
+ build_proof do_finalize {dyn_infos with info = new_term}
+ g
+ | LetIn _ ->
+ let new_infos =
+ { dyn_infos with info = nf_betaiotazeta dyn_infos.info }
+ in
+
+ tclTHENLIST
+ [tclMAP
+ (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id))
+ dyn_infos.rec_hyps;
+ h_reduce_with_zeta Tacticals.onConcl;
+ build_proof do_finalize new_infos
+ ]
+ 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
+ build_proof_args do_finalize new_infos
+ in
+ build_proof new_finalize {dyn_infos with info = f } g
+ end
+ | Fix _ | CoFix _ ->
+ error ( "Anonymous local (co)fixpoints are not handled yet")
+
+ | Prod _ -> error "Prod"
+ | LetIn _ ->
+ let new_infos =
+ { dyn_infos with
+ info = nf_betaiotazeta dyn_infos.info
+ }
+ in
+
+ tclTHENLIST
+ [tclMAP
+ (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id))
+ dyn_infos.rec_hyps;
+ h_reduce_with_zeta Tacticals.onConcl;
+ build_proof do_finalize new_infos
+ ] g
+ | Rel _ -> anomaly "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); *)
+ (build_proof_aux do_finalize dyn_infos) g
+ and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic =
+ fun g ->
+(* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *)
+(* then msgnl (str "build_proof_args with " ++ *)
+(* pr_lconstr_env (pf_env g) f_args' *)
+(* ); *)
+ 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 *)
+ (build_proof_args
+ do_finalize
+ {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args}
+ )
+ in
+ build_proof do_finalize
+ {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)
+ in
+ observe_tac "build_proof"
+ (build_proof do_finish_proof dyn_infos)
+
+
+
+
+
+
+
+
+
+
+
+
+(* Proof of principles from structural functions *)
+let is_pte_type t =
+ isSort (snd (decompose_prod t))
+
+let is_pte (_,_,t) = is_pte_type t
+
+
+
+
+type static_fix_info =
+ {
+ idx : int;
+ name : identifier;
+ types : types;
+ offset : int;
+ nb_realargs : int;
+ body_with_param : constr
+ }
+
+
+
+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 (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
+ ;
+ is_valid = fun _ -> true
+ }
+
+
+exception Not_Rec
+
+let generalize_non_dep hyp g =
+ let hyps = [hyp] in
+ let env = Global.env () in
+ let hyp_typ = pf_type_of g (mkVar hyp) in
+ let to_revert,_ =
+ Environ. fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
+ if List.mem hyp hyps
+ or List.exists (occur_var_in_decl env hyp) keep
+ or occur_var env hyp hyp_typ
+ or Termops.is_section_variable hyp (* should be dangerous *)
+ then (clear,decl::keep)
+ else (hyp::clear,keep))
+ ~init:([],[]) (pf_env g)
+ in
+(* observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
+ tclTHEN
+ (observe_tac "h_generalize" (h_generalize (List.map mkVar to_revert)))
+ (observe_tac "thin" (thin to_revert))
+ g
+
+let id_of_decl (na,_,_) = (Nameops.out_name na)
+let var_of_decl decl = mkVar (id_of_decl decl)
+let revert idl =
+ tclTHEN
+ (generalize (List.map mkVar idl))
+ (thin idl)
+
+
+let do_replace params rec_arg_num rev_args_id fun_to_replace body =
+ fun g ->
+ let nb_intro_to_do = nb_prod (pf_concl g) in
+ tclTHEN
+ (tclDO nb_intro_to_do intro)
+ (
+ fun g' ->
+ let just_introduced = nLastHyps nb_intro_to_do g' in
+ let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in
+ let old_rev_args_id = rev_args_id in
+ let rev_args_id = just_introduced_id@rev_args_id in
+ let to_replace =
+ Reductionops.nf_betaiota (substl (List.map mkVar rev_args_id) fun_to_replace )
+ and by =
+ Reductionops.nf_betaiota (applist(body,List.rev_map mkVar rev_args_id))
+ in
+(* observe (str "to_replace := " ++ pr_lconstr_env (pf_env g') to_replace); *)
+(* observe (str "by := " ++ pr_lconstr_env (pf_env g') by); *)
+ let prove_replacement =
+ let rec_id = List.nth (List.rev old_rev_args_id) (rec_arg_num) in
+ observe_tac "prove_replacement"
+ (tclTHENSEQ
+ [
+ revert just_introduced_id;
+ keep ((List.map id_of_decl params)@ old_rev_args_id);
+ generalize_non_dep rec_id;
+ observe_tac "h_case" (h_case(mkVar rec_id,Rawterm.NoBindings));
+ intros_reflexivity
+ ]
+ )
+ in
+ tclTHENS
+ (observe_tac "replacement" (Equality.replace to_replace by))
+ [ revert just_introduced_id;
+ tclSOLVE [prove_replacement]]
+ g'
+ )
+ g
+
+
+
+let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : tactic =
+ fun g ->
+ let princ_type = pf_concl g in
+ let princ_info = compute_elim_sig princ_type in
+ 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 (string_of_id id)
+ | Anonymous -> fresh_id !avoid "H"
+ in
+ avoid := new_id :: !avoid;
+ (Name new_id)
+ )
+ in
+ let fresh_decl =
+ (fun (na,b,t) ->
+ (fresh_id na,b,t)
+ )
+ 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
+ }
+ in
+ let get_body const =
+ match (Global.lookup_constant const ).const_body with
+ | Some b ->
+ let body = force b in
+ Tacred.cbv_norm_flags
+ (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+ (Global.env ())
+ (Evd.empty)
+ body
+ | None -> error ( "Cannot define a principle over an axiom ")
+ in
+ let fbody = get_body fnames.(fun_num) in
+ let f_ctxt,f_body = decompose_lam fbody in
+ let f_ctxt_length = List.length f_ctxt in
+ let diff_params = princ_info.nparams - f_ctxt_length in
+ 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 *)
+ substl (* function instanciated with real params *)
+ (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 *)
+ substl (* function instanciated with real params *)
+ (List.map var_of_decl princ_info.params)
+ f_body
+ )
+ in
+(* observe (str "full_params := " ++ *)
+(* prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) *)
+(* full_params *)
+(* ); *)
+(* observe (str "princ_params := " ++ *)
+(* prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) *)
+(* princ_params *)
+(* ); *)
+(* observe (str "fbody_with_full_params := " ++ *)
+(* pr_lconstr 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
+ let fix_offset = List.length princ_params in
+ let ptes_to_fix,infos =
+ match kind_of_term fbody_with_full_params with
+ | Fix((idxs,i),(names,typess,bodies)) ->
+ let bodies_with_all_params =
+ Array.map
+ (fun body ->
+ Reductionops.nf_betaiota
+ (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 types (List.rev_map var_of_decl princ_params) in
+ { idx = idxs.(i) - fix_offset;
+ name = Nameops.out_name (fresh_id names.(i));
+ types = types;
+ offset = fix_offset;
+ nb_realargs =
+ List.length
+ (fst (decompose_lam bodies.(i))) - fix_offset;
+ body_with_param = bodies_with_all_params.(i)
+ }
+ )
+ typess
+ in
+ let pte_to_fix,rev_info =
+ list_fold_left_i
+ (fun i (acc_map,acc_info) (pte,_,_) ->
+ let infos = info_array.(i) in
+ let type_args,_ = decompose_prod 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.out_name pte),pte_args) in
+ let body_with_param =
+ let body = get_body fnames.(i) in
+ let body_with_full_params =
+ Reductionops.nf_betaiota (
+ applist(body,List.rev_map var_of_decl full_params))
+ in
+ match kind_of_term body_with_full_params with
+ | Fix((_,num),(_,_,bs)) ->
+ Reductionops.nf_betaiota
+ (
+ (applist
+ (substl
+ (List.rev
+ (Array.to_list all_funs_with_full_params))
+ bs.(num),
+ List.rev_map var_of_decl princ_params))
+ )
+ | _ -> error "Not a mutual block"
+ in
+ let info =
+ {infos with
+ types = compose_prod type_args app_pte;
+ body_with_param = body_with_param
+ }
+ in
+(* observe (str "binding " ++ Ppconstr.pr_id (Nameops.out_name pte) ++ *)
+(* str " to " ++ Ppconstr.pr_id info.name); *)
+ (Idmap.add (Nameops.out_name pte) info acc_map,info::acc_info)
+ )
+ 0
+ (Idmap.empty,[])
+ (List.rev princ_info.predicates)
+ in
+ pte_to_fix,List.rev rev_info
+ | _ -> Idmap.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 other_fix_infos = []
+ then
+ observe_tac ("h_fix") (h_fix (Some this_fix_info.name) (this_fix_info.idx +1))
+ else
+ h_mutual_fix this_fix_info.name (this_fix_info.idx + 1)
+ other_fix_infos
+ | _ -> anomaly "Not a valid information"
+ in
+ let first_tac : tactic = (* every operations until fix creations *)
+ tclTHENSEQ
+ [ observe_tac "introducing params" (intros_using (List.rev_map id_of_decl princ_info.params));
+ observe_tac "introducing predictes" (intros_using (List.rev_map id_of_decl princ_info.predicates));
+ observe_tac "introducing branches" (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 = (Sign.decompose_prod_assum (pf_concl gl)) in
+ let pte,pte_args = (decompose_app pte_app) in
+ try
+ let pte = try destVar pte with _ -> anomaly "Property is not a variable" in
+ let fix_info = Idmap.find pte ptes_to_fix in
+ let nb_args = fix_info.nb_realargs in
+ tclTHENSEQ
+ [
+ observe_tac ("introducing args") (tclDO nb_args intro);
+ (fun g -> (* replacement of the function by its body *)
+ let args = nLastHyps 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 args_id = List.map (fun (id,_,_) -> id) args in
+ let dyn_infos =
+ {
+ nb_rec_hyps = -100;
+ rec_hyps = [];
+ info =
+ Reductionops.nf_betaiota
+ (applist(fix_body,List.rev_map mkVar args_id));
+ eq_hyps = []
+ }
+ in
+ tclTHENSEQ
+ [
+ observe_tac "do_replace"
+ (do_replace princ_info.params fix_info.idx args_id
+ (List.hd (List.rev pte_args)) fix_body);
+ let do_prove =
+ build_proof
+ interactive_proof
+ (Array.to_list fnames)
+ (Idmap.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
+ (Idmap.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); *)
+ observe_tac "instancing" (instanciate_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
+ tclTHENSEQ
+ [
+ tclDO nb_args intro;
+ (fun g -> (* replacement of the function by its body *)
+ let args = nLastHyps nb_args g in
+ let args_id = List.map (fun (id,_,_) -> id) args in
+ let dyn_infos =
+ {
+ nb_rec_hyps = -100;
+ rec_hyps = [];
+ info =
+ Reductionops.nf_betaiota
+ (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 (fst (decompose_app (List.hd (List.rev pte_args)))) in
+ tclTHENSEQ
+ [unfold_in_concl [([],Names.EvalConstRef fname)];
+ let do_prove =
+ build_proof
+ interactive_proof
+ (Array.to_list fnames)
+ (Idmap.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
+ (Idmap.map prove_rec_hyp ptes_to_fix)
+ do_prove
+ dyn_infos
+ in
+ instanciate_hyps_with_args prove_tac
+ (List.rev_map id_of_decl princ_info.branches)
+ (List.rev args_id)
+ ]
+ g
+ )
+ ]
+ gl
+ in
+ tclTHEN
+ first_tac
+ intros_after_fixes
+ g
+
+
+
+
+
+
+(* Proof of principles of general functions *)
+let h_id = Recdef.h_id
+and hrec_id = Recdef.hrec_id
+and acc_inv_id = Recdef.acc_inv_id
+and ltof_ref = Recdef.ltof_ref
+and acc_rel = Recdef.acc_rel
+and well_founded = Recdef.well_founded
+and delayed_force = Recdef.delayed_force
+and h_intros = Recdef.h_intros
+and list_rewrite = Recdef.list_rewrite
+and evaluable_of_global_reference = Recdef.evaluable_of_global_reference
+
+let prove_with_tcc tcc_lemma_constr eqs : tactic =
+ match !tcc_lemma_constr with
+ | None -> anomaly "No tcc proof !!"
+ | Some lemma ->
+ fun gls ->
+ let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in
+ tclTHENSEQ
+ [
+ generalize [lemma];
+ h_intro hid;
+ Elim.h_decompose_and (mkVar hid);
+ tclTRY(list_rewrite true eqs);
+ Eauto.gen_eauto false (false,5) [] (Some [])
+ ]
+ gls
+
+
+let backtrack_eqs_until_hrec hrec eqs : tactic =
+ fun gls ->
+ let rewrite =
+ tclFIRST (List.map Equality.rewriteRL eqs )
+ in
+ let _,hrec_concl = decompose_prod (pf_type_of gls (mkVar hrec)) in
+ let f_app = array_last (snd (destApp hrec_concl)) in
+ let f = (fst (destApp f_app)) in
+ let rec backtrack : tactic =
+ fun g ->
+ let f_app = array_last (snd (destApp (pf_concl g))) in
+ match kind_of_term f_app with
+ | App(f',_) when eq_constr f' f -> tclIDTAC g
+ | _ -> tclTHEN rewrite backtrack g
+ in
+ backtrack gls
+
+
+
+
+
+let new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_constr eqs : tactic =
+ match !tcc_lemma_constr with
+ | None -> tclIDTAC_MESSAGE (str "No tcc proof !!")
+ | Some lemma ->
+ fun gls ->
+ let hid = next_global_ident_away true Recdef.h_id (pf_ids_of_hyps gls) in
+ (tclTHENSEQ
+ [
+ generalize [lemma];
+ h_intro hid;
+ Elim.h_decompose_and (mkVar hid);
+ backtrack_eqs_until_hrec hrec eqs;
+ tclCOMPLETE (tclTHENS (* We must have exactly ONE subgoal !*)
+ (apply (mkVar hrec))
+ [ tclTHENSEQ
+ [
+ thin [hrec];
+ apply (Lazy.force acc_inv);
+ (fun g ->
+ if is_mes
+ then
+ unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] g
+ else tclIDTAC g
+ );
+ tclTRY(Recdef.list_rewrite true eqs);
+ observe_tac "finishing" (tclCOMPLETE (Eauto.gen_eauto false (false,5) [] (Some [])))
+ ]
+ ]
+ )
+ ])
+ gls
+
+
+let is_valid_hypothesis predicates_name =
+ let predicates_name = List.fold_right Idset.add predicates_name Idset.empty in
+ let is_pte typ =
+ if isApp typ
+ then
+ let pte,_ = destApp typ in
+ if isVar pte
+ then Idset.mem (destVar pte) predicates_name
+ else false
+ else false
+ in
+ let rec is_valid_hypothesis typ =
+ is_pte typ ||
+ match kind_of_term typ with
+ | Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ'
+ | _ -> false
+ in
+ is_valid_hypothesis
+
+let fresh_id avoid na =
+ let id =
+ match na with
+ | Name id -> id
+ | Anonymous -> h_id
+ in
+ next_global_ident_away true id avoid
+
+
+let prove_principle_for_gen
+ (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes
+ rec_arg_num rec_arg_type relation =
+ fun g ->
+ let type_of_goal = pf_concl g in
+ let goal_ids = pf_ids_of_hyps g in
+ let goal_elim_infos = compute_elim_sig type_of_goal in
+ let params_names,ids = List.fold_left
+ (fun (params_names,avoid) (na,_,_) ->
+ let new_id = fresh_id avoid na in
+ (new_id::params_names,new_id::avoid)
+ )
+ ([],goal_ids)
+ goal_elim_infos.params
+ in
+ let predicates_names,ids =
+ List.fold_left
+ (fun (predicates_names,avoid) (na,_,_) ->
+ let new_id = fresh_id avoid na in
+ (new_id::predicates_names,new_id::avoid)
+ )
+ ([],ids)
+ goal_elim_infos.predicates
+ in
+ let branches_names,ids =
+ List.fold_left
+ (fun (branches_names,avoid) (na,_,_) ->
+ let new_id = fresh_id avoid na in
+ (new_id::branches_names,new_id::avoid)
+ )
+ ([],ids)
+ goal_elim_infos.branches
+ in
+ let to_intro = params_names@predicates_names@branches_names in
+ let nparams = List.length params_names in
+ let rec_arg_num = rec_arg_num - nparams in
+ let tac_intro_static = h_intros to_intro in
+ let args_info = ref None in
+ let arg_tac g = (* introducing args *)
+ let ids = pf_ids_of_hyps g in
+ let func_body = def_of_const (mkConst functional_ref) in
+ (* let _ = Pp.msgnl (Printer.pr_lconstr func_body) in *)
+ let (f_name, _, body1) = destLambda func_body in
+ let f_id =
+ match f_name with
+ | Name f_id -> next_global_ident_away true f_id ids
+ | Anonymous -> anomaly "anonymous function"
+ in
+ let n_names_types,_ = decompose_lam body1 in
+ let n_ids,ids =
+ List.fold_left
+ (fun (n_ids,ids) (n_name,_) ->
+ match n_name with
+ | Name id ->
+ let n_id = next_global_ident_away true id ids in
+ n_id::n_ids,n_id::ids
+ | _ -> anomaly "anonymous argument"
+ )
+ ([],(f_id::ids))
+ n_names_types
+ in
+ let rec_arg_id = List.nth n_ids (rec_arg_num - 1 ) in
+ let args_ids = snd (list_chop nparams n_ids) in
+ args_info := Some (ids,args_ids,rec_arg_id);
+ h_intros args_ids g
+ in
+ let wf_tac =
+ if is_mes
+ then
+ Recdef.tclUSER_if_not_mes
+ else fun _ -> prove_with_tcc tcc_lemma_ref []
+ in
+ let start_tac g =
+ let ids,args_ids,rec_arg_id = out_some !args_info in
+ let nargs = List.length args_ids in
+ let pre_rec_arg =
+ List.rev_map
+ mkVar
+ (fst (list_chop (rec_arg_num - 1) args_ids))
+ in
+ let args_before_rec = pre_rec_arg@(List.map mkVar params_names) in
+ let relation = substl args_before_rec relation in
+ let input_type = substl args_before_rec rec_arg_type in
+ let wf_thm = next_global_ident_away true (id_of_string ("wf_R")) ids in
+ let wf_rec_arg =
+ next_global_ident_away true
+ (id_of_string ("Acc_"^(string_of_id rec_arg_id)))
+ (wf_thm::ids)
+ in
+ let hrec = next_global_ident_away true hrec_id (wf_rec_arg::wf_thm::ids) in
+ let acc_inv =
+ lazy (
+ mkApp (
+ delayed_force acc_inv_id,
+ [|input_type;relation;mkVar rec_arg_id|]
+ )
+ )
+ in
+ (tclTHENS
+ (observe_tac
+ "first assert"
+ (assert_tac
+ true (* the assert thm is in first subgoal *)
+ (Name wf_rec_arg)
+ (mkApp (delayed_force acc_rel,
+ [|input_type;relation;mkVar rec_arg_id|])
+ )
+ )
+ )
+ [
+ (* accesibility proof *)
+ tclTHENS
+ (observe_tac
+ "second assert"
+ (assert_tac
+ true
+ (Name wf_thm)
+ (mkApp (delayed_force well_founded,[|input_type;relation|]))
+ )
+ )
+ [
+ (* interactive proof of the well_foundness of the relation *)
+ wf_tac is_mes;
+ (* well_foundness -> Acc for any element *)
+ observe_tac
+ "apply wf_thm"
+ (h_apply ((mkApp(mkVar wf_thm,
+ [|mkVar rec_arg_id |])),Rawterm.NoBindings)
+ )
+ ]
+ ;
+ (* rest of the proof *)
+ tclTHENSEQ
+ [
+ observe_tac "generalize" (fun g ->
+ let to_thin =
+ fst (list_chop ( nargs + 1) (pf_ids_of_hyps g))
+ in
+ let to_thin_c = List.rev_map mkVar to_thin in
+ tclTHEN (generalize to_thin_c) (observe_tac "thin" (h_clear false to_thin)) g
+ );
+ observe_tac "h_fix" (h_fix (Some hrec) (nargs+1));
+ h_intros args_ids;
+ h_intro wf_rec_arg;
+ Equality.rewriteLR (mkConst eq_ref);
+ (fun g' ->
+ let body =
+ let _,args = destApp (pf_concl g') 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(Lazy.force acc_inv, [|mkVar wf_rec_arg|]) ) in
+ let pte_info =
+ { proving_tac =
+ (fun eqs ->
+ observe_tac "prove_with_tcc"
+ (new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_ref (List.map mkVar eqs))
+ );
+ is_valid = is_valid_hypothesis predicates_names
+ }
+ in
+ let ptes_info : pte_info Idmap.t =
+ List.fold_left
+ (fun map pte_id ->
+ Idmap.add pte_id
+ pte_info
+ map
+ )
+ Idmap.empty
+ predicates_names
+ in
+ let make_proof rec_hyps =
+ build_proof
+ false
+ [f_ref]
+ ptes_info
+ (body_info rec_hyps)
+ in
+ instanciate_hyps_with_args
+ make_proof
+ branches_names
+ args_ids
+ g'
+
+ )
+ ]
+ ]
+ g
+ )
+ in
+ tclTHENSEQ
+ [tac_intro_static;
+ arg_tac;
+ start_tac
+ ] g
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/contrib/funind/functional_principles_proofs.mli b/contrib/funind/functional_principles_proofs.mli
new file mode 100644
index 00000000..35da5d50
--- /dev/null
+++ b/contrib/funind/functional_principles_proofs.mli
@@ -0,0 +1,20 @@
+open Names
+open Term
+
+val prove_princ_for_struct :
+ bool ->
+ int -> constant array -> constr array -> int -> Tacmach.tactic
+
+
+val prove_principle_for_gen :
+ constant*constant*constant -> (* name of the function, the fonctionnal and the fixpoint equation *)
+ constr option ref -> (* a pointer to the obligation proofs lemma *)
+ bool -> (* is that function uses measure *)
+ int -> (* the number of recursive argument *)
+ types -> (* the type of the recursive argument *)
+ constr -> (* the wf relation used to prove the function *)
+ Tacmach.tactic
+
+
+val is_pte : rel_declaration -> bool
+val do_observe : unit -> bool
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
new file mode 100644
index 00000000..8ef13264
--- /dev/null
+++ b/contrib/funind/functional_principles_types.ml
@@ -0,0 +1,562 @@
+open Printer
+open Util
+open Term
+open Termops
+open Names
+open Declarations
+open Pp
+open Entries
+open Hiddentac
+open Evd
+open Tacmach
+open Proof_type
+open Tacticals
+open Tactics
+open Indfun_common
+open Functional_principles_proofs
+
+exception Toberemoved_with_rel of int*constr
+exception Toberemoved
+
+
+
+
+
+(*
+ Transform an inductive induction principle into
+ a functional one
+*)
+let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
+ let princ_type_info = compute_elim_sig princ_type in
+ let env = Global.env () in
+ let change_predicate_sort i (x,_,t) =
+ let new_sort = sorts.(i) in
+ let args,_ = decompose_prod t in
+ let real_args =
+ if princ_type_info.indarg_in_concl
+ then List.tl args
+ else args
+ in
+ x,None,compose_prod real_args (mkSort new_sort)
+ in
+ let new_predicates =
+ list_map_i
+ change_predicate_sort
+ 0
+ princ_type_info.predicates
+ in
+ let env_with_params_and_predicates =
+ Environ.push_rel_context
+ new_predicates
+ (Environ.push_rel_context
+ princ_type_info.params
+ env
+ )
+ in
+ let rel_as_kn =
+ fst (match princ_type_info.indref with
+ | Some (Libnames.IndRef ind) -> ind
+ | _ -> failwith "Not a valid predicate"
+ )
+ in
+ let pre_princ =
+ it_mkProd_or_LetIn
+ ~init:
+ (it_mkProd_or_LetIn
+ ~init:(option_fold_right
+ mkProd_or_LetIn
+ princ_type_info.indarg
+ princ_type_info.concl
+ )
+ princ_type_info.args
+ )
+ princ_type_info.branches
+ in
+ let is_dom c =
+ match kind_of_term c with
+ | Ind((u,_)) -> u = rel_as_kn
+ | Construct((u,_),_) -> u = rel_as_kn
+ | _ -> false
+ in
+ let get_fun_num c =
+ match kind_of_term c with
+ | Ind(_,num) -> num
+ | Construct((_,num),_) -> num
+ | _ -> assert false
+ in
+ let dummy_var = mkVar (id_of_string "________") in
+ let mk_replacement c i args =
+ let res = mkApp(rel_to_fun.(i),Array.map pop (array_get_start args)) in
+(* observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); *)
+ res
+ in
+ let rec has_dummy_var t =
+ fold_constr
+ (fun b t -> b || (eq_constr t dummy_var) || (has_dummy_var t))
+ false
+ t
+ in
+ let rec compute_new_princ_type remove env pre_princ : types*(constr list) =
+ let (new_princ_type,_) as res =
+ match kind_of_term pre_princ with
+ | Rel n ->
+ begin
+ try match Environ.lookup_rel n env with
+ | _,_,t when is_dom t -> raise Toberemoved
+ | _ -> 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 is_pte =
+ match kind_of_term f with
+ | Rel n ->
+ is_pte (Environ.lookup_rel n env)
+ | _ -> false
+ in
+ let args =
+ if is_pte && 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
+ applist(new_f, new_args),
+ list_union_eq eq_constr 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,[]
+ in
+(* observennl ( *)
+(* match kind_of_term pre_princ with *)
+(* | Prod _ -> *)
+(* str "compute_new_princ_type for "++ *)
+(* pr_lconstr_env env pre_princ ++ *)
+(* str" is "++ *)
+(* pr_lconstr_env env new_princ_type ++ fnl () *)
+(* | _ -> str "" *)
+(* ); *)
+ 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_x : name = get_name (ids_of_context env) x in
+ let new_env = Environ.push_rel (x,None,t) env in
+ let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
+ if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
+ then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+ else
+ (
+ bind_fun(new_x,new_t,new_b),
+ list_union_eq
+ eq_constr
+ binders_to_remove_from_t
+ (List.map pop binders_to_remove_from_b)
+ )
+
+ with
+ | Toberemoved ->
+(* msgnl (str "Decl of "++Ppconstr.pr_name 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) ->
+(* msgnl (str "Decl of "++Ppconstr.pr_name 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 eq_constr (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_x : name = get_name (ids_of_context env) x in
+ let new_env = Environ.push_rel (x,Some v,t) env in
+ let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
+ if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
+ then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+ else
+ (
+ mkLetIn(new_x,new_v,new_t,new_b),
+ list_union_eq
+ eq_constr
+ (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v)
+ (List.map pop binders_to_remove_from_b)
+ )
+
+ with
+ | Toberemoved ->
+(* msgnl (str "Decl of "++Ppconstr.pr_name 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) ->
+(* msgnl (str "Decl of "++Ppconstr.pr_name 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 eq_constr (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
+ in
+ new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc
+ in
+(* observe (str "Computing new principe from " ++ pr_lconstr_env env_with_params_and_predicates pre_princ); *)
+ let pre_res,_ =
+ compute_new_princ_type princ_type_info.indarg_in_concl env_with_params_and_predicates pre_princ in
+ it_mkProd_or_LetIn
+ ~init:(it_mkProd_or_LetIn ~init:pre_res new_predicates)
+ princ_type_info.params
+
+
+
+let change_property_sort toSort princ princName =
+ let princ_info = compute_elim_sig princ in
+ let change_sort_in_predicate (x,v,t) =
+ (x,None,
+ let args,_ = decompose_prod t in
+ compose_prod args (mkSort toSort)
+ )
+ in
+ let princName_as_constr = Tacinterp.constr_of_id (Global.env ()) princName in
+ let init =
+ let nargs = (princ_info.nparams + (List.length princ_info.predicates)) in
+ mkApp(princName_as_constr,
+ Array.init nargs
+ (fun i -> mkRel (nargs - i )))
+ in
+ it_mkLambda_or_LetIn
+ ~init:
+ (it_mkLambda_or_LetIn ~init
+ (List.map change_sort_in_predicate princ_info.predicates)
+ )
+ princ_info.params
+
+
+let pp_dur time time' =
+ str (string_of_float (System.time_difference time time'))
+
+(* End of things to be removed latter : just here to compare
+ saving proof with and without normalizing the proof
+*)
+
+let qed () = Command.save_named true
+let defined () = Command.save_named false
+let generate_functional_principle
+ interactive_proof
+ old_princ_type sorts new_princ_name funs i proof_tac
+ =
+ let f = funs.(i) in
+ let type_sort = Termops.new_sort_in_family InType in
+ let new_sorts =
+ match sorts with
+ | None -> Array.make (Array.length funs) (type_sort)
+ | Some a -> a
+ in
+ (* First we get the type of the old graph principle *)
+ let mutr_nparams = (compute_elim_sig old_princ_type).nparams in
+ (* First we get the type of the old graph principle *)
+ let new_principle_type =
+ compute_new_princ_type_from_rel
+ (Array.map mkConst funs)
+ new_sorts
+ old_princ_type
+ in
+(* observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); *)
+ let base_new_princ_name,new_princ_name =
+ match new_princ_name with
+ | Some (id) -> id,id
+ | None ->
+ let id_of_f = id_of_label (con_label f) in
+ id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
+ in
+ let names = ref [new_princ_name] in
+ let hook _ _ =
+ if sorts = None
+ then
+(* let id_of_f = id_of_label (con_label f) in *)
+ let register_with_sort fam_sort =
+ let s = Termops.new_sort_in_family fam_sort in
+ let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
+ let value =
+ change_property_sort s new_principle_type new_princ_name
+ in
+(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
+ let ce =
+ { const_entry_body = value;
+ const_entry_type = None;
+ const_entry_opaque = false;
+ const_entry_boxed = Options.boxed_definitions()
+ }
+ in
+ ignore(
+ Declare.declare_constant
+ name
+ (Entries.DefinitionEntry ce,
+ Decl_kinds.IsDefinition (Decl_kinds.Scheme)
+ )
+ );
+ names := name :: !names
+ in
+ register_with_sort InProp;
+ register_with_sort InSet
+ in
+ begin
+ Command.start_proof
+ new_princ_name
+ (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
+ new_principle_type
+ hook
+ ;
+ try
+ let _tim1 = System.get_time () in
+ Pfedit.by (proof_tac (Array.map mkConst funs) mutr_nparams);
+ 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; *)
+ let do_save = not (do_observe ()) && not interactive_proof in
+ let _ =
+ try
+(* Vernacentries.show_script (); *)
+ Options.silently defined ();
+ let _dur2 = System.time_difference _tim2 (System.get_time ()) in
+(* Pp.msgnl (str ("Time to check proof: ") ++ str (string_of_float dur2)); *)
+ Options.if_verbose
+ (fun () ->
+ Pp.msgnl (
+ prlist_with_sep
+ (fun () -> str" is defined " ++ fnl ())
+ Ppconstr.pr_id
+ (List.rev !names) ++ str" is defined "
+ )
+ )
+ ()
+ with e when do_save ->
+ msg_warning
+ (
+ Cerrors.explain_exn e
+ );
+ if not (do_observe ())
+ then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end
+ in
+ ()
+
+(* let tim3 = Sys.time () in *)
+(* Pp.msgnl (str ("Time to save proof: ") ++ str (string_of_float (tim3 -. tim2))); *)
+
+ with
+ | e ->
+ msg_warning
+ (
+ Cerrors.explain_exn e
+ );
+ if not ( do_observe ())
+ then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end
+ end
+
+
+
+
+exception Not_Rec
+
+let get_funs_constant mp dp =
+ let rec get_funs_constant const e : (Names.constant*int) array =
+ match kind_of_term (snd (decompose_lam e)) with
+ | Fix((_,(na,_,_))) ->
+ Array.mapi
+ (fun i na ->
+ match na with
+ | Name id ->
+ let const = make_con mp dp (label_of_id id) in
+ const,i
+ | Anonymous ->
+ anomaly "Anonymous fix"
+ )
+ na
+ | _ -> [|const,0|]
+ in
+ function const ->
+ let find_constant_body const =
+ match (Global.lookup_constant const ).const_body with
+ | Some b ->
+ let body = force b in
+ let body = Tacred.cbv_norm_flags
+ (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+ (Global.env ())
+ (Evd.empty)
+ body
+ in
+ body
+ | None -> error ( "Cannot define a principle over an axiom ")
+ in
+ let f = find_constant_body const in
+ let l_const = get_funs_constant const f in
+ (*
+ We need to check that all the functions found are in the same block
+ to prevent Reset stange thing
+ *)
+ let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in
+ let l_params,l_fixes = List.split (List.map decompose_lam l_bodies) in
+ (* all the paremeter must be equal*)
+ let _check_params =
+ let first_params = List.hd l_params in
+ List.iter
+ (fun params ->
+ if not ((=) first_params params)
+ then error "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 kind_of_term body with
+ | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca)
+ | _ ->
+ if is_first && (List.length l_bodies = 1)
+ then raise Not_Rec
+ else error "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 not (first_infos = (extract_info false body))
+ then error "Not a mutal recursive block"
+ in
+ List.iter check l_bodies
+ with Not_Rec -> ()
+ in
+ l_const
+
+exception No_graph_found
+
+let make_scheme fas =
+ let env = Global.env ()
+ and sigma = Evd.empty in
+ let id_to_constr id =
+ Tacinterp.constr_of_id env id
+ in
+ let funs =
+ List.map
+ (fun (_,f,_) ->
+ try id_to_constr f
+ with Not_found ->
+ Util.error ("Cannot find "^ string_of_id f)
+ )
+ fas
+ in
+ let first_fun = destConst (List.hd funs) in
+ let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in
+ let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in
+ let first_fun_kn =
+ try
+ (* Fixme: take into account funs_mp and funs_dp *)
+ fst (destInd (id_to_constr first_fun_rel_id))
+ with Not_found -> raise No_graph_found
+ in
+ let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
+ let this_block_funs = Array.map fst this_block_funs_indexes in
+ let prop_sort = InProp in
+ let funs_indexes =
+ let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
+ List.map
+ (function const -> List.assoc (destConst const) this_block_funs_indexes)
+ funs
+ in
+ let ind_list =
+ List.map
+ (fun (idx) ->
+ let ind = first_fun_kn,idx in
+ let (mib,mip) = Global.lookup_inductive ind in
+ ind,mib,mip,true,prop_sort
+ )
+ funs_indexes
+ in
+ let l_schemes = List.map (Typing.type_of env sigma ) (Indrec.build_mutual_indrec env sigma ind_list) in
+ let i = ref (-1) in
+ let sorts =
+ List.rev_map (fun (_,_,x) ->
+ Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
+ )
+ fas
+ in
+ let princ_names = List.map (fun (x,_,_) -> x) fas in
+ let _ = List.map2
+ (fun princ_name scheme_type ->
+ incr i;
+(* observe (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 *)
+(* ); *)
+ generate_functional_principle
+ false
+ scheme_type
+ (Some (Array.of_list sorts))
+ (Some princ_name)
+ this_block_funs
+ !i
+ (prove_princ_for_struct false !i (Array.of_list (List.map destConst funs)))
+ )
+ princ_names
+ l_schemes
+ in
+ ()
+
+let make_case_scheme fa =
+ let env = Global.env ()
+ and sigma = Evd.empty in
+ let id_to_constr id =
+ Tacinterp.constr_of_id env id
+ in
+ let funs = (fun (_,f,_) -> id_to_constr f) fa in
+ let first_fun = destConst funs in
+ let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in
+ let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in
+ let first_fun_kn =
+ (* Fixme: take into accour funs_mp and funs_dp *)
+ fst (destInd (id_to_constr first_fun_rel_id))
+ in
+ let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
+ let this_block_funs = Array.map fst this_block_funs_indexes in
+ let prop_sort = InProp in
+ let funs_indexes =
+ let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
+ List.assoc (destConst funs) this_block_funs_indexes
+ in
+ let ind_fun =
+ let ind = first_fun_kn,funs_indexes in
+ ind,prop_sort
+ in
+ let scheme_type = (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.make_case_gen env sigma ind sf) ind_fun) in
+ let sorts =
+ (fun (_,_,x) ->
+ Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
+ )
+ fa
+ in
+ let princ_name = (fun (x,_,_) -> x) fa in
+ let _ =
+(* observe (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 *)
+(* ); *)
+ generate_functional_principle
+ false
+ scheme_type
+ (Some ([|sorts|]))
+ (Some princ_name)
+ this_block_funs
+ 0
+ (prove_princ_for_struct false 0 [|destConst funs|])
+ in
+ ()
diff --git a/contrib/funind/functional_principles_types.mli b/contrib/funind/functional_principles_types.mli
new file mode 100644
index 00000000..8b4faaf4
--- /dev/null
+++ b/contrib/funind/functional_principles_types.mli
@@ -0,0 +1,31 @@
+open Names
+open Term
+val generate_functional_principle :
+ (* do we accept interactive proving *)
+ bool ->
+ (* induction principle on rel *)
+ types ->
+ (* *)
+ sorts array option ->
+ (* Name of the new principle *)
+ (identifier) option ->
+ (* the compute functions to use *)
+ constant array ->
+ (* We prove the nth- principle *)
+ int ->
+ (* The tactic to use to make the proof w.r
+ the number of params
+ *)
+ (constr array -> int -> Tacmach.tactic) ->
+ unit
+
+
+
+val compute_new_princ_type_from_rel : constr array -> sorts array ->
+ types -> types
+
+
+exception No_graph_found
+
+val make_scheme : (identifier*identifier*Rawterm.rawsort) list -> unit
+val make_case_scheme : (identifier*identifier*Rawterm.rawsort) -> unit
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 2fcdd3a7..f6d554a8 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -1,7 +1,6 @@
open Util
open Names
open Term
-
open Pp
open Indfun_common
open Libnames
@@ -29,6 +28,11 @@ let interp_casted_constr_with_implicits sigma env impls c =
Constrintern.intern_gen false sigma env ~impls:([],impls)
~allow_soapp:false ~ltacvars:([],[]) c
+
+(*
+ Construct a fixpoint as a Rawterm
+ and not as a constr
+*)
let build_newrecursive
(lnameargsardef) =
let env0 = Global.env()
@@ -71,31 +75,43 @@ let compute_annot (name,annot,args,types,body) =
| None ->
if List.length names > 1 then
user_err_loc
- (dummy_loc,"GenFixpoint",
+ (dummy_loc,"Function",
Pp.str "the recursive argument needs to be specified");
let new_annot = (id_of_name (List.hd names)) in
(name,Struct new_annot,args,types,body)
| Some r -> (name,r,args,types,body)
-
+(* Checks whether or not the mutual bloc is recursive *)
let rec is_rec names =
let names = List.fold_right Idset.add names Idset.empty in
- let check_id id = Idset.mem id names in
- let rec lookup = function
- | RVar(_,id) -> check_id id
+ let check_id id names = Idset.mem id names in
+ let rec lookup names = function
+ | RVar(_,id) -> check_id id names
| RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false
- | RCast(_,b,_,_) -> lookup b
- | RRec _ -> assert false
- | RIf _ -> failwith "Rif not implemented"
- | RLetIn(_,_,t,b) | RLambda(_,_,t,b) | RProd(_,_,t,b) | RLetTuple(_,_,_,t,b) ->
- lookup t || lookup b
- | RApp(_,f,args) -> List.exists lookup (f::args)
+ | RCast(_,b,_,_) -> lookup names b
+ | RRec _ -> error "RRec not handled"
+ | RIf(_,b,_,lhs,rhs) ->
+ (lookup names b) || (lookup names lhs) || (lookup names rhs)
+ | RLetIn(_,na,t,b) | RLambda(_,na,t,b) | RProd(_,na,t,b) ->
+ lookup names t || lookup (Nameops.name_fold Idset.remove na names) b
+ | RLetTuple(_,nal,_,t,b) -> lookup names t ||
+ lookup
+ (List.fold_left
+ (fun acc na -> Nameops.name_fold Idset.remove na acc)
+ names
+ nal
+ )
+ b
+ | RApp(_,f,args) -> List.exists (lookup names) (f::args)
| RCases(_,_,el,brl) ->
- List.exists (fun (e,_) -> lookup e) el ||
- List.exists (fun (_,_,_,ret)-> lookup ret) brl
+ List.exists (fun (e,_) -> lookup names e) el ||
+ List.exists (lookup_br names) brl
+ and lookup_br names (_,idl,_,rt) =
+ let new_names = List.fold_right Idset.remove idl names in
+ lookup new_names rt
in
- lookup
+ lookup names
let prepare_body (name,annot,args,types,body) rt =
let n = (Topconstr.local_binders_length args) in
@@ -139,7 +155,7 @@ let generate_principle
let princ_type =
(Global.lookup_constant princ).Declarations.const_type
in
- New_arg_principle.generate_functional_principle
+ Functional_principles_types.generate_functional_principle
interactive_proof
princ_type
None
@@ -171,12 +187,12 @@ let register_struct is_rec fixpoint_exprl =
| _ ->
Command.build_recursive fixpoint_exprl (Options.boxed_definitions())
-
-let generate_correction_proof_wf tcc_lemma_ref
- is_mes f_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+let generate_correction_proof_wf f_ref tcc_lemma_ref
+ is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
(_: int) (_:Names.constant array) (_:Term.constr array) (_:int) : Tacmach.tactic =
- Recdef.prove_principle tcc_lemma_ref
- is_mes f_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+ Functional_principles_proofs.prove_principle_for_gen
+ (f_ref,functional_ref,eq_ref)
+ tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation
let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
@@ -214,11 +230,11 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
[(f_app_args,None);(body,None)])
in
let eq = Command.generalize_constr_expr unbounded_eq args in
- let hook tcc_lemma_ref f_ref eq_ref rec_arg_num rec_arg_type nb_args relation =
+ let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation =
try
pre_hook
- (generate_correction_proof_wf tcc_lemma_ref is_mes
- f_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
);
Command.save_named true
with e ->
@@ -317,7 +333,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl =
(Topconstr.names_of_local_assums args)
in
let annot =
- try Util.list_index (Name id) names - 1, Topconstr.CStructRec
+ try Some (Util.list_index (Name id) names - 1), Topconstr.CStructRec
with Not_found -> raise (UserError("",str "Cannot find argument " ++ Ppconstr.pr_id id))
in
(name,annot,args,types,body),(None:Vernacexpr.decl_notation)
@@ -325,10 +341,10 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl =
let names = (Topconstr.names_of_local_assums args) in
if is_one_rec recdef && List.length names > 1 then
Util.user_err_loc
- (Util.dummy_loc,"GenFixpoint",
- Pp.str "the recursive argument needs to be specified")
+ (Util.dummy_loc,"Function",
+ Pp.str "the recursive argument needs to be specified in Function")
else
- (name,(0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation)
+ (name,(Some 0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation)
| (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_->
error
("Cannot use mutual definition with well-founded recursion")
@@ -347,12 +363,69 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl =
recdefs
interactive_proof
true
- (New_arg_principle.prove_princ_for_struct interactive_proof);
+ (Functional_principles_proofs.prove_princ_for_struct interactive_proof);
true
in
()
+open Topconstr
+let rec add_args id new_args b =
+ match b with
+ | CRef r ->
+ begin match r with
+ | Libnames.Ident(loc,fname) when fname = id ->
+ CAppExpl(dummy_loc,(None,r),new_args)
+ | _ -> b
+ end
+ | CFix _ | CCoFix _ -> anomaly "add_args : todo"
+ | CArrow(loc,b1,b2) ->
+ CArrow(loc,add_args id new_args b1, add_args id new_args b2)
+ | CProdN(loc,nal,b1) ->
+ CProdN(loc,List.map (fun (nal,b2) -> (nal,add_args id new_args b2)) nal, add_args id new_args b1)
+ | CLambdaN(loc,nal,b1) ->
+ CLambdaN(loc,List.map (fun (nal,b2) -> (nal,add_args id new_args b2)) nal, add_args id new_args b1)
+ | CLetIn(loc,na,b1,b2) ->
+ CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2)
+ | CAppExpl(loc,(pf,r),exprl) ->
+ begin
+ match r with
+ | Libnames.Ident(loc,fname) when fname = id ->
+ CAppExpl(loc,(pf,r),new_args@(List.map (add_args id new_args) exprl))
+ | _ -> CAppExpl(loc,(pf,r),List.map (add_args id new_args) exprl)
+ end
+ | CApp(loc,(pf,b),bl) ->
+ CApp(loc,(pf,add_args id new_args b), List.map (fun (e,o) -> add_args id new_args e,o) bl)
+ | CCases(loc,b_option,cel,cal) ->
+ CCases(loc,Util.option_map (add_args id new_args) b_option,
+ List.map (fun (b,(na,b_option)) -> add_args id new_args b,(na,Util.option_map (add_args id new_args) b_option)) cel,
+ List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal
+ )
+ | CLetTuple(loc,nal,(na,b_option),b1,b2) ->
+ CLetTuple(loc,nal,(na,Util.option_map (add_args id new_args) b_option),
+ add_args id new_args b1,
+ add_args id new_args b2
+ )
+
+ | CIf(loc,b1,(na,b_option),b2,b3) ->
+ CIf(loc,add_args id new_args b1,
+ (na,Util.option_map (add_args id new_args) b_option),
+ add_args id new_args b2,
+ add_args id new_args b3
+ )
+ | CHole _ -> b
+ | CPatVar _ -> b
+ | CEvar _ -> b
+ | CSort _ -> b
+ | CCast(loc,b1,ck,b2) ->
+ CCast(loc,add_args id new_args b1,ck,add_args id new_args b2)
+ | CNotation _ -> anomaly "add_args : CNotation"
+ | CPrim _ -> b
+ | CDelimiters _ -> anomaly "add_args : CDelimiters"
+ | CDynamic _ -> anomaly "add_args : CDynamic"
+
+
+
let make_graph (id:identifier) =
let c_body =
try
@@ -367,8 +440,6 @@ let make_graph (id:identifier) =
| Some b ->
let env = Global.env () in
let body = (force b) in
-
-
let extern_body,extern_type =
let old_implicit_args = Impargs.is_implicit_args ()
and old_strict_implicit_args = Impargs.is_strict_implicit_args ()
@@ -400,68 +471,102 @@ let make_graph (id:identifier) =
Options.raw_print := old_rawprint;
raise e
in
+ let rec get_args b t : Topconstr.local_binder list *
+ Topconstr.constr_expr * Topconstr.constr_expr =
+(* Pp.msgnl (str "body: " ++Ppconstr.pr_lconstr_expr b); *)
+(* Pp.msgnl (str "type: " ++ Ppconstr.pr_lconstr_expr t); *)
+(* Pp.msgnl (fnl ()); *)
+ match b with
+ | Topconstr.CLambdaN (loc, (nal_ta), b') ->
+ begin
+ let n =
+ (List.fold_left (fun n (nal,_) ->
+ n+List.length nal) 0 nal_ta )
+ in
+ let rec chop_n_arrow n t =
+ if n > 0
+ then
+ match t with
+ | Topconstr.CArrow(_,_,t) -> chop_n_arrow (n-1) t
+ | Topconstr.CProdN(_,nal_ta',t') ->
+ let n' =
+ List.fold_left
+ (fun n (nal,t'') ->
+ n+List.length nal) n nal_ta'
+ in
+ assert (n'<= n);
+ chop_n_arrow (n - n') t'
+ | _ -> anomaly "Not enough products"
+ else t
+ in
+ let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in
+ (List.map (fun (nal,ta) -> (Topconstr.LocalRawAssum (nal,ta))) nal_ta)@nal_tas, b'',t''
+ end
+ | _ -> [],b,t
+ in
+ let (nal_tas,b,t) = get_args extern_body extern_type in
let expr_list =
- match extern_body with
+ match b with
| Topconstr.CFix(loc,l_id,fixexprl) ->
- let l =
- List.map
- (fun (id,(n,recexp),bl,t,b) ->
- let nal =
- List.flatten
- (List.map
- (function
- | Topconstr.LocalRawDef (na,_)-> []
- | Topconstr.LocalRawAssum (nal,_) -> nal
- )
- bl
- )
- in
- let rec_id =
- match List.nth nal n with |(_,Name id) -> id | _ -> anomaly ""
- in
- (id, Some (Struct rec_id),bl,t,b)
- )
- fixexprl
- in
- l
- | _ ->
- let rec get_args b t : Topconstr.local_binder list *
- Topconstr.constr_expr * Topconstr.constr_expr =
-(* Pp.msgnl (str "body: " ++Ppconstr.pr_lconstr_expr b); *)
-(* Pp.msgnl (str "type: " ++ Ppconstr.pr_lconstr_expr t); *)
-(* Pp.msgnl (fnl ()); *)
- match b with
- | Topconstr.CLambdaN (loc, (nal_ta), b') ->
- begin
- let n =
- (List.fold_left (fun n (nal,_) ->
- n+List.length nal) 0 nal_ta )
- in
- let rec chop_n_arrow n t =
- if n > 0
- then
- match t with
- | Topconstr.CArrow(_,_,t) -> chop_n_arrow (n-1) t
- | Topconstr.CProdN(_,nal_ta',t') ->
- let n' =
- List.fold_left
- (fun n (nal,t'') ->
- n+List.length nal) n nal_ta'
- in
- assert (n'<= n);
- chop_n_arrow (n - n') t'
- | _ -> anomaly "Not enough products"
- else t
- in
- let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in
- (List.map (fun (nal,ta) -> (Topconstr.LocalRawAssum (nal,ta))) nal_ta)@nal_tas, b'',t''
- end
- | _ -> [],b,t
+ let l =
+ List.map
+ (fun (id,(n,recexp),bl,t,b) ->
+(* let nal = *)
+(* List.flatten *)
+(* (List.map *)
+(* (function *)
+(* | Topconstr.LocalRawDef (na,_)-> [] *)
+(* | Topconstr.LocalRawAssum (nal,_) -> nal *)
+(* ) *)
+(* (nal_tas@bl) *)
+(* ) *)
+(* in *)
+ let bl' =
+ List.flatten
+ (List.map
+ (function
+ | Topconstr.LocalRawDef (na,_)-> []
+ | Topconstr.LocalRawAssum (nal,_) -> nal
+ )
+ bl
+ )
+ in
+ let rec_id =
+ match List.nth bl' (out_some n) with |(_,Name id) -> id | _ -> anomaly ""
+ in
+ let new_args =
+ List.flatten
+ (List.map
+ (function
+ | Topconstr.LocalRawDef (na,_)-> []
+ | Topconstr.LocalRawAssum (nal,_) -> List.map (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n))) nal
+ )
+ nal_tas
+ )
+ in
+ let b' = add_args id new_args b in
+ (id, Some (Struct rec_id),nal_tas@bl,t,b')
+ )
+ fixexprl
in
- let nal_tas,b,t = get_args extern_body extern_type in
+ l
+ | _ ->
[(id,None,nal_tas,t,b)]
-
in
+(* List.iter (fun (id,rec_arg,bl,t,b) -> *)
+(* Pp.msgnl *)
+(* (Ppconstr.pr_id id ++ *)
+(* Ppconstr.pr_binders bl ++ *)
+(* begin match rec_arg with *)
+(* | Some (Struct id) -> str " { struct " ++ Ppconstr.pr_id id ++ str " }" *)
+(* | _ -> (mt ()) *)
+(* end ++ *)
+(* str " : " ++ Ppconstr.pr_lconstr_expr t ++ *)
+(* str " := " ++ *)
+(* Ppconstr.pr_lconstr_expr b *)
+(* ) *)
+(* ) *)
+(* expr_list; *)
do_generate_principle false false expr_list
(* let make_graph _ = assert false *)
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index 7b3d8cbd..61f26d30 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -13,37 +13,72 @@ open Topconstr
open Indfun_common
open Indfun
open Genarg
+open Pcoq
-TACTIC EXTEND newfuninv
- [ "functional" "inversion" ident(hyp) ident(fname) ] ->
- [
- Invfun.invfun hyp fname
- ]
-END
+let pr_binding prc = function
+ | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c)
+ | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
+
+let pr_bindings prc prlc = function
+ | Rawterm.ImplicitBindings l ->
+ brk (1,1) ++ str "with" ++ brk (1,1) ++
+ Util.prlist_with_sep spc prc l
+ | Rawterm.ExplicitBindings l ->
+ brk (1,1) ++ str "with" ++ brk (1,1) ++
+ Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+ | Rawterm.NoBindings -> mt ()
+
+
+let pr_with_bindings prc prlc (c,bl) =
+ prc c ++ hv 0 (pr_bindings prc prlc bl)
-let pr_fun_ind_using prc _ _ opt_c =
- match opt_c with
+let pr_fun_ind_using prc prlc _ opt_c =
+ match opt_c with
| None -> mt ()
- | Some c -> spc () ++ hov 2 (str "using" ++ spc () ++ prc c)
+ | Some c -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc c)
ARGUMENT EXTEND fun_ind_using
- TYPED AS constr_opt
+ TYPED AS constr_with_bindings_opt
PRINTED BY pr_fun_ind_using
-| [ "using" constr(c) ] -> [ Some c ]
+| [ "using" constr_with_bindings(c) ] -> [ Some c ]
| [ ] -> [ None ]
END
-let pr_intro_as_pat prc _ _ pat =
- str "as" ++ spc () ++ pr_intro_pattern pat
+TACTIC EXTEND newfuninv
+ [ "functional" "inversion" ident(hyp) ident(fname) fun_ind_using(princl)] ->
+ [
+ fun g ->
+ let fconst = const_of_id fname in
+ let princ =
+ match princl with
+ | None ->
+ let f_ind_id =
+ (
+ Indrec.make_elimination_ident
+ fname
+ (Tacticals.elimination_sort_of_goal g)
+ )
+ in
+ let princ = const_of_id f_ind_id in
+ princ
+ | Some princ -> destConst (fst princ)
+ in
+ Invfun.invfun hyp fconst princ g
+ ]
+END
+let pr_intro_as_pat prc _ _ pat =
+ match pat with
+ | Some pat -> spc () ++ str "as" ++ spc () ++ pr_intro_pattern pat
+ | None -> mt ()
-ARGUMENT EXTEND with_names TYPED AS intro_pattern PRINTED BY pr_intro_as_pat
-| [ "as" simple_intropattern(ipat) ] -> [ ipat ]
-| [] ->[ IntroAnonymous ]
+ARGUMENT EXTEND with_names TYPED AS intro_pattern_opt PRINTED BY pr_intro_as_pat
+| [ "as" simple_intropattern(ipat) ] -> [ Some ipat ]
+| [] ->[ None ]
END
@@ -61,16 +96,25 @@ let is_rec scheme_info =
let choose_dest_or_ind scheme_info =
if is_rec scheme_info
then Tactics.new_induct
- else
- Tactics.new_destruct
+ else Tactics.new_destruct
TACTIC EXTEND newfunind
- ["new" "functional" "induction" constr(c) fun_ind_using(princl) with_names(pat)] ->
+ ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
[
+ let pat =
+ match pat with
+ | None -> IntroAnonymous
+ | Some pat -> pat
+ in
+ let c = match cl with
+ | [] -> assert false
+ | [c] -> c
+ | c::cl -> applist(c,cl)
+ in
let f,args = decompose_app c in
fun g ->
- let princ =
+ let princ,bindings =
match princl with
| None -> (* No principle is given let's find the good one *)
let fname =
@@ -86,7 +130,7 @@ TACTIC EXTEND newfunind
(Tacticals.elimination_sort_of_goal g)
)
in
- mkConst(const_of_id princ_name )
+ mkConst(const_of_id princ_name ),Rawterm.NoBindings
| Some princ -> princ
in
let princ_type = Tacmach.pf_type_of g princ in
@@ -98,12 +142,46 @@ TACTIC EXTEND newfunind
in
List.map (fun c -> Tacexpr.ElimOnConstr c) (args@c_list)
in
- let princ' = Some (princ,Rawterm.NoBindings) in
- choose_dest_or_ind
+ let princ' = Some (princ,bindings) in
+ let princ_vars =
+ List.fold_right
+ (fun a acc ->
+ try Idset.add (destVar a) acc
+ with _ -> acc
+ )
+ args
+ Idset.empty
+ in
+ let old_idl = List.fold_right Idset.add (Tacmach.pf_ids_of_hyps g) Idset.empty in
+ let old_idl = Idset.diff old_idl princ_vars in
+ let subst_and_reduce g =
+ let idl =
+ Util.map_succeed
+ (fun id ->
+ if Idset.mem id old_idl then failwith "";
+ id
+ )
+ (Tacmach.pf_ids_of_hyps g)
+ in
+ let flag =
+ Rawterm.Cbv
+ {Rawterm.all_flags
+ with Rawterm.rDelta = false;
+ }
+ in
+ Tacticals.tclTHEN
+ (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst [id])) idl )
+ (Hiddentac.h_reduce flag Tacticals.allClauses)
+ g
+ in
+ Tacticals.tclTHEN
+ (choose_dest_or_ind
princ_infos
args_as_induction_constr
princ'
- pat g
+ pat)
+ subst_and_reduce
+ g
]
END
@@ -111,7 +189,7 @@ END
VERNAC ARGUMENT EXTEND rec_annotation2
[ "{" "struct" ident(id) "}"] -> [ Struct id ]
| [ "{" "wf" constr(r) ident_opt(id) "}" ] -> [ Wf(r,id) ]
-| [ "{" "mes" constr(r) ident_opt(id) "}" ] -> [ Mes(r,id) ]
+| [ "{" "measure" constr(r) ident_opt(id) "}" ] -> [ Mes(r,id) ]
END
@@ -130,7 +208,7 @@ VERNAC ARGUMENT EXTEND rec_definition2
let check_one_name () =
if List.length names > 1 then
Util.user_err_loc
- (Util.dummy_loc,"GenFixpoint",
+ (Util.dummy_loc,"Function",
Pp.str "the recursive argument needs to be specified");
in
let check_exists_args an =
@@ -138,7 +216,7 @@ VERNAC ARGUMENT EXTEND rec_definition2
let id = match an with Struct id -> id | Wf(_,Some id) -> id | Mes(_,Some id) -> id | Wf(_,None) | Mes(_,None) -> failwith "check_exists_args" in
(try ignore(Util.list_index (Name id) names - 1); annot
with Not_found -> Util.user_err_loc
- (Util.dummy_loc,"GenFixpoint",
+ (Util.dummy_loc,"Function",
Pp.str "No argument named " ++ Nameops.pr_id id)
)
with Failure "check_exists_args" -> check_one_name ();annot
@@ -160,16 +238,11 @@ VERNAC ARGUMENT EXTEND rec_definitions2
END
-VERNAC COMMAND EXTEND GenFixpoint
- ["GenFixpoint" rec_definitions2(recsl)] ->
+VERNAC COMMAND EXTEND Function
+ ["Function" rec_definitions2(recsl)] ->
[ do_generate_principle false recsl]
END
-VERNAC COMMAND EXTEND IGenFixpoint
- ["IGenFixpoint" rec_definitions2(recsl)] ->
- [ do_generate_principle true recsl]
-END
-
VERNAC ARGUMENT EXTEND fun_scheme_arg
| [ ident(princ_name) ":=" "Induction" "for" ident(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ]
@@ -181,17 +254,28 @@ VERNAC ARGUMENT EXTEND fun_scheme_args
END
VERNAC COMMAND EXTEND NewFunctionalScheme
- ["New" "Functional" "Scheme" fun_scheme_args(fas) ] ->
+ ["Functional" "Scheme" fun_scheme_args(fas) ] ->
[
- New_arg_principle.make_scheme fas
+ try
+ Functional_principles_types.make_scheme fas
+ with Functional_principles_types.No_graph_found ->
+ match fas with
+ | (_,fun_name,_)::_ ->
+ begin
+ make_graph fun_name;
+ try Functional_principles_types.make_scheme fas
+ with Functional_principles_types.No_graph_found ->
+ Util.error ("Cannot generate induction principle(s)")
+ end
+ | _ -> assert false (* we can only have non empty list *)
]
END
VERNAC COMMAND EXTEND NewFunctionalCase
- ["New" "Functional" "Case" fun_scheme_arg(fas) ] ->
+ ["Functional" "Case" fun_scheme_arg(fas) ] ->
[
- New_arg_principle.make_case_scheme fas
+ Functional_principles_types.make_case_scheme fas
]
END
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 1f711297..2e5616f0 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -88,18 +88,9 @@ let gen_fargs fargs : tactic =
g
-let invfun (hypname:identifier) (fid:identifier) : tactic=
+let invfun (hypname:identifier) fname princ : tactic=
fun g ->
let nprod_goal = nb_prod (pf_concl g) in
- let f_ind_id =
- (
- Indrec.make_elimination_ident
- fid
- (Tacticals.elimination_sort_of_goal g)
- )
- in
- let fname = const_of_id fid in
- let princ = const_of_id f_ind_id in
let princ_info =
let princ_type =
(try (match (Global.lookup_constant princ) with
@@ -114,7 +105,7 @@ let invfun (hypname:identifier) (fid:identifier) : tactic=
let frealargs = (snd (array_chop (List.length princ_info.params) fargs))
in
let pat_args =
- (List.map (fun e -> ([-1],e)) (Array.to_list frealargs)) @ [[],appf]
+ (List.map (fun e -> ([Rawterm.ArgArg (-1)],e)) (Array.to_list frealargs)) @ [[],appf]
in
tclTHENSEQ
[
diff --git a/contrib/funind/new_arg_principle.ml b/contrib/funind/new_arg_principle.ml
deleted file mode 100644
index 8ef23c48..00000000
--- a/contrib/funind/new_arg_principle.ml
+++ /dev/null
@@ -1,1770 +0,0 @@
-open Printer
-open Util
-open Term
-open Termops
-open Names
-open Declarations
-open Pp
-open Entries
-open Hiddentac
-open Evd
-open Tacmach
-open Proof_type
-open Tacticals
-open Tactics
-open Indfun_common
-
-
-let msgnl = Pp.msgnl
-
-let do_observe () =
- Tacinterp.get_debug () <> Tactic_debug.DebugOff
-
-
-let observe strm =
- if do_observe ()
- then Pp.msgnl strm
- else ()
-
-let observennl strm =
- if do_observe ()
- then begin Pp.msg strm;Pp.pp_flush () end
- else ()
-
-
-
-
-let do_observe_tac s tac g =
- try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v
- with e ->
- let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in
- msgnl (str "observation "++str s++str " raised exception " ++
- Cerrors.explain_exn e ++ str "on goal " ++ goal );
- raise e;;
-
-
-let observe_tac s tac g =
- if do_observe ()
- then do_observe_tac s tac g
- else tac g
-
-
-let tclTRYD tac =
- if !Options.debug || do_observe ()
- then (fun g -> try do_observe_tac "" tac g with _ -> tclIDTAC g)
- else tac
-
-
-let list_chop ?(msg="") n l =
- try
- list_chop n l
- with Failure (msg') ->
- failwith (msg ^ msg')
-
-
-let make_refl_eq type_of_t t =
- let refl_equal_term = Lazy.force refl_equal in
- mkApp(refl_equal_term,[|type_of_t;t|])
-
-
-type static_fix_info =
- {
- idx : int;
- name : identifier;
- types : types
- }
-
-type static_infos =
- {
- fixes_ids : identifier list;
- ptes_to_fixes : static_fix_info Idmap.t
- }
-
-type 'a dynamic_info =
- {
- nb_rec_hyps : int;
- rec_hyps : identifier list ;
- eq_hyps : identifier list;
- info : 'a
- }
-
-let finish_proof dynamic_infos g =
- observe_tac "finish"
- h_assumption
- g
-
-
-let refine c =
- Tacmach.refine_no_check c
-
-let thin l =
- Tacmach.thin_no_check l
-
-
-let cut_replacing id t tac :tactic=
- tclTHENS (cut t)
- [ tclTHEN (thin_no_check [id]) (introduction_no_check id);
- tac
- ]
-
-let intro_erasing id = tclTHEN (thin [id]) (introduction id)
-
-
-
-let rec_hyp_id = id_of_string "rec_hyp"
-
-let is_trivial_eq t =
- match kind_of_term t with
- | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) ->
- eq_constr t1 t2
- | _ -> false
-
-
-let rec incompatible_constructor_terms t1 t2 =
- let c1,arg1 = decompose_app t1
- and c2,arg2 = decompose_app t2
- in
- (not (eq_constr t1 t2)) &&
- isConstruct c1 && isConstruct c2 &&
- (
- not (eq_constr c1 c2) ||
- List.exists2 incompatible_constructor_terms arg1 arg2
- )
-
-let is_incompatible_eq t =
- match kind_of_term t with
- | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) ->
- incompatible_constructor_terms t1 t2
- | _ -> false
-
-let change_hyp_with_using hyp_id t tac =
- fun g ->
- let prov_id = pf_get_new_id hyp_id g in
- tclTHENLIST
- [
- forward (Some tac) (Genarg.IntroIdentifier prov_id) t;
- thin [hyp_id];
- h_rename prov_id hyp_id
- ] g
-
-exception TOREMOVE
-
-
-let prove_trivial_eq h_id context (type_of_term,term) =
- let nb_intros = List.length context in
- tclTHENLIST
- [
- tclDO nb_intros 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(Lazy.force refl_equal,[|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 isAppConstruct t =
- if isApp t
- then isConstruct (fst (destApp t))
- else false
-
-
-let nf_betaoiotazeta = Reductionops.local_strong Reductionops.whd_betaiotazeta
-
-let remove_useless_rel env sigma hyp_id (context:Sign.rel_context) t end_of_type t1 t2 =
- let rel_num = destRel t2 in
-
- let nb_kept = List.length context - rel_num
- and nb_popped = rel_num - 1
- in
-
- (* We remove the equation *)
- let new_end_of_type = pop end_of_type in
-
- let lt_relnum,ge_relnum =
- list_chop
- ~msg:("removing useless variable "^(string_of_int rel_num)^" :")
- nb_popped
- context
- in
- (* we rebuilt the type of hypothesis after the rel to remove *)
- let hyp_type_lt_relnum =
- it_mkProd_or_LetIn ~init:new_end_of_type lt_relnum
- in
- (* we replace Rel 1 by t1 *)
- let new_hyp_type_lt_relnum = subst1 t1 hyp_type_lt_relnum in
- (* we resplit the type of hyp_type *)
- let new_lt_relnum,new_end_of_type =
- Sign.decompose_prod_n_assum nb_popped new_hyp_type_lt_relnum
- in
- (* and rebuilt new context of hyp *)
- let new_context = new_lt_relnum@(List.tl ge_relnum) in
- let new_typ_of_hyp =
- nf_betaoiotazeta (it_mkProd_or_LetIn ~init:new_end_of_type new_context)
- in
- let prove_simpl_eq =
- tclTHENLIST
- [
- tclDO (nb_popped + nb_kept) intro;
- (fun g' ->
- let new_hyps_ids = pf_ids_of_hyps g' in
- let popped_ids,others =
- list_chop ~msg:"removing useless variable pop :"
- nb_popped new_hyps_ids in
- let kept_ids,_ =
- list_chop ~msg: " removing useless variable kept : "
- nb_kept others
- in
- let rev_to_apply =
- (mkApp(Lazy.force refl_equal,[|Typing.type_of env sigma t1;t1|]))::
- ((List.map mkVar popped_ids)@
- (t1::
- (List.map mkVar kept_ids)))
- in
- let to_refine = applist(mkVar hyp_id,List.rev rev_to_apply) in
- refine to_refine g'
- )
- ]
- in
- let simpl_eq_tac = change_hyp_with_using hyp_id new_typ_of_hyp
- (observe_tac "prove_simpl_eq" prove_simpl_eq)
- in
- let new_end_of_type = nf_betaoiotazeta new_end_of_type in
- (new_context,new_end_of_type,simpl_eq_tac),new_typ_of_hyp,
- (str " removing useless variable " ++ str (string_of_int rel_num) )
-
-
-let decompose_eq env sigma hyp_id (context:Sign.rel_context) t end_of_type t1 t2 =
- let c1,args1 = destApp t1
- and c2,args2 = destApp t2
- in
- (* This tactic must be used after is_incompatible_eq *)
- assert (eq_constr c1 c2);
- (* we remove this equation *)
- let new_end_of_type = pop end_of_type in
- let new_eqs =
- array_map2_i
- (fun i arg1 arg2 ->
- let new_eq =
- let type_of_arg = Typing.type_of env sigma arg1 in
- mkApp(Lazy.force eq,[|type_of_arg;arg1;arg2|])
- in
- Anonymous,None,lift i new_eq
- )
- args1
- args2
- in
- let nb_new_eqs = Array.length new_eqs in
- (* we add the new equation *)
- let new_end_of_type = lift nb_new_eqs new_end_of_type in
- let local_context =
- List.rev (Array.to_list new_eqs) in
- let new_end_of_type = it_mkProd_or_LetIn ~init:new_end_of_type local_context in
- let new_typ_of_hyp =
- nf_betaoiotazeta (it_mkProd_or_LetIn ~init:new_end_of_type context)
- in
- let prove_pattern_simplification =
- let context_length = List.length context in
- tclTHENLIST
- [
- tclDO (context_length + nb_new_eqs) intro ;
- (fun g ->
- let new_eqs,others =
- list_chop ~msg:"simplifying pattern : new_eqs" nb_new_eqs (pf_hyps g)
- in
- let context_hyps,_ = list_chop ~msg:"simplifying pattern : context_hyps"
- context_length others in
- let eq_args =
- List.rev_map
- (fun (_,_, eq) -> let _,args = destApp eq in args.(1),args.(2))
- new_eqs
- in
- let lhs_args,rhs_args = List.split eq_args in
- let lhs_eq = applist(c1,lhs_args)
- and rhs_eq = applist(c1,rhs_args)
- in
- let type_of_eq = pf_type_of g lhs_eq in
- let eq_to_assert =
- mkApp(Lazy.force eq,[|type_of_eq;lhs_eq;rhs_eq|])
- in
- let prove_new_eq =
- tclTHENLIST [
- tclMAP
- (fun (id,_,_) ->
- (* The tclTRY here is used when trying to rewrite
- on Set
- eg (@cons A x l)=(@cons A x' l') generates 3 eqs
- A=A -> x=x' -> l = l' ...
-
- *)
- tclTRY (Equality.rewriteLR (mkVar id))
- )
- new_eqs;
- reflexivity
- ]
- in
- let new_eq_id = pf_get_new_id (id_of_string "H") g in
- let create_new_eq =
- forward
- (Some (observe_tac "prove_new_eq" (prove_new_eq)))
- (Genarg.IntroIdentifier new_eq_id)
- eq_to_assert
- in
- let to_refine =
- applist (
- mkVar hyp_id,
- List.rev ((mkVar new_eq_id)::
- (List.map (fun (id,_,_) -> mkVar id) context_hyps)))
- in
- tclTHEN
- (observe_tac "create_new_eq" create_new_eq )
- (observe_tac "refine in decompose_eq " (refine to_refine))
- g
- )
- ]
- in
- let simpl_eq_tac =
- change_hyp_with_using hyp_id new_typ_of_hyp (observe_tac "prove_pattern_simplification " prove_pattern_simplification)
- in
- (context,nf_betaoiotazeta new_end_of_type,simpl_eq_tac),new_typ_of_hyp,
- str "simplifying an equation "
-
-let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type =
- if not (noccurn 1 end_of_type)
- then (* if end_of_type depends on this term we don't touch it *)
- begin
- observe (str "Not treating " ++ pr_lconstr t );
- failwith "NoChange";
- end;
- let res,new_typ_of_hyp,msg =
- if not (isApp t) then failwith "NoChange";
- let f,args = destApp t in
- if not (eq_constr f (Lazy.force eq)) then failwith "NoChange";
- let t1 = args.(1)
- and t2 = args.(2)
- in
- if isRel t2 && closed0 t1 then (* closed_term = x with x bound in context *)
- begin
- remove_useless_rel env sigma hyp_id (context:Sign.rel_context) t end_of_type t1 t2
- end
- else if isAppConstruct t1 && isAppConstruct t2 (* C .... = C .... *)
- then decompose_eq env sigma hyp_id context t end_of_type t1 t2
- else failwith "NoChange"
- in
- observe (str "In " ++ Ppconstr.pr_id hyp_id ++
- msg ++ 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_typ_of_hyp ++ fnl ());
- (res:'a*'b*'c)
-
-
-
-
-let is_property static_info t_x =
- if isApp t_x
- then
- let pte,args = destApp t_x in
- if isVar pte && array_for_all closed0 args
- then Idmap.mem (destVar pte) static_info.ptes_to_fixes
- else false
- else false
-
-let isLetIn t =
- match kind_of_term t with
- | LetIn _ -> true
- | _ -> false
-
-
-let h_reduce_with_zeta =
- h_reduce
- (Rawterm.Cbv
- {Rawterm.all_flags
- with Rawterm.rDelta = false;
- })
-
-(*
-let rewrite_until_var arg_num : tactic =
- let constr_eq = Lazy.force eq in
- let replace_if_unify arg (pat,cl,id,lhs) : tactic =
- fun g ->
- try
- let (evd,matched) =
- Unification.w_unify_to_subterm
- (pf_env g) ~mod_delta:false (pat,arg) cl.Clenv.env
- in
- let cl' = {cl with Clenv.env = evd } in
- let c2 = Clenv.clenv_nf_meta cl' lhs in
- (Equality.replace matched c2) g
- with _ -> tclFAIL 0 (str "") g
- in
- let rewrite_on_step equalities : tactic =
- fun g ->
- match kind_of_term (pf_concl g) with
- | App(_,args) when (not (test_var args arg_num)) ->
-(* tclFIRST (List.map (fun a -> observe_tac (str "replace_if_unify") (replace_if_unify args.(arg_num) a)) equalities) g *)
- tclFIRST (List.map (replace_if_unify args.(arg_num)) equalities) g
- | _ ->
- raise (Util.UserError("", (str "No more rewrite" ++
- pr_lconstr_env (pf_env g) (pf_concl g))))
- in
- fun g ->
- let equalities =
- List.filter
- (
- fun (_,_,id_t) ->
- match kind_of_term id_t with
- | App(f,_) -> eq_constr f constr_eq
- | _ -> false
- )
- (pf_hyps g)
- in
- let f (id,_,ctype) =
- let c = mkVar id in
- let eqclause = Clenv.make_clenv_binding g (c,ctype) Rawterm.NoBindings in
- let clause_type = Clenv.clenv_type eqclause in
- let f,args = decompose_app (clause_type) in
- let rec split_last_two = function
- | [c1;c2] -> (c1, c2)
- | x::y::z ->
- split_last_two (y::z)
- | _ ->
- error ("The term provided is not an equivalence")
- in
- let (c1,c2) = split_last_two args in
- (c2,eqclause,id,c1)
- in
- let matching_hyps = List.map f equalities in
- tclTRY (tclREPEAT (tclPROGRESS (rewrite_on_step matching_hyps))) g
-
-*)
-
-
-let rewrite_until_var arg_num eq_ids : tactic =
- let test_var g =
- let _,args = destApp (pf_concl g) in
- isVar args.(arg_num)
- in
- let rec do_rewrite eq_ids g =
- if test_var g
- then tclIDTAC g
- else
- match eq_ids with
- | [] -> anomaly "Cannot find a way to prove recursive property";
- | eq_id::eq_ids ->
- tclTHEN
- (tclTRY (Equality.rewriteRL (mkVar eq_id)))
- (do_rewrite eq_ids)
- g
- in
- do_rewrite eq_ids
-
-let prove_rec_hyp eq_hyps fix_info =
- tclTHEN
- (rewrite_until_var (fix_info.idx - 1) eq_hyps)
- (fun g ->
- let _,pte_args = destApp (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 rec_pte_id = id_of_string "Hrec"
-let clean_hyp_with_heq static_infos eq_hyps hyp_id env sigma =
- let coq_False = Coqlib.build_coq_False () in
- let coq_True = Coqlib.build_coq_True () in
- let coq_I = Coqlib.build_coq_I () in
- let rec scan_type context type_of_hyp : tactic =
- if isLetIn type_of_hyp then
- let real_type_of_hyp = it_mkProd_or_LetIn ~init:type_of_hyp context in
- let reduced_type_of_hyp = nf_betaoiotazeta real_type_of_hyp in
- (* length of context didn't change ? *)
- let new_context,new_typ_of_hyp =
- Sign.decompose_prod_n_assum (List.length context) reduced_type_of_hyp
- in
- tclTHENLIST
- [
- h_reduce_with_zeta
- (Tacticals.onHyp hyp_id)
- ;
- scan_type new_context new_typ_of_hyp
-
- ]
- else if isProd type_of_hyp
- then
- begin
- let (x,t_x,t') = destProd type_of_hyp in
- if is_property static_infos t_x then
- begin
- let pte,pte_args = (destApp t_x) in
- let fix_info = Idmap.find (destVar pte) static_infos.ptes_to_fixes in
- let popped_t' = pop t' in
- let real_type_of_hyp = it_mkProd_or_LetIn ~init:popped_t' context in
- let prove_new_type_of_hyp =
- let context_length = List.length context in
- tclTHENLIST
- [
- tclDO context_length 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
- tclTHENLIST
- [
- forward
- (Some (prove_rec_hyp eq_hyps fix_info))
- (Genarg.IntroIdentifier rec_pte_id)
- t_x;
- refine to_refine
- ]
- g
- )
- ]
- in
- tclTHENLIST
- [
- observe_tac "hyp rec"
- (change_hyp_with_using hyp_id real_type_of_hyp prove_new_type_of_hyp);
- scan_type context popped_t'
- ]
- end
- else if eq_constr 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 t_x then raise TOREMOVE (* t_x := C1 ... = C2 ... *)
- else if eq_constr t_x coq_True (* Trivial => we remove this precons *)
- then
- let _ =
- observe (str "In "++Ppconstr.pr_id hyp_id++
- str " removing useless precond True"
- )
- in
- let popped_t' = pop t' in
- let real_type_of_hyp =
- it_mkProd_or_LetIn ~init:popped_t' context
- in
- let prove_trivial =
- let nb_intro = List.length context in
- tclTHENLIST [
- tclDO nb_intro 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 hyp_id real_type_of_hyp (observe_tac "prove_trivial" prove_trivial);
- scan_type context popped_t'
- ]
- else if is_trivial_eq 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 ~init:popped_t' context
- in
- let _,args = destApp t_x in
- tclTHENLIST
- [
- change_hyp_with_using
- hyp_id
- real_type_of_hyp
- (observe_tac "prove_trivial_eq" (prove_trivial_eq hyp_id context (args.(0),args.(1))));
- 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 Failure "NoChange" ->
- (* Last thing todo : push the rel in the context and continue *)
- scan_type ((x,None,t_x)::context) t'
- end
- end
- else
- tclIDTAC
- in
- try
- scan_type [] (Typing.type_of env sigma (mkVar hyp_id)), [hyp_id]
- with TOREMOVE ->
- thin [hyp_id],[]
-
-
-let clean_goal_with_heq static_infos continue_tac dyn_infos =
- fun g ->
- let env = pf_env g
- and sigma = project g
- in
- let tac,new_hyps =
- List.fold_left (
- fun (hyps_tac,new_hyps) hyp_id ->
- let hyp_tac,new_hyp =
- clean_hyp_with_heq static_infos dyn_infos.eq_hyps hyp_id env sigma
- in
- (tclTHEN hyp_tac hyps_tac),new_hyp@new_hyps
- )
- (tclIDTAC,[])
- dyn_infos.rec_hyps
- in
- let new_infos =
- { dyn_infos with
- rec_hyps = new_hyps;
- nb_rec_hyps = List.length new_hyps
- }
- in
- tclTHENLIST
- [
- tac ;
- (continue_tac new_infos)
- ]
- g
-
-let heq_id = id_of_string "Heq"
-
-let treat_new_case static_infos nb_prod continue_tac term dyn_infos =
- fun g ->
- let heq_id = pf_get_new_id heq_id g in
- let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in
- tclTHENLIST
- [
- (* We first introduce the variables *)
- tclDO nb_first_intro (intro_avoiding dyn_infos.rec_hyps);
- (* Then the equation itself *)
- introduction_no_check heq_id;
- (* Then the new hypothesis *)
- tclMAP introduction_no_check dyn_infos.rec_hyps;
- observe_tac "after_introduction" (fun g' ->
- (* We get infos on the equations introduced*)
- let new_term_value_eq = pf_type_of g' (mkVar heq_id) in
- (* compute the new value of the body *)
- let new_term_value =
- match kind_of_term new_term_value_eq with
- | App(f,[| _;_;args2 |]) -> args2
- | _ ->
- observe (pr_gls g' ++ fnl () ++ str "last hyp is" ++
- pr_lconstr_env (pf_env g') new_term_value_eq
- );
- assert false
- in
- let fun_body =
- mkLambda(Anonymous,
- pf_type_of g' term,
- replace_term 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 static_infos continue_tac new_infos g'
- )
- ]
- g
-
-let do_prove_princ_for_struct
- (interactive_proof:bool)
- (fnames:constant list)
- static_infos
-(* (ptes:identifier list) *)
-(* (fixes:(int*constr*identifier*constr) Idmap.t) *)
-(* (hyps: identifier list) *)
-(* (term:constr) *)
- dyn_infos
- : tactic =
-(* let fixes_ids = Idmap.fold (fun _ (_,_,id,_) acc -> id::acc) fixes [] in *)
- let rec do_prove_princ_for_struct_aux do_finalize dyn_infos : tactic =
- fun g ->
-(* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
- match kind_of_term dyn_infos.info with
- | Case(_,_,t,_) ->
- let g_nb_prod = nb_prod (pf_concl g) in
- let type_of_term = pf_type_of g t in
- let term_eq =
- make_refl_eq type_of_term t
- in
- tclTHENSEQ
- [
- h_generalize (term_eq::List.map mkVar dyn_infos.rec_hyps);
- thin dyn_infos.rec_hyps;
- pattern_option [[-1],t] None;
- h_simplest_case t;
- (fun g' ->
- let g'_nb_prod = nb_prod (pf_concl g') in
- let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
- observe_tac "treat_new_case"
- (treat_new_case
- static_infos
- nb_instanciate_partial
- (do_prove_princ_for_struct do_finalize)
- t
- dyn_infos)
- g'
- )
-
- ] g
- | Lambda(n,t,b) ->
- begin
- match kind_of_term( pf_concl g) with
- | Prod _ ->
- tclTHEN
- intro
- (fun g' ->
- let (id,_,_) = pf_last_hyp g' 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
- do_prove_princ_for_struct do_finalize new_infos g'
- ) g
- | _ ->
- do_finalize dyn_infos g
- end
- | Cast(t,_,_) ->
- do_prove_princ_for_struct do_finalize {dyn_infos with info = t} g
- | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
- do_finalize dyn_infos g
- | App(_,_) ->
- let f,args = decompose_app dyn_infos.info in
- begin
- match kind_of_term f with
- | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ ->
- let new_infos =
- { dyn_infos with
- info = (f,args)
- }
- in
- do_prove_princ_for_struct_args do_finalize new_infos g
- | Const c when not (List.mem c fnames) ->
- let new_infos =
- { dyn_infos with
- info = (f,args)
- }
- in
- do_prove_princ_for_struct_args do_finalize new_infos g
- | Const _ ->
- do_finalize dyn_infos g
- | _ ->
-(* observe *)
-(* (str "Applied binders not yet implemented: in "++ fnl () ++ *)
-(* pr_lconstr_env (pf_env g) term ++ fnl () ++ *)
-(* pr_lconstr_env (pf_env g) f ++ spc () ++ str "is applied") ; *)
- tclFAIL 0 (str "TODO : Applied binders not yet implemented") g
- end
- | Fix _ | CoFix _ ->
- error ( "Anonymous local (co)fixpoints are not handled yet")
-
- | Prod _ -> assert false
- | LetIn _ ->
- let new_infos =
- { dyn_infos with
- info = nf_betaoiotazeta dyn_infos.info
- }
- in
-
- tclTHENLIST
- [tclMAP
- (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id))
- dyn_infos.rec_hyps;
- h_reduce_with_zeta Tacticals.onConcl;
- do_prove_princ_for_struct do_finalize new_infos
- ] g
- | _ ->
- errorlabstrm "" (str "in do_prove_princ_for_struct found : "(* ++ *)
-(* pr_lconstr_env (pf_env g) term *)
- )
- and do_prove_princ_for_struct do_finalize dyn_infos g =
-(* observe (str "proving with "++Printer.pr_lconstr term++ str " on goal " ++ pr_gls g); *)
- do_prove_princ_for_struct_aux do_finalize dyn_infos g
- and do_prove_princ_for_struct_args do_finalize dyn_infos (* f_args' args *) :tactic =
- fun g ->
-(* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *)
-(* then msgnl (str "do_prove_princ_for_struct_args with " ++ *)
-(* pr_lconstr_env (pf_env g) f_args' *)
-(* ); *)
- let (f_args',args) = dyn_infos.info in
- let tac =
- match args with
- | [] ->
- do_finalize {dyn_infos with info = f_args'}
- | arg::args ->
- let do_finalize dyn_infos =
- let new_arg = dyn_infos.info in
- tclTRYD
- (do_prove_princ_for_struct_args
- do_finalize
- {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args}
- )
- in
- do_prove_princ_for_struct do_finalize
- {dyn_infos with info = arg }
- in
- tclTRYD(tac ) g
- in
- let do_finish_proof dyn_infos =
- clean_goal_with_heq
- static_infos
- finish_proof dyn_infos
- in
- observe_tac "do_prove_princ_for_struct"
- (do_prove_princ_for_struct do_finish_proof dyn_infos)
-
-let is_pte_type t =
- isSort (snd (decompose_prod t))
-
-let is_pte (_,_,t) = is_pte_type t
-
-exception Not_Rec
-
-
-
-let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id =
- let args = Array.of_list (List.map mkVar args_id) in
- let instanciate_one_hyp hid =
- tclORELSE
- ( (* we instanciate the hyp if possible *)
-(* tclTHENLIST *)
-(* [h_generalize [mkApp(mkVar hid,args)]; *)
-(* intro_erasing hid] *)
- fun g ->
- let prov_hid = pf_get_new_id hid g in
- tclTHENLIST[
- forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
- thin [hid];
- h_rename 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.
-
- We are not supposed to use it while proving this
- principle so that we can trash it
-
- *)
- (fun g ->
- observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid);
- thin [hid] g
- )
- )
- in
- (* if no args then no instanciation ! *)
- if args_id = []
- then
- tclTHENLIST [
- tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps;
- do_prove hyps
- ]
- else
- tclTHENLIST
- [
- tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps;
- tclMAP instanciate_one_hyp hyps;
- (fun g ->
- let all_g_hyps_id =
- List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty
- in
- let remaining_hyps =
- List.filter (fun id -> Idset.mem id all_g_hyps_id) hyps
- in
- do_prove remaining_hyps g
- )
- ]
-
-
-let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : tactic =
- fun goal ->
-(* observe (str "Proving principle for "++ str (string_of_int fun_num) ++ str "th function : " ++ *)
-(* pr_lconstr (mkConst fnames.(fun_num))); *)
- let princ_type = pf_concl goal in
- let princ_info = compute_elim_sig princ_type in
- let get_body const =
- match (Global.lookup_constant const ).const_body with
- | Some b ->
- let body = force b in
- Tacred.cbv_norm_flags
- (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
- (Global.env ())
- (Evd.empty)
- body
- | None -> error ( "Cannot define a principle over an axiom ")
- in
- let fbody = get_body fnames.(fun_num) in
- let params : identifier list ref = ref [] in
- let predicates : identifier list ref = ref [] in
- let args : identifier list ref = ref [] in
- let branches : identifier list ref = ref [] in
- let pte_to_fix = ref Idmap.empty in
- let fbody_with_params = ref None in
- let intro_with_remembrance ref number : tactic =
- tclTHEN
- ( tclDO number intro )
- (fun g ->
- let last_n = list_chop number (pf_hyps g) in
- ref := List.map (fun (id,_,_) -> id) (fst last_n)@ !ref;
- tclIDTAC g
- )
- in
- let rec partial_combine body params =
- match kind_of_term body,params with
- | Lambda (x,t,b),param::params ->
- partial_combine (subst1 param b) params
- | Fix(infos),_ ->
- body,params, Some (infos)
- | _ -> body,params,None
- in
- let build_pte_to_fix (offset:int) params predicates
- ((idxs,fix_num),(na,typearray,ca)) (avoid,_) =
-(* let true_params,_ = list_chop offset params in *)
- let true_params = List.rev params in
- let avoid = ref avoid in
- let res = list_fold_left_i
- (fun i acc pte_id ->
- let this_fix_id = fresh_id !avoid "fix___" in
- avoid := this_fix_id::!avoid;
-(* let this_body = substl (List.rev fnames_as_constr) ca.(i) in *)
- let new_type = prod_applist typearray.(i) true_params in
- let new_type_args,_ = decompose_prod new_type in
- let nargs = List.length new_type_args in
- let pte_args =
- (* let rev_args = List.rev_map (fun (id,_,_) -> mkVar id) new_type_args in *)
- let f = applist((* all_funs *)mkConst fnames.(i),true_params) in
- let app_f = mkApp(f,Array.init nargs (fun i -> mkRel(nargs - i))) in
- (Array.to_list (Array.init nargs (fun i -> mkRel(nargs - i))))@[app_f]
- in
- let app_pte = applist(mkVar pte_id,pte_args) in
- let new_type = compose_prod new_type_args app_pte in
- let fix_info =
- {
- idx = idxs.(i) - offset + 1;
- name = this_fix_id;
- types = new_type
- }
- in
- pte_to_fix := Idmap.add pte_id fix_info !pte_to_fix;
- fix_info::acc
- )
- 0
- []
- predicates
- in
- !avoid,List.rev res
- in
- let mk_fixes : tactic =
- fun g ->
- let body_p,params',fix_infos =
- partial_combine fbody (List.rev_map mkVar !params)
- in
- fbody_with_params := Some body_p;
- let offset = List.length params' in
- let not_real_param,true_params =
- list_chop
- ((List.length !params ) - offset)
- !params
- in
- params := true_params; args := not_real_param;
-(* observe (str "mk_fixes : params are "++ *)
-(* prlist_with_sep spc *)
-(* (fun id -> pr_lconstr (mkVar id)) *)
-(* !params *)
-(* ); *)
- let new_avoid,infos =
- option_fold_right
- (build_pte_to_fix
- offset
- (List.map mkVar !params)
- (List.rev !predicates)
- )
- fix_infos
- ((pf_ids_of_hyps g),[])
- in
- let pre_info,infos = list_chop fun_num infos in
- match pre_info,infos with
- | [],[] -> tclIDTAC g
- | _,this_fix_info::infos' ->
- let other_fix_info =
- List.map
- (fun fix_info -> fix_info.name,fix_info.idx,fix_info.types)
- (pre_info@infos')
- in
- tclORELSE
- (h_mutual_fix this_fix_info.name this_fix_info.idx other_fix_info)
- (tclFAIL 1000 (str "bad index" ++
- str (string_of_int this_fix_info.idx) ++
- str "offset := " ++
- (str (string_of_int offset))))
- g
- | _,[] -> anomaly "Not a valid information"
- in
- let do_prove ptes_to_fixes args branches : tactic =
- fun g ->
- let static_infos =
- {
- ptes_to_fixes = ptes_to_fixes;
- fixes_ids =
- Idmap.fold
- (fun _ fix_info acc -> fix_info.name::acc)
- ptes_to_fixes []
- }
- in
- match kind_of_term (pf_concl g) with
- | App(pte,pte_args) when isVar pte ->
- begin
- let pte = destVar pte in
- try
- if not (Idmap.mem pte ptes_to_fixes) then raise Not_Rec;
- let nparams = List.length !params in
- let args_as_constr = List.map mkVar args in
- let rec_num,new_body =
- let idx' = list_index pte (List.rev !predicates) - 1 in
- let f = fnames.(idx') in
- let body_with_params = match !fbody_with_params with Some f -> f | _ -> anomaly ""
- in
- let name_of_f = Name ( id_of_label (con_label f)) in
- let ((rec_nums,_),(na,_,bodies)) = destFix body_with_params in
- let idx'' = list_index name_of_f (Array.to_list na) - 1 in
- let body = substl (List.rev (Array.to_list all_funs)) bodies.(idx'') in
- let body = Reductionops.nf_beta (applist(body,(List.rev_map mkVar !params))) in
- rec_nums.(idx'') - nparams ,body
- in
- let applied_body =
- Reductionops.nf_beta
- (applist(new_body,List.rev args_as_constr))
- in
- let do_prove branches applied_body =
- do_prove_princ_for_struct
- interactive_proof
- (Array.to_list fnames)
- static_infos
- branches
- applied_body
- in
- let replace_and_prove =
- tclTHENS
- (fun g ->
-(* observe (str "replacing " ++ *)
-(* pr_lconstr_env (pf_env g) (array_last pte_args) ++ *)
-(* str " with " ++ *)
-(* pr_lconstr_env (pf_env g) applied_body ++ *)
-(* str " rec_arg_num is " ++ str (string_of_int rec_num) *)
-(* ); *)
- (Equality.replace (array_last pte_args) applied_body) g
- )
- [
- clean_goal_with_heq
- static_infos do_prove
- {
- nb_rec_hyps = List.length branches;
- rec_hyps = branches;
- info = applied_body;
- eq_hyps = [];
- } ;
- try
- let id = List.nth (List.rev args_as_constr) (rec_num) in
- (* observe (str "choosen var := "++ pr_lconstr id); *)
- (tclTHENSEQ
- [(h_simplest_case id);
- Tactics.intros_reflexivity
- ])
- with _ -> tclIDTAC
-
- ]
- in
- (observe_tac "doing replacement" ( replace_and_prove)) g
- with Not_Rec ->
- let fname = destConst (fst (decompose_app (array_last pte_args))) in
- tclTHEN
- (unfold_in_concl [([],Names.EvalConstRef fname)])
- (observe_tac ""
- (fun g' ->
- let body = array_last (snd (destApp (pf_concl g'))) in
- let dyn_infos =
- { nb_rec_hyps = List.length branches;
- rec_hyps = branches;
- info = body;
- eq_hyps = []
- }
- in
- let do_prove =
- do_prove_princ_for_struct
- interactive_proof
- (Array.to_list fnames)
- static_infos
- in
- clean_goal_with_heq static_infos
- do_prove dyn_infos g'
- )
- )
- g
- end
- | _ -> assert false
- in
- tclTHENSEQ
- [
- (fun g -> observe_tac "introducing params" (intro_with_remembrance params princ_info.nparams) g);
- (fun g -> observe_tac "introducing predicate" (intro_with_remembrance predicates princ_info.npredicates) g);
- (fun g -> observe_tac "introducing branches" (intro_with_remembrance branches princ_info.nbranches) g);
- (fun g -> observe_tac "declaring fix(es)" mk_fixes g);
- (fun g ->
- let nb_prod_g = nb_prod (pf_concl g) in
- tclTHENLIST [
- tclDO nb_prod_g intro;
- (fun g' ->
- let args =
- fst (list_chop ~msg:"args" nb_prod_g (pf_ids_of_hyps g'))
- in
- let do_prove_on_branches branches : tactic =
- observe_tac "proving" (do_prove !pte_to_fix args branches)
- in
- observe_tac "instanciating rec hyps"
- (instanciate_hyps_with_args do_prove_on_branches !branches (List.rev args))
- g'
- )
- ]
- g
- )
- ]
- goal
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-exception Toberemoved_with_rel of int*constr
-exception Toberemoved
-
-let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
- let princ_type_info = compute_elim_sig princ_type in
- let env = Global.env () in
-(* let type_sort = (Termops.new_sort_in_family InType) in *)
- let change_predicate_sort i (x,_,t) =
- let new_sort = sorts.(i) in
- let args,_ = decompose_prod t in
- let real_args =
- if princ_type_info.indarg_in_concl
- then List.tl args
- else args
- in
- x,None,compose_prod real_args (mkSort new_sort)
- in
- let new_predicates =
- list_map_i
- change_predicate_sort
- 0
- princ_type_info.predicates
- in
- let env_with_params_and_predicates =
- Environ.push_rel_context
- new_predicates
- (Environ.push_rel_context
- princ_type_info.params
- env
- )
- in
- let rel_as_kn =
- fst (match princ_type_info.indref with
- | Some (Libnames.IndRef ind) -> ind
- | _ -> failwith "Not a valid predicate"
- )
- in
- let pre_princ =
- it_mkProd_or_LetIn
- ~init:
- (it_mkProd_or_LetIn
- ~init:(option_fold_right
- mkProd_or_LetIn
- princ_type_info.indarg
- princ_type_info.concl
- )
- princ_type_info.args
- )
- princ_type_info.branches
- in
- let is_dom c =
- match kind_of_term c with
- | Ind((u,_)) -> u = rel_as_kn
- | Construct((u,_),_) -> u = rel_as_kn
- | _ -> false
- in
- let get_fun_num c =
- match kind_of_term c with
- | Ind(_,num) -> num
- | Construct((_,num),_) -> num
- | _ -> assert false
- in
- let dummy_var = mkVar (id_of_string "________") in
- let mk_replacement c i args =
- let res = mkApp(rel_to_fun.(i),Array.map pop (array_get_start args)) in
-(* observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); *)
- res
- in
- let rec has_dummy_var t =
- fold_constr
- (fun b t -> b || (eq_constr t dummy_var) || (has_dummy_var t))
- false
- t
- in
- let rec compute_new_princ_type remove env pre_princ : types*(constr list) =
- let (new_princ_type,_) as res =
- match kind_of_term pre_princ with
- | Rel n ->
- begin
- try match Environ.lookup_rel n env with
- | _,_,t when is_dom t -> raise Toberemoved
- | _ -> 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 is_pte =
- match kind_of_term f with
- | Rel n ->
- is_pte (Environ.lookup_rel n env)
- | _ -> false
- in
- let args =
- if is_pte && 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
- applist(new_f, new_args),
- list_union_eq eq_constr 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,[]
- in
-(* observennl ( *)
-(* match kind_of_term pre_princ with *)
-(* | Prod _ -> *)
-(* str "compute_new_princ_type for "++ *)
-(* pr_lconstr_env env pre_princ ++ *)
-(* str" is "++ *)
-(* pr_lconstr_env env new_princ_type ++ fnl () *)
-(* | _ -> str "" *)
-(* ); *)
- 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_x : name = get_name (ids_of_context env) x in
- let new_env = Environ.push_rel (x,None,t) env in
- let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
- if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
- then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
- else
- (
- bind_fun(new_x,new_t,new_b),
- list_union_eq
- eq_constr
- binders_to_remove_from_t
- (List.map pop binders_to_remove_from_b)
- )
-
- with
- | Toberemoved ->
-(* msgnl (str "Decl of "++Ppconstr.pr_name 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) ->
-(* msgnl (str "Decl of "++Ppconstr.pr_name 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 eq_constr (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_x : name = get_name (ids_of_context env) x in
- let new_env = Environ.push_rel (x,Some v,t) env in
- let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
- if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
- then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
- else
- (
- mkLetIn(new_x,new_v,new_t,new_b),
- list_union_eq
- eq_constr
- (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v)
- (List.map pop binders_to_remove_from_b)
- )
-
- with
- | Toberemoved ->
-(* msgnl (str "Decl of "++Ppconstr.pr_name 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) ->
-(* msgnl (str "Decl of "++Ppconstr.pr_name 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 eq_constr (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
- in
- new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc
- in
-(* observe (str "Computing new principe from " ++ pr_lconstr_env env_with_params_and_predicates pre_princ); *)
- let pre_res,_ =
- compute_new_princ_type princ_type_info.indarg_in_concl env_with_params_and_predicates pre_princ in
- it_mkProd_or_LetIn
- ~init:(it_mkProd_or_LetIn ~init:pre_res new_predicates)
- princ_type_info.params
-
-
-
-let change_property_sort toSort princ princName =
- let princ_info = compute_elim_sig princ in
- let change_sort_in_predicate (x,v,t) =
- (x,None,
- let args,_ = decompose_prod t in
- compose_prod args (mkSort toSort)
- )
- in
- let princName_as_constr = Tacinterp.constr_of_id (Global.env ()) princName in
- let init =
- let nargs = (princ_info.nparams + (List.length princ_info.predicates)) in
- mkApp(princName_as_constr,
- Array.init nargs
- (fun i -> mkRel (nargs - i )))
- in
- it_mkLambda_or_LetIn
- ~init:
- (it_mkLambda_or_LetIn ~init
- (List.map change_sort_in_predicate princ_info.predicates)
- )
- princ_info.params
-
-
-let pp_dur time time' =
- str (string_of_float (System.time_difference time time'))
-
-(* Things to be removed latter : just here to compare
- saving proof with and without normalizing the proof
-*)
-let new_save id const (locality,kind) hook =
- let {const_entry_body = pft;
- const_entry_type = tpo;
- const_entry_opaque = opacity } = const in
- let l,r = match locality with
- | Decl_kinds.Local when Lib.sections_are_opened () ->
- let k = Decl_kinds.logical_kind_of_goal_kind kind in
- let c = Declare.SectionLocalDef (pft, tpo, opacity) in
- let _ = Declare.declare_variable id (Lib.cwd(), c, k) in
- (Decl_kinds.Local, Libnames.VarRef id)
- | Decl_kinds.Local ->
- let k = Decl_kinds.logical_kind_of_goal_kind kind in
- let kn = Declare.declare_constant id (DefinitionEntry const, k) in
- (Decl_kinds.Global, Libnames.ConstRef kn)
- | Decl_kinds.Global ->
- let k = Decl_kinds.logical_kind_of_goal_kind kind in
- let kn = Declare.declare_constant id (DefinitionEntry const, k) in
- (Decl_kinds.Global, Libnames.ConstRef kn) in
- let time1 = System.get_time () in
- Pfedit.delete_current_proof ();
- let time2 = System.get_time () in
- hook l r;
- time1,time2
-(* definition_message id *)
-
-
-
-
-
-let new_save_named opacity =
-(* if do_observe () *)
-(* then *)
- let time1 = System.get_time () in
- let id,(const,persistence,hook) = Pfedit.cook_proof () in
- let time2 = System.get_time () in
- let const =
- { const with
- const_entry_body = (* nf_betaoiotazeta *)const.const_entry_body ;
- const_entry_opaque = opacity
- }
- in
- let time3 = System.get_time () in
- let time4,time5 = new_save id const persistence hook in
- let time6 = System.get_time () in
- Pp.msgnl
- (str "cooking proof time : " ++ pp_dur time1 time2 ++ fnl () ++
- str "reducing proof time : " ++ pp_dur time2 time3 ++ fnl () ++
- str "saving proof time : " ++ pp_dur time3 time4 ++fnl () ++
- str "deleting proof time : " ++ pp_dur time4 time5 ++fnl () ++
- str "hook time :" ++ pp_dur time5 time6
- )
-
-;;
-
-(* End of things to be removed latter : just here to compare
- saving proof with and without normalizing the proof
-*)
-
-
-let generate_functional_principle
- interactive_proof
- old_princ_type sorts new_princ_name funs i proof_tac
- =
- let f = funs.(i) in
- let type_sort = Termops.new_sort_in_family InType in
- let new_sorts =
- match sorts with
- | None -> Array.make (Array.length funs) (type_sort)
- | Some a -> a
- in
- (* First we get the type of the old graph principle *)
- let mutr_nparams = (compute_elim_sig old_princ_type).nparams in
- (* First we get the type of the old graph principle *)
- let new_principle_type =
- compute_new_princ_type_from_rel
- (Array.map mkConst funs)
- new_sorts
- old_princ_type
- in
-(* observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); *)
- let base_new_princ_name,new_princ_name =
- match new_princ_name with
- | Some (id) -> id,id
- | None ->
- let id_of_f = id_of_label (con_label f) in
- id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
- in
- let names = ref [new_princ_name] in
- let hook _ _ =
- if sorts = None
- then
-(* let id_of_f = id_of_label (con_label f) in *)
- let register_with_sort fam_sort =
- let s = Termops.new_sort_in_family fam_sort in
- let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
- let value =
- change_property_sort s new_principle_type new_princ_name
- in
-(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
- let ce =
- { const_entry_body = value;
- const_entry_type = None;
- const_entry_opaque = false;
- const_entry_boxed = Options.boxed_definitions()
- }
- in
- ignore(
- Declare.declare_constant
- name
- (Entries.DefinitionEntry ce,
- Decl_kinds.IsDefinition (Decl_kinds.Scheme)
- )
- );
- names := name :: !names
- in
- register_with_sort InProp;
- register_with_sort InSet
- in
- begin
- Command.start_proof
- new_princ_name
- (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
- new_principle_type
- hook
- ;
- try
- let _tim1 = System.get_time () in
- Pfedit.by (proof_tac (Array.map mkConst funs) mutr_nparams);
- 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; *)
- let do_save = not (do_observe ()) && not interactive_proof in
- let _ =
- try
- Options.silently Command.save_named true;
- let _dur2 = System.time_difference _tim2 (System.get_time ()) in
-(* Pp.msgnl (str ("Time to check proof: ") ++ str (string_of_float dur2)); *)
- Options.if_verbose
- (fun () ->
- Pp.msgnl (
- prlist_with_sep
- (fun () -> str" is defined " ++ fnl ())
- Ppconstr.pr_id
- (List.rev !names) ++ str" is defined "
- )
- )
- ()
- with e when do_save ->
- msg_warning
- (
- Cerrors.explain_exn e
- );
- if not (do_observe ())
- then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end
- in
- ()
-
-(* let tim3 = Sys.time () in *)
-(* Pp.msgnl (str ("Time to save proof: ") ++ str (string_of_float (tim3 -. tim2))); *)
-
- with
- | e ->
- msg_warning
- (
- Cerrors.explain_exn e
- );
- if not ( do_observe ())
- then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end
- end
-
-
-
-
-
-
-let get_funs_constant mp dp =
- let rec get_funs_constant const e : (Names.constant*int) array =
- match kind_of_term (snd (decompose_lam e)) with
- | Fix((_,(na,_,_))) ->
- Array.mapi
- (fun i na ->
- match na with
- | Name id ->
- let const = make_con mp dp (label_of_id id) in
- const,i
- | Anonymous ->
- anomaly "Anonymous fix"
- )
- na
- | _ -> [|const,0|]
- in
- function const ->
- let find_constant_body const =
- match (Global.lookup_constant const ).const_body with
- | Some b ->
- let body = force b in
- let body = Tacred.cbv_norm_flags
- (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
- (Global.env ())
- (Evd.empty)
- body
- in
- body
- | None -> error ( "Cannot define a principle over an axiom ")
- in
- let f = find_constant_body const in
- let l_const = get_funs_constant const f in
- (*
- We need to check that all the functions found are in the same block
- to prevent Reset stange thing
- *)
- let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in
- let l_params,l_fixes = List.split (List.map decompose_lam l_bodies) in
- (* all the paremeter must be equal*)
- let _check_params =
- let first_params = List.hd l_params in
- List.iter
- (fun params ->
- if not ((=) first_params params)
- then error "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 kind_of_term body with
- | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca)
- | _ ->
- if is_first && (List.length l_bodies = 1)
- then raise Not_Rec
- else error "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 not (first_infos = (extract_info false body))
- then error "Not a mutal recursive block"
- in
- List.iter check l_bodies
- with Not_Rec -> ()
- in
- l_const
-
-let make_scheme fas =
- let env = Global.env ()
- and sigma = Evd.empty in
- let id_to_constr id =
- Tacinterp.constr_of_id env id
- in
- let funs = List.map (fun (_,f,_) -> id_to_constr f) fas in
- let first_fun = destConst (List.hd funs) in
- let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in
- let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in
- let first_fun_kn =
- (* Fixme: take into accour funs_mp and funs_dp *)
- fst (destInd (id_to_constr first_fun_rel_id))
- in
- let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
- let this_block_funs = Array.map fst this_block_funs_indexes in
- let prop_sort = InProp in
- let funs_indexes =
- let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
- List.map
- (function const -> List.assoc (destConst const) this_block_funs_indexes)
- funs
- in
- let ind_list =
- List.map
- (fun (idx) ->
- let ind = first_fun_kn,idx in
- let (mib,mip) = Global.lookup_inductive ind in
- ind,mib,mip,true,prop_sort
- )
- funs_indexes
- in
- let l_schemes = List.map (Typing.type_of env sigma ) (Indrec.build_mutual_indrec env sigma ind_list) in
- let i = ref (-1) in
- let sorts =
- List.rev_map (fun (_,_,x) ->
- Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
- )
- fas
- in
- let princ_names = List.map (fun (x,_,_) -> x) fas in
- let _ = List.map2
- (fun princ_name scheme_type ->
- incr i;
-(* observe (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 *)
-(* ); *)
- generate_functional_principle
- false
- scheme_type
- (Some (Array.of_list sorts))
- (Some princ_name)
- this_block_funs
- !i
- (prove_princ_for_struct false !i (Array.of_list (List.map destConst funs)))
- )
- princ_names
- l_schemes
- in
- ()
-
-let make_case_scheme fa =
- let env = Global.env ()
- and sigma = Evd.empty in
- let id_to_constr id =
- Tacinterp.constr_of_id env id
- in
- let funs = (fun (_,f,_) -> id_to_constr f) fa in
- let first_fun = destConst funs in
- let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in
- let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in
- let first_fun_kn =
- (* Fixme: take into accour funs_mp and funs_dp *)
- fst (destInd (id_to_constr first_fun_rel_id))
- in
- let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
- let this_block_funs = Array.map fst this_block_funs_indexes in
- let prop_sort = InProp in
- let funs_indexes =
- let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
- List.assoc (destConst funs) this_block_funs_indexes
- in
- let ind_fun =
- let ind = first_fun_kn,funs_indexes in
- ind,prop_sort
- in
- let scheme_type = (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.make_case_gen env sigma ind sf) ind_fun) in
- let sorts =
- (fun (_,_,x) ->
- Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
- )
- fa
- in
- let princ_name = (fun (x,_,_) -> x) fa in
- let _ =
-(* observe (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 *)
-(* ); *)
- generate_functional_principle
- false
- scheme_type
- (Some ([|sorts|]))
- (Some princ_name)
- this_block_funs
- 0
- (prove_princ_for_struct false 0 [|destConst funs|])
- in
- ()
diff --git a/contrib/funind/new_arg_principle.mli b/contrib/funind/new_arg_principle.mli
deleted file mode 100644
index cad68da6..00000000
--- a/contrib/funind/new_arg_principle.mli
+++ /dev/null
@@ -1,34 +0,0 @@
-
-val generate_functional_principle :
- (* do we accept interactive proving *)
- bool ->
- (* induction principle on rel *)
- Term.types ->
- (* *)
- Term.sorts array option ->
- (* Name of the new principle *)
- (Names.identifier) option ->
- (* the compute functions to use *)
- Names.constant array ->
- (* We prove the nth- principle *)
- int ->
- (* The tactic to use to make the proof w.r
- the number of params
- *)
- (Term.constr array -> int -> Tacmach.tactic) ->
- unit
-
-
-
-(* val my_reflexivity : Tacmach.tactic *)
-
-val prove_princ_for_struct :
- bool ->
- int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic
-
-
-val compute_new_princ_type_from_rel : Term.constr array -> Term.sorts array ->
- Term.types -> Term.types
-
-val make_scheme : (Names.identifier*Names.identifier*Rawterm.rawsort) list -> unit
-val make_case_scheme : (Names.identifier*Names.identifier*Rawterm.rawsort) -> unit
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 327198b9..b6f26dfd 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -17,18 +17,11 @@ let observennl strm =
then Pp.msg strm
else ()
-(* type binder_type = *)
-(* | Lambda *)
-(* | Prod *)
-(* | LetIn *)
-
-(* type raw_context = (binder_type*name*rawconstr) list *)
type binder_type =
| Lambda of name
| Prod of name
| LetIn of name
-(* | LetTuple of name list * name *)
type raw_context = (binder_type*rawconstr) list
@@ -44,8 +37,6 @@ let compose_raw_context =
| Lambda n -> mkRLambda(n,t,acc)
| Prod n -> mkRProd(n,t,acc)
| LetIn n -> mkRLetIn(n,t,acc)
-(* | LetTuple (nal,na) -> *)
-(* RLetTuple(dummy_loc,nal,(na,None),t,acc) *)
in
List.fold_right compose_binder
@@ -145,37 +136,6 @@ let rec replace_var_by_term_in_binder x_id term = function
let add_bt_names bt = List.append (ids_of_binder bt)
-(* let rec replace_var_by_term_in_binder x_id term = function *)
-(* | [] -> [] *)
-(* | (bt,Name id,t)::l when id_ord id x_id = 0 -> *)
-(* (bt,Name id,replace_var_by_term x_id term t)::l *)
-(* | (bt,na,t)::l -> *)
-(* (bt,na,replace_var_by_term x_id term t)::(replace_var_by_term_in_binder x_id term l) *)
-
-(* let rec change_vars_in_binder mapping = function *)
-(* | [] -> [] *)
-(* | (bt,(Name id as na),t)::l when Idmap.mem id mapping -> *)
-(* (bt,na,change_vars mapping t):: l *)
-(* | (bt,na,t)::l -> *)
-(* (bt,na,change_vars mapping t):: *)
-(* (change_vars_in_binder mapping l) *)
-
-
-(* let alpha_ctxt avoid b = *)
-(* let rec alpha_ctxt = function *)
-(* | [] -> [],b *)
-(* | (bt,n,t)::ctxt -> *)
-(* let new_ctxt,new_b = alpha_ctxt ctxt in *)
-(* match n with *)
-(* | Name id when List.mem id avoid -> *)
-(* let new_id = Nameops.next_ident_away id avoid in *)
-(* let mapping = Idmap.add id new_id Idmap.empty in *)
-(* (bt,Name new_id,t):: *)
-(* (change_vars_in_binder mapping new_ctxt), *)
-(* change_vars mapping new_b *)
-(* | _ -> (bt,n,t)::new_ctxt,new_b *)
-(* in *)
-(* alpha_ctxt *)
let apply_args ctxt body args =
let need_convert_id avoid id =
List.exists (is_free_in id) args || List.mem id avoid
@@ -183,11 +143,6 @@ let apply_args ctxt body args =
let need_convert avoid bt =
List.exists (need_convert_id avoid) (ids_of_binder bt)
in
-(* let add_name na avoid = *)
-(* match na with *)
-(* | Anonymous -> avoid *)
-(* | Name id -> id::avoid *)
-(* in *)
let next_name_away (na:name) (mapping: identifier Idmap.t) (avoid: identifier list) =
match na with
| Name id when List.mem id avoid ->
@@ -206,17 +161,6 @@ let apply_args ctxt body args =
| Lambda na ->
let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid in
Lambda new_na,mapping,new_avoid
-(* | LetTuple (nal,na) -> *)
-(* let rev_new_nal,mapping,new_avoid = *)
-(* List.fold_left *)
-(* (fun (nal,mapping,(avoid:identifier list)) na -> *)
-(* let new_na,new_mapping,new_avoid = next_name_away na mapping avoid in *)
-(* (new_na::nal,new_mapping,new_avoid) *)
-(* ) *)
-(* ([],Idmap.empty,avoid) *)
-(* nal *)
-(* in *)
-(* (LetTuple(List.rev rev_new_nal,na),mapping,new_avoid) *)
in
let rec do_apply avoid ctxt body args =
match ctxt,args with
@@ -292,11 +236,6 @@ let combine_prod n t b =
let combine_letin n t b =
{ context = t.context@((LetIn n,t.value)::b.context); value = b.value}
-(* let combine_tuple nal na b in_e = *)
-(* { *)
-(* context = b.context@(LetTuple(nal,na),b.value)::in_e.context; *)
-(* value = in_e.value *)
-(* } *)
let mk_result ctxt value avoid =
{
@@ -402,6 +341,77 @@ let make_pattern_eq_precond id e pat =
res
+let build_constructors_of_type msg ind' argl =
+ let (mib,ind) = Inductive.lookup_mind_specif (Global.env()) ind' in
+ let npar = mib.Declarations.mind_nparams in
+ Array.mapi (fun i _ ->
+ let construct = ind',i+1 in
+ let constructref = ConstructRef(construct) in
+ let _implicit_positions_of_cst =
+ Impargs.implicits_of_global constructref
+ in
+ let cst_narg =
+ Inductiveops.mis_constructor_nargs_env
+ (Global.env ())
+ construct
+ in
+ let argl =
+ if argl = []
+ then
+ Array.to_list
+ (Array.init (cst_narg - npar) (fun _ -> mkRHole ())
+ )
+ else argl
+ in
+ let pat_as_term =
+ mkRApp(mkRRef (ConstructRef(ind',i+1)),argl)
+ in
+(* Pp.msgnl (str "new constructor := " ++ Printer.pr_rawconstr pat_as_term); *)
+ cases_pattern_of_rawconstr Anonymous pat_as_term
+ )
+ ind.Declarations.mind_consnames
+
+let find_constructors_of_raw_type msg t argl : Rawterm.cases_pattern array =
+ let ind,args = raw_decompose_app t in
+ match ind with
+ | RRef(_,IndRef ind') ->
+(* let _,ind = Global.lookup_inductive ind' in *)
+ build_constructors_of_type msg ind' argl
+ | _ -> error msg
+
+
+
+let rec find_type_of nb b =
+ let f,_ = raw_decompose_app b in
+ match f with
+ | RRef(_,ref) ->
+ begin
+ let ind_type =
+ match ref with
+ | VarRef _ | ConstRef _ ->
+ let constr_of_ref = constr_of_global ref in
+ let type_of_ref = Typing.type_of (Global.env ()) Evd.empty constr_of_ref in
+ let (_,ret_type) = Reduction.dest_prod (Global.env ()) type_of_ref in
+ let ret_type,_ = decompose_app ret_type in
+ if not (isInd ret_type) then
+ begin
+(* Pp.msgnl (str "not an inductive" ++ pr_lconstr ret_type); *)
+ raise (Invalid_argument "not an inductive")
+ end;
+ destInd ret_type
+ | IndRef ind -> ind
+ | ConstructRef c -> fst c
+ in
+ let _,ind_type_info = Inductive.lookup_mind_specif (Global.env()) ind_type in
+ if not (Array.length ind_type_info.Declarations.mind_consnames = nb )
+ then raise (Invalid_argument "find_type_of : not a valid inductive");
+ ind_type
+ end
+ | RCast(_,b,_,_) -> find_type_of nb b
+ | RApp _ -> assert false (* we have decomposed any application via raw_decompose_app *)
+ | _ -> raise (Invalid_argument "not a ref")
+
+
let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
(* Pp.msgnl (str " Entering : " ++ Printer.pr_rawconstr rt); *)
match rt with
@@ -466,14 +476,13 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
funnames
avoid
(mkRLetIn(new_n,t,mkRApp(new_b,args)))
- | RCases _ | RLambda _ ->
+ | RCases _ | RLambda _ | RIf _ | RLetTuple _ ->
let f_res = build_entry_lc funnames args_res.to_avoid f in
combine_results combine_app f_res args_res
| RDynamic _ ->error "Not handled RDynamic"
- | RCast _ -> error "Not handled RCast"
+ | RCast(_,b,_,_) ->
+ build_entry_lc funnames avoid (mkRApp(b,args))
| RRec _ -> error "Not handled RRec"
- | RIf _ -> error "Not handled RIf"
- | RLetTuple _ -> error "Not handled RLetTuple"
| RProd _ -> error "Cannot apply a type"
end
| RLambda(_,n,t,b) ->
@@ -496,16 +505,88 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
| RCases(_,_,el,brl) ->
let make_discr = make_discr_match brl in
build_entry_lc_from_case funnames make_discr el brl avoid
- | RIf _ -> error "Not handled RIf"
- | RLetTuple _ -> error "Not handled RLetTuple"
+ | RIf(_,b,(na,e_option),lhs,rhs) ->
+ begin
+ match b with
+ | RCast(_,b,_,t) ->
+ let msg = "If construction must be used with cast" in
+ let case_pat = find_constructors_of_raw_type msg t [] in
+ assert (Array.length case_pat = 2);
+ let brl =
+ list_map_i
+ (fun i x -> (dummy_loc,[],[case_pat.(i)],x))
+ 0
+ [lhs;rhs]
+ in
+ let match_expr =
+ mkRCases(None,[(b,(Anonymous,None))],brl)
+ in
+(* Pp.msgnl (str "new case := " ++ Printer.pr_rawconstr match_expr); *)
+ build_entry_lc funnames avoid match_expr
+ | _ ->
+ try
+ let ind = find_type_of 2 b in
+ let case_pat = build_constructors_of_type (str "") ind [] in
+ let brl =
+ list_map_i
+ (fun i x -> (dummy_loc,[],[case_pat.(i)],x))
+ 0
+ [lhs;rhs]
+ in
+ let match_expr =
+ mkRCases(None,[(b,(Anonymous,None))],brl)
+ in
+ (* Pp.msgnl (str "new case := " ++ Printer.pr_rawconstr match_expr); *)
+ build_entry_lc funnames avoid match_expr
+ with Invalid_argument s ->
+ let msg = "If construction must be used with cast : "^ s in
+ error msg
+
+ end
+ | RLetTuple(_,nal,_,b,e) ->
+ begin
+ let nal_as_rawconstr =
+ List.map
+ (function
+ Name id -> mkRVar id
+ | Anonymous -> mkRHole ()
+ )
+ nal
+ in
+ match b with
+ | RCast(_,b,_,t) ->
+ let case_pat =
+ find_constructors_of_raw_type
+ "LetTuple construction must be used with cast" t nal_as_rawconstr in
+ assert (Array.length case_pat = 1);
+ let br =
+ (dummy_loc,[],[case_pat.(0)],e)
+ in
+ let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in
+ build_entry_lc funnames avoid match_expr
+ | _ ->
+ try
+ let ind = find_type_of 1 b in
+ let case_pat =
+ build_constructors_of_type
+ (str "LetTuple construction must be used with cast") ind nal_as_rawconstr in
+ let br =
+ (dummy_loc,[],[case_pat.(0)],e)
+ in
+ let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in
+ build_entry_lc funnames avoid match_expr
+ with Invalid_argument s ->
+ let msg = "LetTuple construction must be used with cast : "^ s in
+ error msg
+
+ end
| RRec _ -> error "Not handled RRec"
- | RCast _ -> error "Not handled RCast"
+ | RCast(_,b,_,_) ->
+ build_entry_lc funnames avoid b
| RDynamic _ -> error "Not handled RDynamic"
and build_entry_lc_from_case funname make_discr
- (el:(Rawterm.rawconstr *
- (Names.name * (loc * Names.inductive * Names.name list) option) )
- list)
- (brl:(loc * identifier list * cases_pattern list * rawconstr) list) avoid :
+ (el:tomatch_tuple)
+ (brl:Rawterm.cases_clauses) avoid :
rawconstr build_entry_return =
match el with
| [] -> assert false (* matched on Nothing !*)
@@ -521,7 +602,7 @@ and build_entry_lc_from_case funname make_discr
in
let results =
List.map
- (build_entry_lc_from_case_term funname make_discr [] brl case_resl.to_avoid)
+ (build_entry_lc_from_case_term funname (make_discr (List.map fst el)) [] brl case_resl.to_avoid)
case_resl.result
in
{
@@ -567,7 +648,6 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo
avoid
matched_expr
in
-(* let ids = List.map (fun id -> Prod (Name id),mkRHole ()) idl in *)
let those_pattern_preconds =
( List.flatten
(
@@ -597,7 +677,7 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo
List.for_all (fun x -> x) unif) patterns_to_prevent
then
let i = List.length patterns_to_prevent in
- [(Prod Anonymous,make_discr (List.map pattern_to_term patl) i )]
+ [(Prod Anonymous,make_discr i )]
else
[]
)
@@ -839,6 +919,7 @@ let rec rebuild_return_type rt =
let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bool) list list) returned_types (rtl:rawconstr list) =
+ let _time1 = System.get_time () in
(* Pp.msgnl (prlist_with_sep fnl Printer.pr_rawconstr rtl); *)
let funnames_as_set = List.fold_right Idset.add funnames Idset.empty in
let funnames = Array.of_list funnames in
@@ -975,14 +1056,25 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo
Impargs.make_implicit_args false;
Impargs.make_strict_implicit_args false;
Impargs.make_contextual_implicit_args false;
+ let _time2 = System.get_time () in
+(* Pp.msgnl (str "Bulding Inductive : " ++ str (string_of_float (System.time_difference time1 time2))); *)
try
Options.silently (Command.build_mutual rel_inds) true;
+ let _time3 = System.get_time () in
+(* Pp.msgnl (str "Bulding Done: "++ str (string_of_float (System.time_difference time2 time3))); *)
+(* let msg = *)
+(* str "while trying to define"++ spc () ++ *)
+(* Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () *)
+(* in *)
+(* Pp.msgnl msg; *)
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;
Options.raw_print := old_rawprint;
with
- | UserError(s,msg) ->
+ | UserError(s,msg) ->
+ let _time3 = System.get_time () in
+(* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
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;
@@ -996,6 +1088,8 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo
raise
(UserError(s, msg))
| e ->
+ let _time3 = System.get_time () in
+(* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
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;
@@ -1010,3 +1104,4 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo
(UserError("",msg))
+
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index 99bf2bf1..c6406468 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -68,7 +68,10 @@ let rec raw_make_or_list = function
| e::l -> raw_make_or e (raw_make_or_list l)
-
+let remove_name_from_mapping mapping na =
+ match na with
+ | Anonymous -> mapping
+ | Name id -> Idmap.remove id mapping
let change_vars =
let rec change_vars mapping rt =
@@ -88,34 +91,31 @@ let change_vars =
change_vars mapping rt',
List.map (change_vars mapping) rtl
)
- | RLambda(_,Name id,_,_) when Idmap.mem id mapping -> rt
| RLambda(loc,name,t,b) ->
RLambda(loc,
name,
change_vars mapping t,
- change_vars mapping b
+ change_vars (remove_name_from_mapping mapping name) b
)
- | RProd(_,Name id,_,_) when Idmap.mem id mapping -> rt
| RProd(loc,name,t,b) ->
RProd(loc,
name,
change_vars mapping t,
- change_vars mapping b
+ change_vars (remove_name_from_mapping mapping name) b
)
- | RLetIn(_,Name id,_,_) when Idmap.mem id mapping -> rt
| RLetIn(loc,name,def,b) ->
RLetIn(loc,
name,
change_vars mapping def,
- change_vars mapping b
+ change_vars (remove_name_from_mapping mapping name) b
)
- | RLetTuple(_,nal,(na,_),_,_) when List.exists (function Name id -> Idmap.mem id mapping | _ -> false) (na::nal) -> rt
| RLetTuple(loc,nal,(na,rto),b,e) ->
+ let new_mapping = List.fold_left remove_name_from_mapping mapping nal in
RLetTuple(loc,
- nal,
- (na, option_app (change_vars mapping) rto),
- change_vars mapping b,
- change_vars mapping e
+ nal,
+ (na, option_map (change_vars mapping) rto),
+ change_vars mapping b,
+ change_vars new_mapping e
)
| RCases(loc,infos,el,brl) ->
RCases(loc,
@@ -123,8 +123,14 @@ let change_vars =
List.map (fun (e,x) -> (change_vars mapping e,x)) el,
List.map (change_vars_br mapping) brl
)
- | RIf _ -> error "Not handled RIf"
- | RRec _ -> error "Not handled RRec"
+ | RIf(loc,b,(na,e_option),lhs,rhs) ->
+ RIf(loc,
+ change_vars mapping b,
+ (na,option_map (change_vars mapping) e_option),
+ change_vars mapping lhs,
+ change_vars mapping rhs
+ )
+ | RRec _ -> error "Local (co)fixes are not supported"
| RSort _ -> rt
| RHole _ -> rt
| RCast(loc,b,k,t) ->
@@ -230,7 +236,7 @@ let rec alpha_rt excluded rt =
then t,b
else
let replace = change_vars (Idmap.add id new_id Idmap.empty) in
- (replace t,replace b)
+ (t,replace b)
in
let new_excluded = new_id::excluded in
let new_t = alpha_rt new_excluded t in
@@ -244,7 +250,7 @@ let rec alpha_rt excluded rt =
then t,b
else
let replace = change_vars (Idmap.add id new_id Idmap.empty) in
- (replace t,replace b)
+ (t,replace b)
in
let new_t = alpha_rt new_excluded t in
let new_b = alpha_rt new_excluded b in
@@ -256,7 +262,7 @@ let rec alpha_rt excluded rt =
then t,b
else
let replace = change_vars (Idmap.add id new_id Idmap.empty) in
- (replace t,replace b)
+ (t,replace b)
in
let new_excluded = new_id::excluded in
let new_t = alpha_rt new_excluded t in
@@ -286,18 +292,23 @@ let rec alpha_rt excluded rt =
if idmap_is_empty mapping
then rto,t,b
else let replace = change_vars mapping in
- (option_app replace rto,replace t,replace b)
+ (option_map replace rto, t,replace b)
in
let new_t = alpha_rt new_excluded new_t in
let new_b = alpha_rt new_excluded new_b in
- let new_rto = option_app (alpha_rt new_excluded) new_rto in
+ let new_rto = option_map (alpha_rt new_excluded) new_rto in
RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b)
| RCases(loc,infos,el,brl) ->
let new_el =
List.map (function (rt,i) -> alpha_rt excluded rt, i) el
in
RCases(loc,infos,new_el,List.map (alpha_br excluded) brl)
- | RIf _ -> error "Not handled RIf"
+ | RIf(loc,b,(na,e_o),lhs,rhs) ->
+ RIf(loc,alpha_rt excluded b,
+ (na,option_map (alpha_rt excluded) e_o),
+ alpha_rt excluded lhs,
+ alpha_rt excluded rhs
+ )
| RRec _ -> error "Not handled RRec"
| RSort _ -> rt
| RHole _ -> rt
@@ -439,7 +450,7 @@ let replace_var_by_term x_id term =
| RLetTuple(loc,nal,(na,rto),def,b) ->
RLetTuple(loc,
nal,
- (na,option_app replace_var_by_pattern rto),
+ (na,option_map replace_var_by_pattern rto),
replace_var_by_pattern def,
replace_var_by_pattern b
)
@@ -449,7 +460,12 @@ let replace_var_by_term x_id term =
List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el,
List.map replace_var_by_pattern_br brl
)
- | RIf _ -> raise (UserError("",str "Not handled RIf"))
+ | RIf(loc,b,(na,e_option),lhs,rhs) ->
+ RIf(loc, replace_var_by_pattern b,
+ (na,option_map replace_var_by_pattern e_option),
+ replace_var_by_pattern lhs,
+ replace_var_by_pattern rhs
+ )
| RRec _ -> raise (UserError("",str "Not handled RRec"))
| RSort _ -> rt
| RHole _ -> rt
diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli
index 92df0ec6..5dcdb15c 100644
--- a/contrib/funind/rawtermops.mli
+++ b/contrib/funind/rawtermops.mli
@@ -22,10 +22,7 @@ val mkRApp : rawconstr*(rawconstr list) -> rawconstr
val mkRLambda : Names.name*rawconstr*rawconstr -> rawconstr
val mkRProd : Names.name*rawconstr*rawconstr -> rawconstr
val mkRLetIn : Names.name*rawconstr*rawconstr -> rawconstr
-val mkRCases : rawconstr option *
- (rawconstr * (Names.name * (Util.loc * Names.inductive * Names.name list) option)) list *
- (Util.loc * Names.identifier list * cases_pattern list * rawconstr) list ->
- rawconstr
+val mkRCases : rawconstr option * tomatch_tuple * cases_clauses -> rawconstr
val mkRSort : rawsort -> rawconstr
val mkRHole : unit -> rawconstr (* we only build Evd.BinderType Anonymous holes *)
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index c2410d55..2c7e4d33 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -378,7 +378,7 @@ let rec proofPrinc mi: constr funind =
(* <pcase> Cases b of arrPt end.*)
| Case (cinfo, pcase, b, arrPt) ->
let prod_pcase,_ = decompose_lam pcase in
- let nmeb,_ = List.hd prod_pcase in
+ let _nmeb,_ = List.hd prod_pcase in
let newb'= apply_leqtrpl_t b mi.lst_eqs in
let type_of_b = Typing.type_of mi.env mi.sigma b in
(* Replace the recursive calls to the function by calls to the constant *)
@@ -428,7 +428,7 @@ let rec proofPrinc mi: constr funind =
let varnames = List.map snd mi.lst_vars in
let nb_vars = List.length varnames in
let nb_eqs = List.length mi.lst_eqs in
- let eqrels = List.map fst mi.lst_eqs in
+ let _eqrels = List.map fst mi.lst_eqs in
(* [terms_recs]: appel rec du fixpoint, On concatène les appels recs
trouvés dans les let in et les Cases avec ceux trouves dans u (ie
mi.mimick). *)
@@ -772,11 +772,6 @@ let invfun_verif c l dorew gl =
else error "wrong number of arguments for the function"
-TACTIC EXTEND functional_induction
- [ "functional" "induction" constr(c) ne_constr_list(l) ]
- -> [ invfun_verif c l true ]
-END
-
(* Construction of the functional scheme. *)
@@ -847,15 +842,20 @@ let declareFunScheme f fname mutflist =
+TACTIC EXTEND functional_induction
+ [ "old" "functional" "induction" constr(c) ne_constr_list(l) ]
+ -> [ invfun_verif c l true ]
+END
+
VERNAC COMMAND EXTEND FunctionalScheme
- [ "Functional" "Scheme" ident(na) ":=" "Induction" "for"
+ [ "Old" "Functional" "Scheme" ident(na) ":=" "Induction" "for"
ident(c) "with" ne_ident_list(l) ]
-> [ declareFunScheme c na l ]
-| [ "Functional" "Scheme" ident(na) ":=" "Induction" "for" ident (c) ]
+| [ "Old" "Functional" "Scheme" ident(na) ":=" "Induction" "for" ident (c) ]
-> [ declareFunScheme c na [] ]
END
-
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 01:01:25 +0000