summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/extraction/extraction.ml4
-rw-r--r--contrib/funind/functional_principles_proofs.ml188
-rw-r--r--contrib/funind/functional_principles_proofs.mli3
-rw-r--r--contrib/funind/functional_principles_types.ml531
-rw-r--r--contrib/funind/functional_principles_types.mli11
-rw-r--r--contrib/funind/indfun.ml218
-rw-r--r--contrib/funind/indfun_common.ml495
-rw-r--r--contrib/funind/indfun_common.mli64
-rw-r--r--contrib/funind/indfun_main.ml4302
-rw-r--r--contrib/funind/invfun.ml1068
-rw-r--r--contrib/funind/rawterm_to_relation.ml752
-rw-r--r--contrib/funind/rawterm_to_relation.mli22
-rw-r--r--contrib/funind/rawtermops.ml86
-rw-r--r--contrib/funind/rawtermops.mli10
-rw-r--r--contrib/funind/tacinv.ml413
-rw-r--r--contrib/interface/xlate.ml7
-rw-r--r--contrib/romega/ReflOmegaCore.v5
-rw-r--r--contrib/subtac/FixSub.v24
-rw-r--r--contrib/subtac/Utils.v10
-rw-r--r--contrib/subtac/eterm.ml56
-rw-r--r--contrib/subtac/subtac.ml6
-rw-r--r--contrib/subtac/subtac.mli11
-rw-r--r--contrib/subtac/subtac_coercion.ml18
-rw-r--r--contrib/subtac/subtac_command.ml271
-rw-r--r--contrib/subtac/subtac_command.mli1
-rw-r--r--contrib/subtac/subtac_interp_fixpoint.ml3
-rw-r--r--contrib/subtac/subtac_interp_fixpoint.mli11
-rw-r--r--contrib/subtac/subtac_utils.ml130
-rw-r--r--contrib/subtac/subtac_utils.mli15
-rw-r--r--contrib/subtac/test/ListsTest.v8
-rw-r--r--contrib/subtac/test/Mutind.v14
-rw-r--r--contrib/subtac/test/euclid.v4
-rw-r--r--contrib/subtac/test/measure.v24
-rw-r--r--contrib/subtac/test/wf.v48
-rw-r--r--contrib/xml/xmlcommand.ml2
35 files changed, 3225 insertions, 1210 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index e97df539..2b4b7967 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extraction.ml 8931 2006-06-09 07:43:37Z letouzey $ i*)
+(*i $Id: extraction.ml 9032 2006-07-07 16:30:34Z herbelin $ i*)
(*i*)
open Util
@@ -406,7 +406,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
List.iter
(option_iter
(fun kn -> if Cset.mem kn !projs then add_projection n kn))
- (lookup_structure ip).s_PROJ
+ (lookup_projections ip)
with Not_found -> ()
end;
Record field_glob
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index f0e986fb..7977d4e0 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -16,10 +16,7 @@ open Indfun_common
open Libnames
let msgnl = Pp.msgnl
-
-let do_observe () =
- Tacinterp.get_debug () <> Tactic_debug.DebugOff
-
+
let observe strm =
if do_observe ()
@@ -173,9 +170,11 @@ let isAppConstruct t =
then isConstruct (fst (destApp t))
else false
-
-let nf_betaiotazeta = Reductionops.local_strong Reductionops.whd_betaiotazeta
-
+let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
+ let clos_norm_flags flgs env sigma t =
+ Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
+ clos_norm_flags Closure.betaiotazeta Environ.empty_env Evd.empty
+
let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type =
let nochange msg =
@@ -231,12 +230,6 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t 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,
@@ -556,10 +549,17 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
g
+let my_orelse tac1 tac2 g =
+ try
+ tac1 g
+ with e ->
+(* observe (str "using snd tac since : " ++ Cerrors.explain_exn e); *)
+ tac2 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
+ my_orelse
( (* we instanciate the hyp if possible *)
fun g ->
let prov_hid = pf_get_new_id hid g in
@@ -748,10 +748,6 @@ let build_proof
(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 ->
@@ -812,7 +808,8 @@ type static_fix_info =
types : types;
offset : int;
nb_realargs : int;
- body_with_param : constr
+ body_with_param : constr;
+ num_in_block : int
}
@@ -838,11 +835,12 @@ let prove_rec_hyp fix_info =
exception Not_Rec
let generalize_non_dep hyp g =
+(* observe (str "rec id := " ++ Ppconstr.pr_id hyp); *)
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) ->
+ 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
@@ -853,7 +851,7 @@ let generalize_non_dep hyp 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 "h_generalize" (h_generalize (List.map mkVar to_revert) ))
(observe_tac "thin" (thin to_revert))
g
@@ -864,47 +862,97 @@ let revert idl =
(generalize (List.map mkVar idl))
(thin idl)
+let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
+(* observe (str "nb_args := " ++ str (string_of_int nb_args)); *)
+(* observe (str "nb_params := " ++ str (string_of_int nb_params)); *)
+(* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
+ let f_def = Global.lookup_constant (destConst f) in
+ let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
+ let f_body =
+ force (out_some f_def.const_body)
+ in
+ let params,f_body_with_params = decompose_lam_n nb_params f_body in
+ let (_,num),(_,_,bodies) = destFix f_body_with_params in
+ let fnames_with_params =
+ let params = Array.init nb_params (fun i -> mkRel(nb_params - i)) in
+ let fnames = List.rev (Array.to_list (Array.map (fun f -> mkApp(f,params)) fnames)) in
+ fnames
+ in
+(* observe (str "fnames_with_params " ++ prlist_with_sep fnl pr_lconstr fnames_with_params); *)
+(* observe (str "body " ++ pr_lconstr bodies.(num)); *)
+ let f_body_with_params_and_other_fun = substl fnames_with_params bodies.(num) in
+(* observe (str "f_body_with_params_and_other_fun " ++ pr_lconstr f_body_with_params_and_other_fun); *)
+ let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
+(* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *)
+ let type_ctxt,type_of_f = Sign.decompose_prod_n_assum (nb_params + nb_args) f_def.const_type in
+ let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
+ let lemma_type = it_mkProd_or_LetIn ~init:eqn type_ctxt in
+ let f_id = id_of_label (con_label (destConst f)) in
+ let prove_replacement =
+ tclTHENSEQ
+ [
+ tclDO (nb_params + rec_args_num + 1) intro;
+ observe_tac "" (fun g ->
+ let rec_id = pf_nth_hyp_id g 1 in
+ tclTHENSEQ
+ [observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id);
+ observe_tac "h_case" (h_case(mkVar rec_id,Rawterm.NoBindings));
+ intros_reflexivity] g
+ )
+ ]
+ in
+ Command.start_proof
+ (*i The next call to mk_equation_id is valid since we are constructing the lemma
+ Ensures by: obvious
+ i*)
+ (mk_equation_id f_id)
+ (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
+ lemma_type
+ (fun _ _ -> ());
+ Pfedit.by (prove_replacement);
+ Command.save_named false
+
+
-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
+
+let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
+ let equation_lemma =
+ try
+ let finfos = find_Function_infos (destConst f) in
+ mkConst (out_some finfos.equation_lemma)
+ with (Not_found | Failure "out_some" as e) ->
+ let f_id = id_of_label (con_label (destConst f)) in
+ (*i The next call to mk_equation_id is valid since we will construct the lemma
+ Ensures by: obvious
+ i*)
+ let equation_lemma_id = (mk_equation_id f_id) in
+ generate_equation_lemma all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
+ let _ =
+ match e with
+ | Failure "out_some" ->
+ let finfos = find_Function_infos (destConst f) in
+ update_Function
+ {finfos with
+ equation_lemma = Some (match Nametab.locate (make_short_qualid equation_lemma_id) with
+ ConstRef c -> c
+ | _ -> Util.anomaly "Not a constant"
+ )
+ }
+ | _ -> ()
+
+ in
+ Tacinterp.constr_of_id (pf_env g) equation_lemma_id
+ in
+ 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'
+ tclTHEN (Equality.rewriteLR equation_lemma) (revert just_introduced_id) g'
)
g
-
-
let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : tactic =
fun g ->
@@ -1011,7 +1059,8 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
nb_realargs =
List.length
(fst (decompose_lam bodies.(i))) - fix_offset;
- body_with_param = bodies_with_all_params.(i)
+ body_with_param = bodies_with_all_params.(i);
+ num_in_block = i
}
)
typess
@@ -1027,7 +1076,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
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_with_param,num =
let body = get_body fnames.(i) in
let body_with_full_params =
Reductionops.nf_betaiota (
@@ -1043,13 +1092,14 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
(Array.to_list all_funs_with_full_params))
bs.(num),
List.rev_map var_of_decl princ_params))
- )
+ ),num
| _ -> error "Not a mutual block"
in
let info =
{infos with
types = compose_prod type_args app_pte;
- body_with_param = body_with_param
+ body_with_param = body_with_param;
+ num_in_block = num
}
in
(* observe (str "binding " ++ Ppconstr.pr_id (Nameops.out_name pte) ++ *)
@@ -1118,8 +1168,17 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
tclTHENSEQ
[
observe_tac "do_replace"
- (do_replace princ_info.params fix_info.idx args_id
- (List.hd (List.rev pte_args)) fix_body);
+ (do_replace
+ full_params
+ (fix_info.idx + List.length princ_params)
+ (args_id@(List.map (fun (id,_,_) -> Nameops.out_name id ) princ_params))
+ (all_funs.(fix_info.num_in_block))
+ fix_info.num_in_block
+ all_funs
+ );
+(* 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
@@ -1133,13 +1192,16 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
nb_rec_hyps = List.length branches
}
in
- clean_goal_with_heq
+ observe_tac "cleaning" (clean_goal_with_heq
(Idmap.map prove_rec_hyp ptes_to_fix)
do_prove
- dyn_infos
+ dyn_infos)
in
-(* observe (str "branches := " ++ *)
-(* prlist_with_sep spc (fun decl -> Ppconstr.pr_id (id_of_decl decl)) princ_info.branches); *)
+(* observe (str "branches := " ++ *)
+(* prlist_with_sep spc (fun decl -> Ppconstr.pr_id (id_of_decl decl)) princ_info.branches ++ fnl () ++ *)
+(* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *)
+
+(* ); *)
observe_tac "instancing" (instanciate_hyps_with_args prove_tac
(List.rev_map id_of_decl princ_info.branches)
(List.rev args_id))
diff --git a/contrib/funind/functional_principles_proofs.mli b/contrib/funind/functional_principles_proofs.mli
index 35da5d50..62eb528e 100644
--- a/contrib/funind/functional_principles_proofs.mli
+++ b/contrib/funind/functional_principles_proofs.mli
@@ -16,5 +16,4 @@ val prove_principle_for_gen :
Tacmach.tactic
-val is_pte : rel_declaration -> bool
-val do_observe : unit -> bool
+(* val is_pte : rel_declaration -> bool *)
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index 8ef13264..f83eae8d 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -19,9 +19,41 @@ exception Toberemoved_with_rel of int*constr
exception Toberemoved
+let pr_elim_scheme el =
+ let env = Global.env () in
+ let msg = str "params := " ++ Printer.pr_rel_context env el.params in
+ let env = Environ.push_rel_context el.params env in
+ let msg = msg ++ fnl () ++ str "predicates := "++ Printer.pr_rel_context env el.predicates in
+ let env = Environ.push_rel_context el.predicates env in
+ let msg = msg ++ fnl () ++ str "branches := " ++ Printer.pr_rel_context env el.branches in
+ let env = Environ.push_rel_context el.branches env in
+ let msg = msg ++ fnl () ++ str "args := " ++ Printer.pr_rel_context env el.args in
+ let env = Environ.push_rel_context el.args env in
+ msg ++ fnl () ++ str "concl := " ++ pr_lconstr_env env el.concl
+
+let observe s =
+ if do_observe ()
+ then Pp.msgnl s
+let pr_elim_scheme el =
+ let env = Global.env () in
+ let msg = str "params := " ++ Printer.pr_rel_context env el.params in
+ let env = Environ.push_rel_context el.params env in
+ let msg = msg ++ fnl () ++ str "predicates := "++ Printer.pr_rel_context env el.predicates in
+ let env = Environ.push_rel_context el.predicates env in
+ let msg = msg ++ fnl () ++ str "branches := " ++ Printer.pr_rel_context env el.branches in
+ let env = Environ.push_rel_context el.branches env in
+ let msg = msg ++ fnl () ++ str "args := " ++ Printer.pr_rel_context env el.args in
+ let env = Environ.push_rel_context el.args env in
+ msg ++ fnl () ++ str "concl := " ++ pr_lconstr_env env el.concl
+
+
+let observe s =
+ if do_observe ()
+ then Pp.msgnl s
+
(*
Transform an inductive induction principle into
a functional one
@@ -29,6 +61,25 @@ 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 env_with_params = Environ.push_rel_context princ_type_info.params env in
+ let tbl = Hashtbl.create 792 in
+ let rec change_predicates_names (avoid:identifier list) (predicates:Sign.rel_context) : Sign.rel_context =
+ match predicates with
+ | [] -> []
+ |(Name x,v,t)::predicates ->
+ let id = Nameops.next_ident_away x avoid in
+ Hashtbl.add tbl id x;
+ (Name id,v,t)::(change_predicates_names (id::avoid) predicates)
+ | (Anonymous,_,_)::_ -> anomaly "Anonymous property binder "
+ in
+ let avoid = (Termops.ids_of_context env_with_params ) in
+ let princ_type_info =
+ { princ_type_info with
+ predicates = change_predicates_names avoid princ_type_info.predicates
+ }
+ in
+(* observe (str "starting princ_type := " ++ pr_lconstr_env env princ_type); *)
+(* observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *)
let change_predicate_sort i (x,_,t) =
let new_sort = sorts.(i) in
let args,_ = decompose_prod t in
@@ -37,7 +88,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
then List.tl args
else args
in
- x,None,compose_prod real_args (mkSort new_sort)
+ Nameops.out_name x,None,compose_prod real_args (mkSort new_sort)
in
let new_predicates =
list_map_i
@@ -45,20 +96,21 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
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 env_with_params_and_predicates = List.fold_right Environ.push_named new_predicates env_with_params in
let rel_as_kn =
fst (match princ_type_info.indref with
| Some (Libnames.IndRef ind) -> ind
- | _ -> failwith "Not a valid predicate"
+ | _ -> error "Not a valid predicate"
)
in
+ let ptes_vars = List.map (fun (id,_,_) -> id) new_predicates in
+ let is_pte =
+ let set = List.fold_right Idset.add ptes_vars Idset.empty in
+ fun t ->
+ match kind_of_term t with
+ | Var id -> Idset.mem id set
+ | _ -> false
+ in
let pre_princ =
it_mkProd_or_LetIn
~init:
@@ -72,6 +124,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
)
princ_type_info.branches
in
+ let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in
let is_dom c =
match kind_of_term c with
| Ind((u,_)) -> u = rel_as_kn
@@ -108,21 +161,15 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
| 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
+ 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
+ if is_pte f && remove
then array_get_start args
else args
in
@@ -138,15 +185,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
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 "++ *)
+(* let _ = match kind_of_term pre_princ with *)
+(* | Prod _ -> *)
+(* observe(str "compute_new_princ_type for "++ *)
(* pr_lconstr_env env pre_princ ++ *)
(* str" is "++ *)
-(* pr_lconstr_env env new_princ_type ++ fnl () *)
-(* | _ -> str "" *)
-(* ); *)
+(* pr_lconstr_env env new_princ_type ++ fnl ()) *)
+(* | _ -> () in *)
res
and compute_new_princ_type_for_binder remove bind_fun env x t b =
@@ -156,25 +201,25 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
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
+ 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 ->
+(* observe (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
+(* observe (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 =
@@ -184,7 +229,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
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
+ 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
@@ -198,24 +243,33 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
with
| Toberemoved ->
-(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* observe (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 "); *)
+(* observe (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
+ 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
+ compute_new_princ_type princ_type_info.indarg_in_concl env_with_params_and_predicates pre_princ
+ in
+ let pre_res =
+ replace_vars
+ (list_map_i (fun i id -> (id, mkRel i)) 1 ptes_vars)
+ (lift (List.length ptes_vars) pre_res)
+ in
it_mkProd_or_LetIn
- ~init:(it_mkProd_or_LetIn ~init:pre_res new_predicates)
+ ~init:(it_mkProd_or_LetIn
+ ~init:pre_res (List.map (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b)
+ new_predicates)
+ )
princ_type_info.params
@@ -246,128 +300,101 @@ let change_property_sort toSort princ princName =
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 qed () = 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
+
+
+
+
+
+let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook =
(* 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 =
+ (* let time1 = System.get_time () in *)
+ let new_principle_type =
compute_new_princ_type_from_rel
(Array.map mkConst funs)
- new_sorts
+ 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
+ (* let time2 = System.get_time () in *)
+ (* Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
+ (* observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); *)
+ let new_princ_name =
+ next_global_ident_away true (id_of_string "___________princ_________") []
in
begin
Command.start_proof
new_princ_name
(Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
new_principle_type
- hook
+ (hook new_principle_type)
;
- 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
+ (* 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; *)
+ get_proof_clean true
end
+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
+ 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 new_principle_type _ _ =
+ 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
+ let (id,(entry,g_kind,hook)) =
+ build_functional_principle interactive_proof old_princ_type new_sorts funs i proof_tac hook
+ in
+ save false new_princ_name entry g_kind hook
+(* defined () *)
+
exception Not_Rec
@@ -441,30 +468,20 @@ let get_funs_constant mp dp =
l_const
exception No_graph_found
-
-let make_scheme fas =
+exception Found_type of int
+
+let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_entry list =
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 funs = List.map fst fas in
+ let first_fun = List.hd funs in
+
+
+ let funs_mp,funs_dp,_ = Names.repr_con first_fun 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
+ fst (find_Function_infos first_fun).graph_ind
+ 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
@@ -472,7 +489,7 @@ let make_scheme fas =
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)
+ (function const -> List.assoc const this_block_funs_indexes)
funs
in
let ind_list =
@@ -484,49 +501,149 @@ let make_scheme fas =
)
funs_indexes
in
- let l_schemes = List.map (Typing.type_of env sigma ) (Indrec.build_mutual_indrec env sigma ind_list) 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) ->
+ 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
+ (* We create the first priciple by tactic *)
+ let first_type,other_princ_types =
+ match l_schemes with
+ s::l_schemes -> s,l_schemes
+ | _ -> anomaly ""
in
- ()
+ let (_,(const,_,_)) =
+ build_functional_principle false
+ first_type
+ (Array.of_list sorts)
+ this_block_funs
+ 0
+ (prove_princ_for_struct false 0 (Array.of_list funs))
+ (fun _ _ _ -> ())
+ in
+ incr i;
+ (* The others are just deduced *)
+ if other_princ_types = []
+ then
+ [const]
+ else
+ let other_fun_princ_types =
+ let funs = Array.map mkConst this_block_funs in
+ let sorts = Array.of_list sorts in
+ List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
+ in
+ let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in
+ let ctxt,fix = Sign.decompose_lam_assum first_princ_body in (* the principle has for forall ...., fix .*)
+ let (idxs,_),(_,ta,_ as decl) = destFix fix in
+ let other_result =
+ List.map (* we can now compute the other principles *)
+ (fun scheme_type ->
+ incr i;
+ observe (Printer.pr_lconstr scheme_type);
+ let type_concl = snd (Sign.decompose_prod_assum scheme_type) in
+ let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in
+ let f = fst (decompose_app applied_f) in
+ try (* we search the number of the function in the fix block (name of the function) *)
+ Array.iteri
+ (fun j t ->
+ let t = snd (Sign.decompose_prod_assum t) in
+ let applied_g = List.hd (List.rev (snd (decompose_app t))) in
+ let g = fst (decompose_app applied_g) in
+ if eq_constr f g
+ then raise (Found_type j);
+ observe (Printer.pr_lconstr f ++ str " <> " ++
+ Printer.pr_lconstr g)
+
+ )
+ ta;
+ (* If we reach this point, the two principle are not mutually recursive
+ We fall back to the previous method
+ *)
+ let (_,(const,_,_)) =
+ build_functional_principle
+ false
+ (List.nth other_princ_types (!i - 1))
+ (Array.of_list sorts)
+ this_block_funs
+ !i
+ (prove_princ_for_struct false !i (Array.of_list funs))
+ (fun _ _ _ -> ())
+ in
+ const
+ with Found_type i ->
+ let princ_body =
+ Termops.it_mkLambda_or_LetIn ~init:(mkFix((idxs,i),decl)) ctxt
+ in
+ {const with
+ Entries.const_entry_body = princ_body;
+ Entries.const_entry_type = Some scheme_type
+ }
+ )
+ other_fun_princ_types
+ in
+ const::other_result
+
+let build_scheme fas =
+(* (fun (f,_) -> *)
+(* try Libnames.constr_of_global (Nametab.global f) *)
+(* with Not_found -> *)
+(* Util.error ("Cannot find "^ Libnames.string_of_reference f) *)
+(* ) *)
+(* fas *)
-let make_case_scheme fa =
+ let bodies_types =
+ make_scheme
+ (List.map
+ (fun (_,f,sort) ->
+ let f_as_constant =
+ try
+ match Nametab.global f with
+ | Libnames.ConstRef c -> c
+ | _ -> Util.error "Functional Scheme can only be used with functions"
+ with Not_found ->
+ Util.error ("Cannot find "^ Libnames.string_of_reference f)
+ in
+ (f_as_constant,sort)
+ )
+ fas
+ )
+ in
+ List.iter2
+ (fun (princ_id,_,_) def_entry ->
+ ignore (Declare.declare_constant
+ princ_id
+ (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
+ Options.if_verbose (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id
+ )
+ fas
+ bodies_types
+
+
+
+let build_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 id_to_constr id = *)
+(* Tacinterp.constr_of_id env id *)
+(* in *)
+ let funs = (fun (_,f,_) ->
+ try Libnames.constr_of_global (Nametab.global f)
+ with Not_found ->
+ Util.error ("Cannot find "^ Libnames.string_of_reference 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 funs_mp,funs_dp,_ = Names.repr_con first_fun in
+ let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind 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
diff --git a/contrib/funind/functional_principles_types.mli b/contrib/funind/functional_principles_types.mli
index 8b4faaf4..cf28c6e6 100644
--- a/contrib/funind/functional_principles_types.mli
+++ b/contrib/funind/functional_principles_types.mli
@@ -1,5 +1,7 @@
open Names
open Term
+
+
val generate_functional_principle :
(* do we accept interactive proving *)
bool ->
@@ -19,13 +21,14 @@ val generate_functional_principle :
(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
+val make_scheme : (constant*Rawterm.rawsort) list -> Entries.definition_entry list
+
+val build_scheme : (identifier*Libnames.reference*Rawterm.rawsort) list -> unit
+val build_case_scheme : (identifier*Libnames.reference*Rawterm.rawsort) -> unit
+
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index f6d554a8..dffc8120 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -7,6 +7,124 @@ open Libnames
open Rawterm
open Declarations
+let is_rec_info scheme_info =
+ let test_branche min acc (_,_,br) =
+ acc || (
+ let new_branche =
+ Sign.it_mkProd_or_LetIn mkProp (fst (Sign.decompose_prod_assum br)) in
+ let free_rels_in_br = Termops.free_rels new_branche in
+ let max = min + scheme_info.Tactics.npredicates in
+ Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br
+ )
+ in
+ Util.list_fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
+
+
+let choose_dest_or_ind scheme_info =
+ if is_rec_info scheme_info
+ then Tactics.new_induct
+ else Tactics.new_destruct
+
+
+let functional_induction with_clean c princl pat =
+ let f,args = decompose_app c in
+ fun g ->
+ let princ,bindings, princ_type =
+ match princl with
+ | None -> (* No principle is given let's find the good one *)
+ begin
+ match kind_of_term f with
+ | Const c' ->
+ let princ_option =
+ let finfo = (* we first try to find out a graph on f *)
+ try find_Function_infos c'
+ with Not_found ->
+ errorlabstrm "" (str "Cannot find induction information on "++Printer.pr_lconstr (mkConst c') )
+ in
+ match Tacticals.elimination_sort_of_goal g with
+ | InProp -> finfo.prop_lemma
+ | InSet -> finfo.rec_lemma
+ | InType -> finfo.rect_lemma
+ in
+ let princ = (* then we get the principle *)
+ try mkConst (out_some princ_option )
+ with Failure "out_some" ->
+ (*i If there is not default lemma defined then, we cross our finger and try to
+ find a lemma named f_ind (or f_rec, f_rect) i*)
+ let princ_name =
+ Indrec.make_elimination_ident
+ (id_of_label (con_label c'))
+ (Tacticals.elimination_sort_of_goal g)
+ in
+ try
+ mkConst(const_of_id princ_name )
+ with Not_found -> (* This one is neither defined ! *)
+ errorlabstrm "" (str "Cannot find induction principle for "
+ ++Printer.pr_lconstr (mkConst c') )
+ in
+ (princ,Rawterm.NoBindings, Tacmach.pf_type_of g princ)
+ | _ -> raise (UserError("",str "functional induction must be used with a function" ))
+
+ end
+ | Some ((princ,binding)) ->
+ princ,binding,Tacmach.pf_type_of g princ
+ in
+ let princ_infos = Tactics.compute_elim_sig princ_type in
+ let args_as_induction_constr =
+ let c_list =
+ if princ_infos.Tactics.farg_in_concl
+ then [c] else []
+ in
+ List.map (fun c -> Tacexpr.ElimOnConstr c) (args@c_list)
+ in
+ 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 =
+ map_succeed
+ (fun id ->
+ if Idset.mem id old_idl then failwith "subst_and_reduce";
+ id
+ )
+ (Tacmach.pf_ids_of_hyps g)
+ in
+ let flag =
+ Rawterm.Cbv
+ {Rawterm.all_flags
+ with Rawterm.rDelta = false;
+ }
+ in
+ if with_clean
+ then
+ Tacticals.tclTHEN
+ (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst [id])) idl )
+ (Hiddentac.h_reduce flag Tacticals.allClauses)
+ g
+ else Tacticals.tclIDTAC g
+
+ in
+ Tacticals.tclTHEN
+ (choose_dest_or_ind
+ princ_infos
+ args_as_induction_constr
+ princ'
+ pat)
+ subst_and_reduce
+ g
+
+
+
+
type annot =
Struct of identifier
| Wf of Topconstr.constr_expr * identifier option
@@ -120,9 +238,22 @@ let prepare_body (name,annot,args,types,body) rt =
(fun_args,rt')
+let derive_inversion fix_names =
+ try
+ Invfun.derive_correctness
+ Functional_principles_types.make_scheme
+ functional_induction
+ (List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names)
+ (*i The next call to mk_rel_id is valid since we have just construct the graph
+ Ensures by : register_built
+ i*)
+ (List.map (fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id))) fix_names)
+ with e ->
+ msg_warning (str "Cannot define correction of function and graph" ++ Cerrors.explain_exn e)
+
let generate_principle
do_built fix_rec_l recdefs interactive_proof parametrize
- (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) =
+ (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) : unit =
let names = List.map (function (name,_,_,_,_) -> name) fix_rec_l in
let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
let funs_args = List.map fst fun_bodies in
@@ -133,6 +264,9 @@ let generate_principle
if do_built
then
begin
+ (*i The next call to mk_rel_id is valid since we have just construct the graph
+ Ensures by : do_built
+ i*)
let f_R_mut = Ident (dummy_loc,mk_rel_id (List.nth names 0)) in
let ind_kn =
fst (locate_with_msg
@@ -149,7 +283,7 @@ let generate_principle
in
let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in
let _ =
- Util.list_map_i
+ list_map_i
(fun i x ->
let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in
let princ_type =
@@ -167,6 +301,7 @@ let generate_principle
0
fix_rec_l
in
+ Array.iter add_Function funs_kn;
()
end
with e ->
@@ -210,7 +345,7 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
if List.length names = 1 then 1
else error "Recursive argument must be specified"
| Some wf_arg ->
- Util.list_index (Name wf_arg) names
+ list_index (Name wf_arg) names
in
let unbounded_eq =
let f_app_args =
@@ -236,7 +371,7 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
(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
+ derive_inversion [fname]
with e ->
(* No proof done *)
()
@@ -333,15 +468,15 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl =
(Topconstr.names_of_local_assums args)
in
let annot =
- try Some (Util.list_index (Name id) names - 1), Topconstr.CStructRec
+ try Some (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)
| (name,None,args,types,body),recdef ->
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,"Function",
+ user_err_loc
+ (dummy_loc,"Function",
Pp.str "the recursive argument needs to be specified in Function")
else
(name,(Some 0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation)
@@ -364,8 +499,8 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl =
interactive_proof
true
(Functional_principles_proofs.prove_princ_for_struct interactive_proof);
- true
-
+ if register_built then derive_inversion fix_names;
+ true;
in
()
@@ -397,19 +532,19 @@ let rec add_args id new_args b =
| 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,
+ CCases(loc,option_map (add_args id new_args) b_option,
+ List.map (fun (b,(na,b_option)) -> add_args id new_args b,(na,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),
+ CLetTuple(loc,nal,(na,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),
+ (na,option_map (add_args id new_args) b_option),
add_args id new_args b2,
add_args id new_args b3
)
@@ -426,15 +561,17 @@ let rec add_args id new_args b =
-let make_graph (id:identifier) =
- let c_body =
- try
- let c = const_of_id id in
- Global.lookup_constant c
- with Not_found ->
- raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id) )
- in
+let make_graph (f_ref:global_reference) =
+ let c,c_body =
+ match f_ref with
+ | ConstRef c ->
+ begin try c,Global.lookup_constant c
+ with Not_found ->
+ raise (UserError ("",str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) )
+ end
+ | _ -> raise (UserError ("", str "Not a function reference") )
+ in
match c_body.const_body with
| None -> error "Cannot build a graph over an axiom !"
| Some b ->
@@ -494,7 +631,7 @@ let make_graph (id:identifier) =
(fun n (nal,t'') ->
n+List.length nal) n nal_ta'
in
- assert (n'<= n);
+(* assert (n'<= n); *)
chop_n_arrow (n - n') t'
| _ -> anomaly "Not enough products"
else t
@@ -511,16 +648,6 @@ let make_graph (id:identifier) =
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
@@ -539,7 +666,8 @@ let make_graph (id:identifier) =
(List.map
(function
| Topconstr.LocalRawDef (na,_)-> []
- | Topconstr.LocalRawAssum (nal,_) -> List.map (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n))) nal
+ | Topconstr.LocalRawAssum (nal,_) ->
+ List.map (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n))) nal
)
nal_tas
)
@@ -551,23 +679,17 @@ let make_graph (id:identifier) =
in
l
| _ ->
+ let id = id_of_label (con_label c) in
[(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
+ do_generate_principle false false expr_list;
+ (* We register the infos *)
+ let mp,dp,_ = repr_con c in
+ List.iter (fun (id,_,_,_,_) -> add_Function (make_con mp dp (label_of_id id))) expr_list
+
+
(* let make_graph _ = assert false *)
let do_generate_principle = do_generate_principle true
+
+
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index b32dfacb..f41aac20 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -5,30 +5,15 @@ open Libnames
let mk_prefix pre id = id_of_string (pre^(string_of_id id))
let mk_rel_id = mk_prefix "R_"
+let mk_correct_id id = Nameops.add_suffix id "_correct"
+let mk_complete_id id = Nameops.add_suffix id "_complete"
+let mk_equation_id id = Nameops.add_suffix id "_equation"
let msgnl m =
()
let invalid_argument s = raise (Invalid_argument s)
-(* let idtbl = Hashtbl.create 29 *)
-(* let reset_name () = Hashtbl.clear idtbl *)
-
-(* let fresh_id s = *)
-(* try *)
-(* let id = Hashtbl.find idtbl s in *)
-(* incr id; *)
-(* id_of_string (s^(string_of_int !id)) *)
-(* with Not_found -> *)
-(* Hashtbl.add idtbl s (ref (-1)); *)
-(* id_of_string s *)
-
-(* let fresh_name s = Name (fresh_id s) *)
-(* let get_name ?(default="H") = function *)
-(* | Anonymous -> fresh_name default *)
-(* | Name n -> Name n *)
-
-
let fresh_id avoid s = Termops.next_global_ident_away true (id_of_string s) avoid
@@ -159,161 +144,323 @@ let find_reference sl s =
let eq = lazy(coq_constant "eq")
let refl_equal = lazy(coq_constant "refl_equal")
+(*****************************************************************)
+(* Copy of the standart save mechanism but without the much too *)
+(* slow reduction function *)
+(*****************************************************************)
+open Declarations
+open Entries
+open Decl_kinds
+open Declare
+let definition_message id =
+ Options.if_verbose message ((string_of_id id) ^ " is defined")
+
+
+let save with_clean 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
+ | Local when Lib.sections_are_opened () ->
+ let k = logical_kind_of_goal_kind kind in
+ let c = SectionLocalDef (pft, tpo, opacity) in
+ let _ = declare_variable id (Lib.cwd(), c, k) in
+ (Local, VarRef id)
+ | Local ->
+ let k = logical_kind_of_goal_kind kind in
+ let kn = declare_constant id (DefinitionEntry const, k) in
+ (Global, ConstRef kn)
+ | Global ->
+ let k = logical_kind_of_goal_kind kind in
+ let kn = declare_constant id (DefinitionEntry const, k) in
+ (Global, ConstRef kn) in
+ if with_clean then Pfedit.delete_current_proof ();
+ hook l r;
+ definition_message id
+
+
+
+
+let extract_pftreestate pts =
+ let pfterm,subgoals = Refiner.extract_open_pftreestate pts in
+ let tpfsigma = Refiner.evc_of_pftreestate pts in
+ let exl = Evarutil.non_instantiated tpfsigma in
+ if subgoals <> [] or exl <> [] then
+ Util.errorlabstrm "extract_proof"
+ (if subgoals <> [] then
+ str "Attempt to save an incomplete proof"
+ else
+ str "Attempt to save a proof with existential variables still non-instantiated");
+ let env = Global.env_of_context (Refiner.proof_of_pftreestate pts).Proof_type.goal.Evd.evar_hyps in
+ env,tpfsigma,pfterm
+
+
+let nf_betaiotazeta =
+ let clos_norm_flags flgs env sigma t =
+ Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
+ clos_norm_flags Closure.betaiotazeta
+
+let nf_betaiota =
+ let clos_norm_flags flgs env sigma t =
+ Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
+ clos_norm_flags Closure.betaiota
+
+let cook_proof do_reduce =
+ let pfs = Pfedit.get_pftreestate ()
+(* and ident = Pfedit.get_current_proof_name () *)
+ and (ident,strength,concl,hook) = Pfedit.current_proof_statement () in
+ let env,sigma,pfterm = extract_pftreestate pfs in
+ let pfterm =
+ if do_reduce
+ then nf_betaiota env sigma pfterm
+ else pfterm
+ in
+ (ident,
+ ({ const_entry_body = pfterm;
+ const_entry_type = Some concl;
+ const_entry_opaque = false;
+ const_entry_boxed = false},
+ strength, hook))
+
+
+let new_save_named opacity =
+ let id,(const,persistence,hook) = cook_proof true in
+ let const = { const with const_entry_opaque = opacity } in
+ save true id const persistence hook
+
+let get_proof_clean do_reduce =
+ let result = cook_proof do_reduce in
+ Pfedit.delete_current_proof ();
+ result
+
+
+
+
+(**********************)
+
+type function_info =
+ {
+ function_constant : constant;
+ graph_ind : inductive;
+ equation_lemma : constant option;
+ correctness_lemma : constant option;
+ completeness_lemma : constant option;
+ rect_lemma : constant option;
+ rec_lemma : constant option;
+ prop_lemma : constant option;
+ }
+
+
+type function_db = function_info list
+
+let function_table = ref ([] : function_db)
+
-(* (\************************************************\) *)
-(* (\* Should be removed latter *\) *)
-(* (\* Comes from new induction (cf Pierre) *\) *)
-(* (\************************************************\) *)
-
-(* open Sign *)
-(* open Term *)
-
-(* type elim_scheme = *)
-
-(* (\* { (\\* lists are in reverse order! *\\) *\) *)
-(* (\* params: rel_context; (\\* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *\\) *\) *)
-(* (\* predicates: rel_context; (\\* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *\\) *\) *)
-(* (\* branches: rel_context; (\\* branchr,...,branch1 *\\) *\) *)
-(* (\* args: rel_context; (\\* (xni, Ti_ni) ... (x1, Ti_1) *\\) *\) *)
-(* (\* indarg: rel_declaration option; (\\* Some (H,I prm1..prmp x1...xni) if present, None otherwise *\\) *\) *)
-(* (\* concl: types; (\\* Qi x1...xni HI, some prmis may not be present *\\) *\) *)
-(* (\* indarg_in_concl:bool; (\\* true if HI appears at the end of conclusion (dependent scheme) *\\) *\) *)
-(* (\* } *\) *)
-
-
-
-(* let occur_rel n c = *)
-(* let res = not (noccurn n c) in *)
-(* res *)
-
-(* let list_filter_firsts f l = *)
-(* let rec list_filter_firsts_aux f acc l = *)
-(* match l with *)
-(* | e::l' when f e -> list_filter_firsts_aux f (acc@[e]) l' *)
-(* | _ -> acc,l *)
-(* in *)
-(* list_filter_firsts_aux f [] l *)
-
-(* let count_rels_from n c = *)
-(* let rels = Termops.free_rels c in *)
-(* let cpt,rg = ref 0, ref n in *)
-(* while Util.Intset.mem !rg rels do *)
-(* cpt:= !cpt+1; rg:= !rg+1; *)
-(* done; *)
-(* !cpt *)
-
-(* let count_nonfree_rels_from n c = *)
-(* let rels = Termops.free_rels c in *)
-(* if Util.Intset.exists (fun x -> x >= n) rels then *)
-(* let cpt,rg = ref 0, ref n in *)
-(* while not (Util.Intset.mem !rg rels) do *)
-(* cpt:= !cpt+1; rg:= !rg+1; *)
-(* done; *)
-(* !cpt *)
-(* else raise Not_found *)
-
-(* (\* cuts a list in two parts, first of size n. Size must be greater than n *\) *)
-(* let cut_list n l = *)
-(* let rec cut_list_aux acc n l = *)
-(* if n<=0 then acc,l *)
-(* else match l with *)
-(* | [] -> assert false *)
-(* | e::l' -> cut_list_aux (acc@[e]) (n-1) l' in *)
-(* let res = cut_list_aux [] n l in *)
-(* res *)
-
-(* let exchange_hd_prod subst_hd t = *)
-(* let hd,args= decompose_app t in mkApp (subst_hd,Array.of_list args) *)
-
-(* let compute_elim_sig elimt = *)
-(* (\* conclusion is the final (Qi ...) *\) *)
-(* let hyps,conclusion = decompose_prod_assum elimt in *)
-(* (\* ccl is conclusion where Qi (that is rel <something>) is replaced *)
-(* by a constant (Prop) to avoid it being counted as an arg or *)
-(* parameter in the following. *\) *)
-(* let ccl = exchange_hd_prod mkProp conclusion in *)
-(* (\* indarg is the inductive argument if it exists. If it exists it is *)
-(* the last hyp before the conclusion, so it is the first element of *)
-(* hyps. To know the first elmt is an inductive arg, we check if the *)
-(* it appears in the conclusion (as rel 1). If yes, then it is not *)
-(* an inductive arg, otherwise it is. There is a pathological case *)
-(* with False_inf where Qi is rel 1, so we first get rid of Qi in *)
-(* ccl. *\) *)
-(* (\* if last arg of ccl is an application then this a functional ind *)
-(* principle *\) let last_arg_ccl = *)
-(* try List.hd (List.rev (snd (decompose_app ccl))) *)
-(* with Failure "hd" -> mkProp in (\* dummy constr that is not an app *)
-(* *\) let hyps',indarg,dep = *)
-(* if isApp last_arg_ccl *)
-(* then *)
-(* hyps,None , false (\* no HI at all *\) *)
-(* else *)
-(* try *)
-(* if noccurn 1 ccl (\* rel 1 does not occur in ccl *\) *)
-(* then *)
-(* List.tl hyps , Some (List.hd hyps), false (\* it does not *)
-(* occur in concl *\) else *)
-(* List.tl hyps , Some (List.hd hyps) , true (\* it does occur in concl *\) *)
-(* with Failure s -> Util.error "cannot recognise an induction schema" *)
-(* in *)
-
-(* (\* Arguments [xni...x1] must appear in the conclusion, so we count *)
-(* successive rels appearing in conclusion **Qi is not considered a *)
-(* rel** *\) let nargs = count_rels_from *)
-(* (match indarg with *)
-(* | None -> 1 *)
-(* | Some _ -> 2) ccl in *)
-(* let args,hyps'' = cut_list nargs hyps' in *)
-(* let rel_is_pred (_,_,c) = isSort (snd(decompose_prod_assum c)) in *)
-(* let branches,hyps''' = *)
-(* list_filter_firsts (function x -> not (rel_is_pred x)) hyps'' *)
-(* in *)
-(* (\* Now we want to know which hyps remaining are predicates and which *)
-(* are parameters *\) *)
-(* (\* We rebuild *)
-
-(* forall (x1:Ti_1) (xni:Ti_ni) (HI:I prm1..prmp x1...xni), DUMMY *)
-(* x1...xni HI ^^^^^^^^^^^^^^^^^^^^^^^^^ ^^ *)
-(* optional *)
-(* opt *)
-
-(* Free rels appearing in this term are parameters. We catch all of *)
-(* them if HI is present. In this case the number of parameters is *)
-(* the number of free rels. Otherwise (principle generated by *)
-(* functional induction or by hand) WE GUESS that all parameters *)
-(* appear in Ti_js, IS THAT TRUE??. *)
-
-(* TODO: if we want to generalize to the case where arges are merged *)
-(* with branches (?) and/or where several predicates are cited in *)
-(* the conclusion, we should do something more precise than just *)
-(* counting free rels. *)
-(* *\) *)
-(* let concl_with_indarg = *)
-(* match indarg with *)
-(* | None -> ccl *)
-(* | Some c -> it_mkProd_or_LetIn ccl [c] in *)
-(* let concl_with_args = it_mkProd_or_LetIn concl_with_indarg args in *)
-(* (\* let nparams2 = Util.Intset.cardinal (Termops.free_rels concl_with_args) in *\) *)
-(* let nparams = *)
-(* try List.length (hyps'''@branches) - count_nonfree_rels_from 1 *)
-(* concl_with_args with Not_found -> 0 in *)
-(* let preds,params = cut_list (List.length hyps''' - nparams) hyps''' in *)
-(* let elimscheme = { *)
-(* params = params; *)
-(* predicates = preds; *)
-(* branches = branches; *)
-(* args = args; *)
-(* indarg = indarg; *)
-(* concl = conclusion; *)
-(* indarg_in_concl = dep; *)
-(* } *)
-(* in *)
-(* elimscheme *)
-
-(* let get_params elimt = *)
-(* (compute_elim_sig elimt).params *)
-(* (\************************************************\) *)
-(* (\* end of Should be removed latter *\) *)
-(* (\* Comes from new induction (cf Pierre) *\) *)
-(* (\************************************************\) *)
+let rec do_cache_info finfo = function
+ | [] -> raise Not_found
+ | (finfo'::finfos as l) ->
+ if finfo' == finfo then l
+ else if finfo'.function_constant = finfo.function_constant
+ then finfo::finfos
+ else
+ let res = do_cache_info finfo finfos in
+ if res == finfos then l else finfo'::l
+
+let cache_Function (_,(finfos)) =
+ let new_tbl =
+ try do_cache_info finfos !function_table
+ with Not_found -> finfos::!function_table
+ in
+ if new_tbl != !function_table
+ then function_table := new_tbl
+
+let load_Function _ = cache_Function
+let open_Function _ = cache_Function
+let subst_Function (_,subst,finfos) =
+ let do_subst_con c = fst (Mod_subst.subst_con subst c)
+ and do_subst_ind (kn,i) = (Mod_subst.subst_kn subst kn,i)
+ in
+ let function_constant' = do_subst_con finfos.function_constant in
+ let graph_ind' = do_subst_ind finfos.graph_ind in
+ let equation_lemma' = Util.option_smartmap do_subst_con finfos.equation_lemma in
+ let correctness_lemma' = Util.option_smartmap do_subst_con finfos.correctness_lemma in
+ let completeness_lemma' = Util.option_smartmap do_subst_con finfos.completeness_lemma in
+ let rect_lemma' = Util.option_smartmap do_subst_con finfos.rect_lemma in
+ let rec_lemma' = Util.option_smartmap do_subst_con finfos.rec_lemma in
+ let prop_lemma' = Util.option_smartmap do_subst_con finfos.prop_lemma in
+ if function_constant' == finfos.function_constant &&
+ graph_ind' == finfos.graph_ind &&
+ equation_lemma' == finfos.equation_lemma &&
+ correctness_lemma' == finfos.correctness_lemma &&
+ completeness_lemma' == finfos.completeness_lemma &&
+ rect_lemma' == finfos.rect_lemma &&
+ rec_lemma' == finfos.rec_lemma &&
+ prop_lemma' == finfos.prop_lemma
+ then finfos
+ else
+ { function_constant = function_constant';
+ graph_ind = graph_ind';
+ equation_lemma = equation_lemma' ;
+ correctness_lemma = correctness_lemma' ;
+ completeness_lemma = completeness_lemma' ;
+ rect_lemma = rect_lemma' ;
+ rec_lemma = rec_lemma';
+ prop_lemma = prop_lemma';
+ }
+
+let classify_Function (_,infos) = Libobject.Substitute infos
+
+let export_Function infos = Some infos
+
+
+let discharge_Function (_,finfos) =
+ let function_constant' = Lib.discharge_con finfos.function_constant
+ and graph_ind' = Lib.discharge_inductive finfos.graph_ind
+ and equation_lemma' = Util.option_smartmap Lib.discharge_con finfos.equation_lemma
+ and correctness_lemma' = Util.option_smartmap Lib.discharge_con finfos.correctness_lemma
+ and completeness_lemma' = Util.option_smartmap Lib.discharge_con finfos.completeness_lemma
+ and rect_lemma' = Util.option_smartmap Lib.discharge_con finfos.rect_lemma
+ and rec_lemma' = Util.option_smartmap Lib.discharge_con finfos.rec_lemma
+ and prop_lemma' = Util.option_smartmap Lib.discharge_con finfos.prop_lemma
+ in
+ if function_constant' == finfos.function_constant &&
+ graph_ind' == finfos.graph_ind &&
+ equation_lemma' == finfos.equation_lemma &&
+ correctness_lemma' == finfos.correctness_lemma &&
+ completeness_lemma' == finfos.completeness_lemma &&
+ rect_lemma' == finfos.rect_lemma &&
+ rec_lemma' == finfos.rec_lemma &&
+ prop_lemma' == finfos.prop_lemma
+ then Some finfos
+ else
+ Some { function_constant = function_constant' ;
+ graph_ind = graph_ind' ;
+ equation_lemma = equation_lemma' ;
+ correctness_lemma = correctness_lemma' ;
+ completeness_lemma = completeness_lemma';
+ rect_lemma = rect_lemma';
+ rec_lemma = rec_lemma';
+ prop_lemma = prop_lemma' ;
+ }
+
+open Term
+let pr_info f_info =
+ str "function_constant := " ++ Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
+ str "function_constant_type := " ++
+ (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) with _ -> mt ()) ++ fnl () ++
+ str "equation_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++
+ str "completeness_lemma :=" ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++
+ str "correctness_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++
+ str "rect_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++
+ str "rec_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++
+ str "prop_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++
+ str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl ()
+
+let pr_table l =
+ Util.prlist_with_sep fnl pr_info l
+
+let in_Function,out_Function =
+ Libobject.declare_object
+ {(Libobject.default_object "FUNCTIONS_DB") with
+ Libobject.cache_function = cache_Function;
+ Libobject.load_function = load_Function;
+ Libobject.classify_function = classify_Function;
+ Libobject.subst_function = subst_Function;
+ Libobject.export_function = export_Function;
+ Libobject.discharge_function = discharge_Function
+(* Libobject.open_function = open_Function; *)
+ }
+
+
+
+(* Synchronisation with reset *)
+let freeze () =
+ let tbl = !function_table in
+(* Pp.msgnl (str "freezing function_table : " ++ pr_table tbl); *)
+ tbl
+
+let unfreeze l =
+(* Pp.msgnl (str "unfreezing function_table : " ++ pr_table l); *)
+ function_table :=
+ l
+let init () =
+(* Pp.msgnl (str "reseting function_table"); *)
+ function_table := []
+
+let _ =
+ Summary.declare_summary "functions_db_sum"
+ { Summary.freeze_function = freeze;
+ Summary.unfreeze_function = unfreeze;
+ Summary.init_function = init;
+ Summary.survive_module = false;
+ Summary.survive_section = false }
+
+let find_or_none id =
+ try Some
+ (match Nametab.locate (make_short_qualid id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant"
+ )
+ with Not_found -> None
+
+
+
+let find_Function_infos f =
+ List.find (fun finfo -> finfo.function_constant = f) !function_table
+
+
+let find_Function_of_graph ind =
+ List.find (fun finfo -> finfo.graph_ind = ind) !function_table
+
+let update_Function finfo =
+(* Pp.msgnl (pr_info finfo); *)
+ Lib.add_anonymous_leaf (in_Function finfo)
+
+
+let add_Function f =
+ let f_id = id_of_label (con_label f) in
+ let equation_lemma = find_or_none (mk_equation_id f_id)
+ and correctness_lemma = find_or_none (mk_correct_id f_id)
+ and completeness_lemma = find_or_none (mk_complete_id f_id)
+ and rect_lemma = find_or_none (Nameops.add_suffix f_id "_rect")
+ and rec_lemma = find_or_none (Nameops.add_suffix f_id "_rec")
+ and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
+ and graph_ind =
+ match Nametab.locate (make_short_qualid (mk_rel_id f_id))
+ with | IndRef ind -> ind | _ -> Util.anomaly "Not an inductive"
+ in
+ let finfos =
+ { function_constant = f;
+ equation_lemma = equation_lemma;
+ completeness_lemma = completeness_lemma;
+ correctness_lemma = correctness_lemma;
+ rect_lemma = rect_lemma;
+ rec_lemma = rec_lemma;
+ prop_lemma = prop_lemma;
+ graph_ind = graph_ind
+ }
+ in
+ update_Function finfos
+
+let pr_table () = pr_table !function_table
+(*********************************)
+(* Debuging *)
+let function_debug = ref false
+open Goptions
+
+let function_debug_sig =
+ {
+ optsync = false;
+ optname = "Function debug";
+ optkey = PrimaryTable("Function_debug");
+ optread = (fun () -> !function_debug);
+ optwrite = (fun b -> function_debug := b)
+ }
+
+let _ = declare_bool_option function_debug_sig
+
+
+let do_observe () =
+ !function_debug = true
+
+
+
diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli
index ab5195b0..00e1ce8d 100644
--- a/contrib/funind/indfun_common.mli
+++ b/contrib/funind/indfun_common.mli
@@ -1,7 +1,15 @@
open Names
open Pp
+(*
+ The mk_?_id function build different name w.r.t. a function
+ Each of their use is justified in the code
+*)
val mk_rel_id : identifier -> identifier
+val mk_correct_id : identifier -> identifier
+val mk_complete_id : identifier -> identifier
+val mk_equation_id : identifier -> identifier
+
val msgnl : std_ppcmds -> unit
@@ -39,3 +47,59 @@ val refl_equal : Term.constr Lazy.t
val const_of_id: identifier -> constant
+(* [save_named] is a copy of [Command.save_named] but uses
+ [nf_betaiotazeta] instead of [nf_betaiotaevar_preserving_vm_cast]
+
+
+
+ DON'T USE IT if you cannot ensure that there is no VMcast in the proof
+
+*)
+
+(* val nf_betaiotazeta : Reductionops.reduction_function *)
+
+val new_save_named : bool -> unit
+
+val save : bool -> identifier -> Entries.definition_entry -> Decl_kinds.goal_kind ->
+ Tacexpr.declaration_hook -> unit
+
+(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
+ abort the proof
+*)
+val get_proof_clean : bool ->
+ Names.identifier *
+ (Entries.definition_entry * Decl_kinds.goal_kind *
+ Tacexpr.declaration_hook)
+
+
+
+
+(*****************)
+
+type function_info =
+ {
+ function_constant : constant;
+ graph_ind : inductive;
+ equation_lemma : constant option;
+ correctness_lemma : constant option;
+ completeness_lemma : constant option;
+ rect_lemma : constant option;
+ rec_lemma : constant option;
+ prop_lemma : constant option;
+ }
+
+val find_Function_infos : constant -> function_info
+val find_Function_of_graph : inductive -> function_info
+(* WARNING: To be used just after the graph definition !!! *)
+val add_Function : constant -> unit
+
+val update_Function : function_info -> unit
+
+
+(** debugging *)
+val pr_info : function_info -> Pp.std_ppcmds
+val pr_table : unit -> Pp.std_ppcmds
+
+
+val function_debug : bool ref
+val do_observe : unit -> bool
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index 61f26d30..00b5f28c 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -14,6 +14,7 @@ open Indfun_common
open Indfun
open Genarg
open Pcoq
+open Tacticals
let pr_binding prc = function
| loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c)
@@ -36,7 +37,8 @@ let pr_with_bindings prc prlc (c,bl) =
let pr_fun_ind_using prc prlc _ opt_c =
match opt_c with
| None -> mt ()
- | Some c -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc c)
+ | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc (p,b))
+
ARGUMENT EXTEND fun_ind_using
TYPED AS constr_with_bindings_opt
@@ -47,25 +49,9 @@ END
TACTIC EXTEND newfuninv
- [ "functional" "inversion" ident(hyp) ident(fname) fun_ind_using(princl)] ->
+ [ "functional" "inversion" quantified_hypothesis(hyp) reference_opt(fname) ] ->
[
- 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
+ Invfun.invfun hyp fname
]
END
@@ -82,26 +68,11 @@ ARGUMENT EXTEND with_names TYPED AS intro_pattern_opt PRINTED BY pr_intro_as_pat
END
-let is_rec scheme_info =
- let test_branche min acc (_,_,br) =
- acc ||
- (let new_branche = Sign.it_mkProd_or_LetIn mkProp (fst (Sign.decompose_prod_assum br)) in
- let free_rels_in_br = Termops.free_rels new_branche in
- let max = min + scheme_info.Tactics.npredicates in
- Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br)
- in
- Util.list_fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
-
-
-let choose_dest_or_ind scheme_info =
- if is_rec scheme_info
- then Tactics.new_induct
- else Tactics.new_destruct
TACTIC EXTEND newfunind
["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
- [
+ [
let pat =
match pat with
| None -> IntroAnonymous
@@ -112,77 +83,23 @@ TACTIC EXTEND newfunind
| [c] -> c
| c::cl -> applist(c,cl)
in
- let f,args = decompose_app c in
- fun g ->
- let princ,bindings =
- match princl with
- | None -> (* No principle is given let's find the good one *)
- let fname =
- match kind_of_term f with
- | Const c' ->
- id_of_label (con_label c')
- | _ -> Util.error "Must be used with a function"
- in
- let princ_name =
- (
- Indrec.make_elimination_ident
- fname
- (Tacticals.elimination_sort_of_goal g)
- )
- in
- mkConst(const_of_id princ_name ),Rawterm.NoBindings
- | Some princ -> princ
- in
- let princ_type = Tacmach.pf_type_of g princ in
- let princ_infos = Tactics.compute_elim_sig princ_type in
- let args_as_induction_constr =
- let c_list =
- if princ_infos.Tactics.farg_in_concl
- then [c] else []
- in
- List.map (fun c -> Tacexpr.ElimOnConstr c) (args@c_list)
- in
- 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)
- subst_and_reduce
- g
- ]
+ functional_induction true c princl pat ]
+END
+(***** debug only ***)
+TACTIC EXTEND snewfunind
+ ["soft" "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
+ functional_induction false c princl pat ]
END
@@ -213,7 +130,10 @@ VERNAC ARGUMENT EXTEND rec_definition2
in
let check_exists_args an =
try
- 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
+ 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,"Function",
@@ -240,12 +160,15 @@ END
VERNAC COMMAND EXTEND Function
["Function" rec_definitions2(recsl)] ->
- [ do_generate_principle false recsl]
+ [
+ do_generate_principle false recsl;
+
+ ]
END
VERNAC ARGUMENT EXTEND fun_scheme_arg
-| [ ident(princ_name) ":=" "Induction" "for" ident(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ]
+| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ]
END
VERNAC ARGUMENT EXTEND fun_scheme_args
@@ -257,29 +180,176 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
["Functional" "Scheme" fun_scheme_args(fas) ] ->
[
try
- Functional_principles_types.make_scheme fas
+ Functional_principles_types.build_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
+ make_graph (Nametab.global fun_name);
+ try Functional_principles_types.build_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
-
+(***** debug only ***)
VERNAC COMMAND EXTEND NewFunctionalCase
["Functional" "Case" fun_scheme_arg(fas) ] ->
[
- Functional_principles_types.make_case_scheme fas
+ Functional_principles_types.build_case_scheme fas
]
END
-
+(***** debug only ***)
VERNAC COMMAND EXTEND GenerateGraph
-["Generate" "graph" "for" ident(c)] -> [ make_graph c ]
+["Generate" "graph" "for" reference(c)] -> [ make_graph (Nametab.global c) ]
+END
+
+
+
+
+
+(* FINDUCTION *)
+
+(* comment this line to see debug msgs *)
+(* let msg x = () ;; let pr_lconstr c = str "" *)
+ (* uncomment this to see debugging *)
+let prconstr c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n")
+let prlistconstr lc = List.iter prconstr lc
+let prstr s = msg(str s)
+
+
+
+(** Information about an occurrence of a function call (application)
+ inside a term. *)
+type fapp_info = {
+ fname: constr; (** The function applied *)
+ largs: constr list; (** List of arguments *)
+ free: bool; (** [true] if all arguments are debruijn free *)
+ max_rel: int; (** max debruijn index in the funcall *)
+ onlyvars: bool (** [true] if all arguments are variables (and not debruijn) *)
+}
+
+
+(** [constr_head_match(a b c) a] returns true, false otherwise. *)
+let constr_head_match u t=
+ if isApp u
+ then
+ let uhd,args= destApp u in
+ uhd=t
+ else false
+
+(** [hdMatchSub inu t] returns the list of occurrences of [t] in
+ [inu]. DeBruijn are not pushed, so some of them may be unbound in
+ the result. *)
+let rec hdMatchSub inu (test: constr -> bool) : fapp_info list =
+ let subres =
+ match kind_of_term inu with
+ | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) ->
+ hdMatchSub tp test @ hdMatchSub (lift 1 cstr) test
+ | Fix (_,(lna,tl,bl)) -> (* not sure Fix is correct *)
+ Array.fold_left
+ (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) test)
+ [] bl
+ | _ -> (* Cofix will be wrong *)
+ fold_constr
+ (fun l cstr ->
+ l @ hdMatchSub cstr test) [] inu in
+ if not (test inu) then subres
+ else
+ let f,args = decompose_app inu in
+ let freeset = Termops.free_rels inu in
+ let max_rel = try Util.Intset.max_elt freeset with Not_found -> -1 in
+ {fname = f; largs = args; free = Util.Intset.is_empty freeset;
+ max_rel = max_rel; onlyvars = List.for_all isVar args }
+ ::subres
+
+
+(** [find_fapp test g] returns the list of [app_info] of all calls to
+ functions that satisfy [test] in the conclusion of goal g. Trivial
+ repetition (not modulo conversion) are deleted. *)
+let find_fapp (test:constr -> bool) g : fapp_info list =
+ let pre_res = hdMatchSub (Tacmach.pf_concl g) test in
+ let res =
+ List.fold_right (fun x acc -> if List.mem x acc then acc else x::acc) pre_res [] in
+ (prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res);
+ res)
+
+
+
+(** [finduction id filter g] tries to apply functional induction on
+ an occurence of function [id] in the conclusion of goal [g]. If
+ [id]=[None] then calls to any function are selected. In any case
+ [heuristic] is used to select the most pertinent occurrence. *)
+let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info list)
+ (nexttac:Proof_type.tactic) g =
+ let test = match oid with
+ | Some id ->
+ let idconstr = mkConst (const_of_id id) in
+ (fun u -> constr_head_match u idconstr) (* select only id *)
+ | None -> (fun u -> isApp u) in (* select calls to any function *)
+ let info_list = find_fapp test g in
+ let ordered_info_list = heuristic info_list in
+ prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list);
+ if List.length ordered_info_list = 0 then Util.error "function not found in goal\n";
+ let taclist: Proof_type.tactic list =
+ List.map
+ (fun info ->
+ (tclTHEN
+ (functional_induction true (applist (info.fname, info.largs))
+ None IntroAnonymous)
+ nexttac)) ordered_info_list in
+ tclFIRST taclist g
+
+
+
+
+(** [chose_heuristic oi x] returns the heuristic for reordering
+ (and/or forgetting some elts of) a list of occurrences of
+ function calls infos to chose first with functional induction. *)
+let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list =
+ match oi with
+ | Some i -> (fun l -> [ List.nth l (i-1) ]) (* occurrence was given by the user *)
+ | None ->
+ (* Default heuristic: keep only occurrence where all arguments
+ are *bound* (meaning already introduced) variables *)
+ (* TODO: put other funcalls at the end instead of deleting them *)
+ let ordering x y =
+ if x.free && x.onlyvars && y.free && y.onlyvars then 0 (* both pertinent *)
+ else if x.free && x.onlyvars then -1
+ else if y.free && y.onlyvars then 1
+ else 0 (* both not pertinent *)
+ in
+ List.sort ordering
+
+
+TACTIC EXTEND finduction
+ ["finduction" ident(id) natural_opt(oi)] ->
+ [
+ match oi with
+ | Some(n) when n<=0 -> Util.error "numerical argument must be > 0"
+ | _ ->
+ let heuristic = chose_heuristic oi in
+ finduction (Some id) heuristic tclIDTAC
+ ]
+END
+
+
+
+TACTIC EXTEND fauto
+ [ "fauto" tactic(tac)] ->
+ [
+ let heuristic = chose_heuristic None in
+ finduction None heuristic (snd tac)
+ ]
+ |
+ [ "fauto" ] ->
+ [
+ let heuristic = chose_heuristic None in
+ finduction None heuristic tclIDTAC
+ ]
+
END
+
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 2e5616f0..084ec7e0 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -1,7 +1,15 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+open Tacexpr
+open Declarations
open Util
open Names
open Term
-open Tacinvutils
open Pp
open Libnames
open Tacticals
@@ -9,131 +17,963 @@ open Tactics
open Indfun_common
open Tacmach
open Sign
+open Hiddentac
+(* Some pretty printing function for debugging purpose *)
-let tac_pattern l =
- (Hiddentac.h_reduce
- (Rawterm.Pattern l)
- Tacticals.onConcl
- )
+let pr_binding prc =
+ function
+ | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
+ | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.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 rec nb_prod x =
- let rec count n c =
- match kind_of_term c with
- Prod(_,_,t) -> count (n+1) t
- | LetIn(_,a,_,t) -> count n (subst1 a t)
- | Cast(c,_,_) -> count n c
- | _ -> n
- in count 0 x
-let intro_discr_until n tac : tactic =
- let rec intro_discr_until acc : tactic =
- fun g ->
- if nb_prod (pf_concl g) <= n then tac (List.rev acc) g
- else
- tclTHEN
- intro
- (fun g' ->
- let id,_,t = pf_last_hyp g' in
- tclORELSE
- (tclABSTRACT None (Extratactics.h_discrHyp (Rawterm.NamedHyp id)))
- (intro_discr_until ((id,t)::acc))
- g'
- )
- g
+let pr_with_bindings prc prlc (c,bl) =
+ prc c ++ hv 0 (pr_bindings prc prlc bl)
+
+
+
+let pr_constr_with_binding prc (c,bl) : Pp.std_ppcmds =
+ pr_with_bindings prc prc (c,bl)
+
+let pr_elim_scheme el =
+ let env = Global.env () in
+ let msg = str "params := " ++ Printer.pr_rel_context env el.params in
+ let env = Environ.push_rel_context el.params env in
+ let msg = msg ++ fnl () ++ str "predicates := "++ Printer.pr_rel_context env el.predicates in
+ let env = Environ.push_rel_context el.predicates env in
+ let msg = msg ++ fnl () ++ str "branches := " ++ Printer.pr_rel_context env el.branches in
+ let env = Environ.push_rel_context el.branches env in
+ let msg = msg ++ fnl () ++ str "args := " ++ Printer.pr_rel_context env el.args in
+ let env = Environ.push_rel_context el.args env in
+ let msg =
+ Util.option_fold_right
+ (fun o msg -> msg ++ fnl () ++ str "indarg := " ++ Printer.pr_rel_context env [o])
+ el.indarg
+ msg
+ in
+ let env = Util.option_fold_right (fun o env -> Environ.push_rel_context [o] env) el.indarg env in
+ msg ++ fnl () ++ str "concl := " ++ Printer.pr_lconstr_env env el.concl
+
+(* The local debuging mechanism *)
+let msgnl = Pp.msgnl
+
+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 goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in
+ let v = tac g in msgnl (goal ++ fnl () ++ 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
+
+(* [nf_zeta] $\zeta$-normalization of a term *)
+let nf_zeta =
+ Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+ Environ.empty_env
+ Evd.empty
+
+
+(* [id_to_constr id] finds the term associated to [id] in the global environment *)
+let id_to_constr id =
+ try
+ Tacinterp.constr_of_id (Global.env ()) id
+ with Not_found ->
+ raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id))
+
+(* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true]
+ (resp. g_to_f = false) where [graph] is the graph of [f] and is the [i]th function in the block.
+
+ [generate_type true f i] returns
+ \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res,
+ graph\ x_1\ldots x_n\ res \rightarrow res = fv \] decomposed as the context and the conclusion
+
+ [generate_type false f i] returns
+ \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res,
+ res = fv \rightarrow graph\ x_1\ldots x_n\ res\] decomposed as the context and the conclusion
+ *)
+
+let generate_type g_to_f f graph i =
+ (*i we deduce the number of arguments of the function and its returned type from the graph i*)
+ let graph_arity = Inductive.type_of_inductive (Global.lookup_inductive (destInd graph)) in
+ let ctxt,_ = decompose_prod_assum graph_arity in
+ let fun_ctxt,res_type =
+ match ctxt with
+ | [] | [_] -> anomaly "Not a valid context"
+ | (_,_,res_type)::fun_ctxt -> fun_ctxt,res_type
in
- intro_discr_until []
-
-
-let rec discr_rew_in_H hypname idl : tactic =
- match idl with
- | [] -> (Extratactics.h_discrHyp (Rawterm.NamedHyp hypname))
- | ((id,t)::idl') ->
- match kind_of_term t with
- | App(eq',[| _ ; arg1 ; _ |]) when eq_constr eq' (Lazy.force eq) ->
- begin
- let constr,_ = decompose_app arg1 in
- if isConstruct constr
- then
- (discr_rew_in_H hypname idl')
- else
- tclTHEN
- (tclTRY (Equality.general_rewrite_in true hypname (mkVar id)))
- (discr_rew_in_H hypname idl')
- end
- | _ -> discr_rew_in_H hypname idl'
-
-let finalize fname hypname idl : tactic =
- tclTRY (
- (tclTHEN
- (Hiddentac.h_reduce
- (Rawterm.Unfold [[],EvalConstRef fname])
- (Tacticals.onHyp hypname)
- )
- (discr_rew_in_H hypname idl)
- ))
+ let nb_args = List.length fun_ctxt in
+ let args_from_decl i decl =
+ match decl with
+ | (_,Some _,_) -> incr i; failwith "args_from_decl"
+ | _ -> let j = !i in incr i;mkRel (nb_args - j + 1)
+ in
+ (*i We need to name the vars [res] and [fv] i*)
+ let res_id =
+ Termops.next_global_ident_away
+ true
+ (id_of_string "res")
+ (map_succeed (function (Name id,_,_) -> id | (Anonymous,_,_) -> failwith "") fun_ctxt)
+ in
+ let fv_id =
+ Termops.next_global_ident_away
+ true
+ (id_of_string "fv")
+ (res_id::(map_succeed (function (Name id,_,_) -> id | (Anonymous,_,_) -> failwith "Anonymous!") fun_ctxt))
+ in
+ (*i we can then type the argument to be applied to the function [f] i*)
+ let args_as_rels =
+ let i = ref 0 in
+ Array.of_list ((map_succeed (args_from_decl i) (List.rev fun_ctxt)))
+ in
+ let args_as_rels = Array.map Termops.pop args_as_rels in
+ (*i
+ the hypothesis [res = fv] can then be computed
+ We will need to lift it by one in order to use it as a conclusion
+ i*)
+ let res_eq_f_of_args =
+ mkApp(Coqlib.build_coq_eq (),[|lift 2 res_type;mkRel 1;mkRel 2|])
+ in
+ (*i
+ The hypothesis [graph\ x_1\ldots x_n\ res] can then be computed
+ We will need to lift it by one in order to use it as a conclusion
+ i*)
+ let graph_applied =
+ let args_and_res_as_rels =
+ let i = ref 0 in
+ Array.of_list ((map_succeed (args_from_decl i) (List.rev ((Name res_id,None,res_type)::fun_ctxt))) )
+ in
+ let args_and_res_as_rels =
+ Array.mapi (fun i c -> if i <> Array.length args_and_res_as_rels - 1 then lift 1 c else c) args_and_res_as_rels
+ in
+ mkApp(graph,args_and_res_as_rels)
+ in
+ (*i The [pre_context] is the defined to be the context corresponding to
+ \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res, \]
+ i*)
+ let pre_ctxt =
+ (Name res_id,None,lift 1 res_type)::(Name fv_id,Some (mkApp(mkConst f,args_as_rels)),res_type)::fun_ctxt
+ in
+ (*i and we can return the solution depending on which lemma type we are defining i*)
+ if g_to_f
+ then (Anonymous,None,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args)
+ else (Anonymous,None,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied)
-let gen_fargs fargs : tactic =
- fun g ->
- generalize
- (List.map
- (fun arg ->
- let targ = pf_type_of g arg in
- let refl_arg = mkApp (Lazy.force refl_equal , [|targ ; arg|]) in
- refl_arg
- )
- (Array.to_list fargs)
- )
- g
-
-let invfun (hypname:identifier) fname princ : tactic=
- fun g ->
- let nprod_goal = nb_prod (pf_concl g) in
- let princ_info =
- let princ_type =
- (try (match (Global.lookup_constant princ) with
- {Declarations.const_type=t} -> t
- )
- with _ -> assert false)
+(*
+ [find_induction_principle f] searches and returns the [body] and the [type] of [f_rect]
+
+ WARNING: while convertible, [type_of body] and [type] can be non equal
+*)
+let find_induction_principle f =
+ let f_as_constant = match kind_of_term f with
+ | Const c' -> c'
+ | _ -> error "Must be used with a function"
+ in
+ let infos = find_Function_infos f_as_constant in
+ match infos.rect_lemma with
+ | None -> raise Not_found
+ | Some rect_lemma ->
+ let rect_lemma = mkConst rect_lemma in
+ let typ = Typing.type_of (Global.env ()) Evd.empty rect_lemma in
+ rect_lemma,typ
+
+
+
+(* let fname = *)
+(* match kind_of_term f with *)
+(* | Const c' -> *)
+(* id_of_label (con_label c') *)
+(* | _ -> error "Must be used with a function" *)
+(* in *)
+
+(* let princ_name = *)
+(* ( *)
+(* Indrec.make_elimination_ident *)
+(* fname *)
+(* InType *)
+(* ) *)
+(* in *)
+(* let c = (\* mkConst(mk_from_const (destConst f) princ_name ) in *\) failwith "" in *)
+(* c,Typing.type_of (Global.env ()) Evd.empty c *)
+
+
+let rec generate_fresh_id x avoid i =
+ if i == 0
+ then []
+ else
+ let id = Termops.next_global_ident_away true x avoid in
+ id::(generate_fresh_id x (id::avoid) (pred i))
+
+
+(* [prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i ]
+ is the tactic used to prove correctness lemma.
+
+ [functional_induction] is the tactic defined in [indfun] (dependency problem)
+ [funs_constr], [graphs_constr] [schemes] [lemmas_types_infos] are the mutually recursive functions
+ (resp. graphs of the functions and principles and correctness lemma types) to prove correct.
+
+ [i] is the indice of the function to prove correct
+
+ The lemma to prove if suppose to have been generated by [generate_type] (in $\zeta$ normal form that is
+ it looks like~:
+ [\forall (x_1:t_1)\ldots(x_n:t_n), forall res,
+ res = f x_1\ldots x_n in, \rightarrow graph\ x_1\ldots x_n\ res]
+
+
+ The sketch of the proof is the following one~:
+ \begin{enumerate}
+ \item intros until $x_n$
+ \item $functional\ induction\ (f.(i)\ x_1\ldots x_n)$ using schemes.(i)
+ \item for each generated branch intro [res] and [hres :res = f x_1\ldots x_n], rewrite [hres] and the
+ apply the corresponding constructor of the corresponding graph inductive.
+ \end{enumerate}
+
+*)
+let prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : tactic =
+ fun g ->
+ (* first of all we recreate the lemmas types to be used as predicates of the induction principle
+ that is~:
+ \[fun (x_1:t_1)\ldots(x_n:t_n)=> fun fv => fun res => res = fv \rightarrow graph\ x_1\ldots x_n\ res\]
+ *)
+ let lemmas =
+ Array.map
+ (fun (_,(ctxt,concl)) ->
+ match ctxt with
+ | [] | [_] | [_;_] -> anomaly "bad context"
+ | hres::res::(x,_,t)::ctxt ->
+ Termops.it_mkLambda_or_LetIn
+ ~init:(Termops.it_mkProd_or_LetIn ~init:concl [hres;res])
+ ((x,None,t)::ctxt)
+ )
+ lemmas_types_infos
+ in
+ (* we the get the definition of the graphs block *)
+ let graph_ind = destInd graphs_constr.(i) in
+ let kn = fst graph_ind in
+ let mib,_ = Global.lookup_inductive graph_ind in
+ (* and the principle to use in this lemma in $\zeta$ normal form *)
+ let f_principle,princ_type = schemes.(i) in
+ let princ_type = nf_zeta princ_type in
+ let princ_infos = Tactics.compute_elim_sig princ_type in
+ (* The number of args of the function is then easilly computable *)
+ let nb_fun_args = nb_prod (pf_concl g) - 2 in
+ let args_names = generate_fresh_id (id_of_string "x") [] nb_fun_args in
+ let ids = args_names@(pf_ids_of_hyps g) in
+ (* Since we cannot ensure that the funcitonnal principle is defined in the
+ environement and due to the bug #1174, we will need to pose the principle
+ using a name
+ *)
+ let principle_id = Termops.next_global_ident_away true (id_of_string "princ") ids in
+ let ids = principle_id :: ids in
+ (* We get the branches of the principle *)
+ let branches = List.rev princ_infos.branches in
+ (* and built the intro pattern for each of them *)
+ let intro_pats =
+ List.map
+ (fun (_,_,br_type) ->
+ List.map
+ (fun id -> Genarg.IntroIdentifier id)
+ (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
+ )
+ branches
+ in
+ (* before building the full intro pattern for the principle *)
+ let pat = Genarg.IntroOrAndPattern intro_pats in
+ let eq_ind = Coqlib.build_coq_eq () in
+ let eq_construct = mkConstruct((destInd eq_ind),1) in
+ (* The next to referencies will be used to find out which constructor to apply in each branch *)
+ let ind_number = ref 0
+ and min_constr_number = ref 0 in
+ (* The tactic to prove the ith branch of the principle *)
+ let prove_branche i g =
+ (* We get the identifiers of this branch *)
+ let this_branche_ids =
+ List.fold_right
+ (fun pat acc ->
+ match pat with
+ | Genarg.IntroIdentifier id -> Idset.add id acc
+ | _ -> anomaly "Not an identifier"
+ )
+ (List.nth intro_pats (pred i))
+ Idset.empty
in
- Tactics.compute_elim_sig princ_type
+ (* and get the real args of the branch by unfolding the defined constant *)
+ let pre_args,pre_tac =
+ List.fold_right
+ (fun (id,b,t) (pre_args,pre_tac) ->
+ if Idset.mem id this_branche_ids
+ then
+ match b with
+ | None -> (id::pre_args,pre_tac)
+ | Some b ->
+ (pre_args,
+ tclTHEN (h_reduce (Rawterm.Unfold([[],EvalVarRef id])) allHyps) pre_tac
+ )
+
+ else (pre_args,pre_tac)
+ )
+ (pf_hyps g)
+ ([],tclIDTAC)
+ in
+ (*
+ We can then recompute the arguments of the constructor.
+ For each [hid] introduced by this branch, if [hid] has type
+ $forall res, res=fv -> graph.(j)\ x_1\ x_n res$ the corresponding arguments of the constructor are
+ [ fv (hid fv (refl_equal fv)) ].
+
+ If [hid] has another type the corresponding argument of the constructor is [hid]
+ *)
+ let constructor_args =
+ List.fold_right
+ (fun hid acc ->
+ let type_of_hid = pf_type_of g (mkVar hid) in
+ match kind_of_term type_of_hid with
+ | Prod(_,_,t') ->
+ begin
+ match kind_of_term t' with
+ | Prod(_,t'',t''') ->
+ begin
+ match kind_of_term t'',kind_of_term t''' with
+ | App(eq,args), App(graph',_)
+ when
+ (eq_constr eq eq_ind) &&
+ array_exists (eq_constr graph') graphs_constr ->
+ ((mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|]))
+ ::args.(2)::acc)
+ | _ -> mkVar hid :: acc
+ end
+ | _ -> mkVar hid :: acc
+ end
+ | _ -> mkVar hid :: acc
+ ) pre_args []
+ in
+ (* in fact we must also add the parameters to the constructor args *)
+ let constructor_args =
+ let params_id = fst (list_chop princ_infos.nparams args_names) in
+ (List.map mkVar params_id)@(List.rev constructor_args)
+ in
+ (* We then get the constructor corresponding to this branch and
+ modifies the references has needed i.e.
+ if the constructor is the last one of the current inductive then
+ add one the number of the inductive to take and add the number of constructor of the previous
+ graph to the minimal constructor number
+ *)
+ let constructor =
+ let constructor_num = i - !min_constr_number in
+ let length = Array.length (mib.Declarations.mind_packets.(!ind_number).Declarations.mind_consnames) in
+ if constructor_num <= length
+ then
+ begin
+ (kn,!ind_number),constructor_num
+ end
+ else
+ begin
+ incr ind_number;
+ min_constr_number := !min_constr_number + length ;
+ (kn,!ind_number),1
+ end
+ in
+ (* we can then build the final proof term *)
+ let app_constructor = applist((mkConstruct(constructor)),constructor_args) in
+ (* an apply the tactic *)
+ let res,hres =
+ match generate_fresh_id (id_of_string "z") (ids(* @this_branche_ids *)) 2 with
+ | [res;hres] -> res,hres
+ | _ -> assert false
+ in
+ observe (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor);
+ (
+ tclTHENSEQ
+ [
+ (* unfolding of all the defined variables introduced by this branch *)
+ observe_tac "unfolding" pre_tac;
+ (* $zeta$ normalizing of the conclusion *)
+ h_reduce
+ (Rawterm.Cbv
+ { Rawterm.all_flags with
+ Rawterm.rDelta = false ;
+ Rawterm.rConst = []
+ }
+ )
+ onConcl;
+ (* introducing the the result of the graph and the equality hypothesis *)
+ observe_tac "introducing" (tclMAP h_intro [res;hres]);
+ (* replacing [res] with its value *)
+ observe_tac "rewriting res value" (Equality.rewriteLR (mkVar hres));
+ (* Conclusion *)
+ observe_tac "exact" (h_exact app_constructor)
+ ]
+ )
+ g
in
- let _,_,typhyp = List.find (fun (id,_,_) -> hypname=id) (pf_hyps g) in
- let do_invert fargs appf : tactic =
- let frealargs = (snd (array_chop (List.length princ_info.params) fargs))
+ (* end of branche proof *)
+ let param_names = fst (list_chop princ_infos.nparams args_names) in
+ let params = List.map mkVar param_names in
+ let lemmas = Array.to_list (Array.map (fun c -> applist(c,params)) lemmas) in
+ (* The bindings of the principle
+ that is the params of the principle and the different lemma types
+ *)
+ let bindings =
+ let params_bindings,avoid =
+ List.fold_left2
+ (fun (bindings,avoid) (x,_,_) p ->
+ let id = Termops.next_global_ident_away false (Nameops.out_name x) avoid in
+ (dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid
+ )
+ ([],[])
+ princ_infos.params
+ (List.rev params)
in
- let pat_args =
- (List.map (fun e -> ([Rawterm.ArgArg (-1)],e)) (Array.to_list frealargs)) @ [[],appf]
+ let lemmas_bindings =
+ List.rev (fst (List.fold_left2
+ (fun (bindings,avoid) (x,_,_) p ->
+ let id = Termops.next_global_ident_away false (Nameops.out_name x) avoid in
+ (dummy_loc,Rawterm.NamedHyp id,nf_zeta p)::bindings,id::avoid)
+ ([],avoid)
+ princ_infos.predicates
+ (lemmas)))
in
- tclTHENSEQ
- [
- gen_fargs frealargs;
- tac_pattern pat_args;
- Hiddentac.h_apply (mkConst princ,Rawterm.NoBindings);
- intro_discr_until nprod_goal (finalize fname hypname)
-
+ Rawterm.ExplicitBindings (params_bindings@lemmas_bindings)
+ in
+ tclTHENSEQ
+ [ observe_tac "intro args_names" (tclMAP h_intro args_names);
+ observe_tac "principle" (forward
+ (Some (h_exact f_principle))
+ (Genarg.IntroIdentifier principle_id)
+ princ_type);
+ tclTHEN_i
+ (observe_tac "functional_induction" (
+ fun g ->
+ observe
+ (str "princ" ++ pr_constr_with_binding (Printer.pr_lconstr_env (pf_env g)) (mkVar principle_id,bindings));
+ functional_induction false (applist(funs_constr.(i),List.map mkVar args_names))
+ (Some (mkVar principle_id,bindings))
+ pat g
+ ))
+ (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
+ ]
+ g
+
+(* [generalize_depedent_of x hyp g]
+ generalize every hypothesis which depends of [x] but [hyp]
+*)
+let generalize_depedent_of x hyp g =
+ tclMAP
+ (function
+ | (id,None,t) when not (id = hyp) &&
+ (Termops.occur_var (pf_env g) x t) -> h_generalize [mkVar id]
+ | _ -> tclIDTAC
+ )
+ (pf_hyps g)
+ g
+
+(* [prove_fun_complete funs graphs schemes lemmas_types_infos i]
+ is the tactic used to prove completness lemma.
+
+ [funcs], [graphs] [schemes] [lemmas_types_infos] are the mutually recursive functions
+ (resp. definitions of the graphs of the functions, principles and correctness lemma types) to prove correct.
+
+ [i] is the indice of the function to prove complete
+
+ The lemma to prove if suppose to have been generated by [generate_type] (in $\zeta$ normal form that is
+ it looks like~:
+ [\forall (x_1:t_1)\ldots(x_n:t_n), forall res,
+ graph\ x_1\ldots x_n\ res, \rightarrow res = f x_1\ldots x_n in]
+
+
+ The sketch of the proof is the following one~:
+ \begin{enumerate}
+ \item intros until $H:graph\ x_1\ldots x_n\ res$
+ \item $elim\ H$ using schemes.(i)
+ \item for each generated branch, intro the news hyptohesis, for each such hyptohesis [h], if [h] has
+ type [x=?] with [x] a variable, then subst [x],
+ if [h] has type [t=?] with [t] not a variable then rewrite [t] in the subterms, else
+ if [h] is a match then destruct it, else do just introduce it,
+ after all intros, the conclusion should be a reflexive equality.
+ \end{enumerate}
+
+*)
+
+
+let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
+ fun g ->
+ (* We compute the types of the different mutually recursive lemmas
+ in $\zeta$ normal form
+ *)
+ let lemmas =
+ Array.map
+ (fun (_,(ctxt,concl)) -> nf_zeta (Termops.it_mkLambda_or_LetIn ~init:concl ctxt))
+ lemmas_types_infos
+ in
+ (* We get the constant and the principle corresponding to this lemma *)
+ let f = funcs.(i) in
+ let graph_principle = nf_zeta schemes.(i) in
+ let princ_type = pf_type_of g graph_principle in
+ let princ_infos = Tactics.compute_elim_sig princ_type in
+ (* Then we get the number of argument of the function
+ and compute a fresh name for each of them
+ *)
+ let nb_fun_args = nb_prod (pf_concl g) - 2 in
+ let args_names = generate_fresh_id (id_of_string "x") [] nb_fun_args in
+ let ids = args_names@(pf_ids_of_hyps g) in
+ (* and fresh names for res H and the principle (cf bug bug #1174) *)
+ let res,hres,graph_principle_id =
+ match generate_fresh_id (id_of_string "z") ids 3 with
+ | [res;hres;graph_principle_id] -> res,hres,graph_principle_id
+ | _ -> assert false
+ in
+ let ids = res::hres::graph_principle_id::ids in
+ (* we also compute fresh names for each hyptohesis of each branche of the principle *)
+ let branches = List.rev princ_infos.branches in
+ let intro_pats =
+ List.map
+ (fun (_,_,br_type) ->
+ List.map
+ (fun id -> id)
+ (generate_fresh_id (id_of_string "y") ids (nb_prod br_type))
+ )
+ branches
+ in
+ let eq_ind = Coqlib.build_coq_eq () in
+ (* We will need to change the function by its body
+ using [f_equation] if it is recursive (that is the graph is infinite
+ or unfold if the graph is finite
+ *)
+ let rewrite_tac j ids : tactic =
+ let graph_def = graphs.(j) in
+ if Rtree.is_infinite graph_def.mind_recargs
+ then
+ let eq_lemma =
+ try out_some (find_Function_infos (destConst funcs.(j))).equation_lemma
+ with Failure "out_some" | Not_found -> anomaly "Cannot find equation lemma"
+ in
+ tclTHENSEQ[
+ tclMAP h_intro ids;
+ Equality.rewriteLR (mkConst eq_lemma);
+ (* Don't forget to $\zeta$ normlize the term since the principles have been $\zeta$-normalized *)
+ h_reduce
+ (Rawterm.Cbv
+ {Rawterm.all_flags
+ with Rawterm.rDelta = false;
+ })
+ onConcl
+ ;
+ h_generalize (List.map mkVar ids);
+ thin ids
]
+ else unfold_in_concl [([],Names.EvalConstRef (destConst f))]
+ in
+ (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis
+ (unfolding, substituting, destructing cases \ldots)
+ *)
+ let rec intros_with_rewrite_aux : tactic =
+ fun g ->
+ match kind_of_term (pf_concl g) with
+ | Prod(_,t,t') ->
+ begin
+ match kind_of_term t with
+ | App(eq,args) when (eq_constr eq eq_ind) ->
+ if isVar args.(1)
+ then
+ let id = pf_get_new_id (id_of_string "y") g in
+ tclTHENSEQ [ h_intro id;
+ generalize_depedent_of (destVar args.(1)) id;
+ tclTRY (Equality.rewriteLR (mkVar id));
+ intros_with_rewrite
+ ]
+ g
+ else
+ begin
+ let id = pf_get_new_id (id_of_string "y") g in
+ tclTHENSEQ[
+ h_intro id;
+ tclTRY (Equality.rewriteLR (mkVar id));
+ intros_with_rewrite
+ ] g
+ end
+ | Ind _ when eq_constr t (Coqlib.build_coq_False ()) ->
+ Tauto.tauto g
+ | Case(_,_,v,_) ->
+ tclTHENSEQ[
+ h_case (v,Rawterm.NoBindings);
+ intros_with_rewrite
+ ] g
+ | LetIn _ ->
+ tclTHENSEQ[
+ h_reduce
+ (Rawterm.Cbv
+ {Rawterm.all_flags
+ with Rawterm.rDelta = false;
+ })
+ onConcl
+ ;
+ intros_with_rewrite
+ ] g
+ | _ ->
+ let id = pf_get_new_id (id_of_string "y") g in
+ tclTHENSEQ [ h_intro id;intros_with_rewrite] g
+ end
+ | LetIn _ ->
+ tclTHENSEQ[
+ h_reduce
+ (Rawterm.Cbv
+ {Rawterm.all_flags
+ with Rawterm.rDelta = false;
+ })
+ onConcl
+ ;
+ intros_with_rewrite
+ ] g
+ | _ -> tclIDTAC g
+ and intros_with_rewrite g =
+ observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
+ in
+ (* The proof of each branche itself *)
+ let ind_number = ref 0 in
+ let min_constr_number = ref 0 in
+ let prove_branche i g =
+ (* we fist compute the inductive corresponding to the branch *)
+ let this_ind_number =
+ let constructor_num = i - !min_constr_number in
+ let length = Array.length (graphs.(!ind_number).Declarations.mind_consnames) in
+ if constructor_num <= length
+ then !ind_number
+ else
+ begin
+ incr ind_number;
+ min_constr_number := !min_constr_number + length;
+ !ind_number
+ end
+ in
+ let this_branche_ids = List.nth intro_pats (pred i) in
+ tclTHENSEQ[
+ (* we expand the definition of the function *)
+ observe_tac "rewrite_tac" (rewrite_tac this_ind_number this_branche_ids);
+ (* introduce hypothesis with some rewrite *)
+ (intros_with_rewrite);
+ (* The proof is complete *)
+ observe_tac "reflexivity" (reflexivity)
+ ]
+ g
+ in
+ let params_names = fst (list_chop princ_infos.nparams args_names) in
+ let params = List.map mkVar params_names in
+ tclTHENSEQ
+ [ tclMAP h_intro (args_names@[res;hres]);
+ observe_tac "h_generalize"
+ (h_generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
+ h_intro graph_principle_id;
+ observe_tac "" (tclTHEN_i
+ (observe_tac "elim" ((elim (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings)))))
+ (fun i g -> prove_branche i g ))
+ ]
+ g
+
+
+
+
+let do_save () = Command.save_named false
+
+
+(* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness
+ lemmas for each function in [funs] w.r.t. [graphs]
+
+ [make_scheme] is Functional_principle_types.make_scheme (dependency pb) and
+ [functional_induction] is Indfun.functional_induction (same pb)
+*)
+
+let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) =
+ let funs = Array.of_list funs and graphs = Array.of_list graphs in
+ let funs_constr = Array.map mkConst funs in
+ try
+ let graphs_constr = Array.map mkInd graphs in
+ let lemmas_types_infos =
+ Util.array_map2_i
+ (fun i f_constr graph ->
+ let const_of_f = destConst f_constr in
+ let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info =
+ generate_type false const_of_f graph i
+ in
+ let type_of_lemma = Termops.it_mkProd_or_LetIn ~init:type_of_lemma_concl type_of_lemma_ctxt in
+ let type_of_lemma = nf_zeta type_of_lemma in
+ observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma);
+ type_of_lemma,type_info
+ )
+ funs_constr
+ graphs_constr
+ in
+ let schemes =
+ (* The functional induction schemes are computed and not saved if there is more that one function
+ if the block contains only one function we can safely reuse [f_rect]
+ *)
+ try
+ if Array.length funs_constr <> 1 then raise Not_found;
+ [| find_induction_principle funs_constr.(0) |]
+ with Not_found ->
+ Array.of_list
+ (List.map
+ (fun entry ->
+ (entry.Entries.const_entry_body, out_some entry.Entries.const_entry_type )
+ )
+ (make_scheme (array_map_to_list (fun const -> const,Rawterm.RType None) funs))
+ )
in
- match kind_of_term typhyp with
- | App(eq',[| _ ; arg1 ; arg2 |]) when eq_constr eq' (Lazy.force eq) ->
-(* let valf = def_of_const (mkConst fname) in *)
- let eq_arg1 , eq_arg2 , good_eq_form , fargs =
- match kind_of_term arg1 , kind_of_term arg2 with
- | App(f, args),_ when eq_constr f (mkConst fname) ->
- arg1 , arg2 , tclIDTAC , args
- | _,App(f, args) when eq_constr f (mkConst fname) ->
- arg2 , arg1 , symmetry_in hypname , args
- | _ , _ -> error "inversion impossible"
- in
- tclTHEN
- good_eq_form
- (do_invert fargs eq_arg1)
- g
- | App(f',fargs) when eq_constr f' (mkConst fname) ->
- do_invert fargs typhyp g
-
-
- | _ -> error "inversion impossible"
+ let proving_tac =
+ prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos
+ in
+ Array.iteri
+ (fun i f_as_constant ->
+ let f_id = id_of_label (con_label f_as_constant) in
+ Command.start_proof
+ (*i The next call to mk_correct_id is valid since we are constructing the lemma
+ Ensures by: obvious
+ i*)
+ (mk_correct_id f_id)
+ (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
+ (fst lemmas_types_infos.(i))
+ (fun _ _ -> ());
+ Pfedit.by (observe_tac ("procve correctness ("^(string_of_id f_id)^")") (proving_tac i));
+ do_save ();
+ let finfo = find_Function_infos f_as_constant in
+ update_Function
+ {finfo with
+ correctness_lemma = Some (destConst (Tacinterp.constr_of_id (Global.env ())(mk_correct_id f_id)))
+ }
+
+ )
+ funs;
+ let lemmas_types_infos =
+ Util.array_map2_i
+ (fun i f_constr graph ->
+ let const_of_f = destConst f_constr in
+ let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info =
+ generate_type true const_of_f graph i
+ in
+ let type_of_lemma = Termops.it_mkProd_or_LetIn ~init:type_of_lemma_concl type_of_lemma_ctxt in
+ let type_of_lemma = nf_zeta type_of_lemma in
+ observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma);
+ type_of_lemma,type_info
+ )
+ funs_constr
+ graphs_constr
+ in
+ let kn,_ as graph_ind = destInd graphs_constr.(0) in
+ let mib,mip = Global.lookup_inductive graph_ind in
+ let schemes =
+ Array.of_list
+ (Indrec.build_mutual_indrec (Global.env ()) Evd.empty
+ (Array.to_list
+ (Array.mapi
+ (fun i mip -> (kn,i),mib,mip,true,InType)
+ mib.Declarations.mind_packets
+ )
+ )
+ )
+ in
+ let proving_tac =
+ prove_fun_complete funs_constr mib.Declarations.mind_packets schemes lemmas_types_infos
+ in
+ Array.iteri
+ (fun i f_as_constant ->
+ let f_id = id_of_label (con_label f_as_constant) in
+ Command.start_proof
+ (*i The next call to mk_complete_id is valid since we are constructing the lemma
+ Ensures by: obvious
+ i*)
+ (mk_complete_id f_id)
+ (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
+ (fst lemmas_types_infos.(i))
+ (fun _ _ -> ());
+ Pfedit.by (observe_tac ("prove completeness ("^(string_of_id f_id)^")") (proving_tac i));
+ do_save ();
+ let finfo = find_Function_infos f_as_constant in
+ update_Function
+ {finfo with
+ completeness_lemma = Some (destConst (Tacinterp.constr_of_id (Global.env ())(mk_complete_id f_id)))
+ }
+ )
+ funs;
+ with e ->
+ (* In case of problem, we reset all the lemmas *)
+ (*i The next call to mk_correct_id is valid since we are erasing the lemmas
+ Ensures by: obvious
+ i*)
+ let first_lemma_id =
+ let f_id = id_of_label (con_label funs.(0)) in
+
+ mk_correct_id f_id
+ in
+ ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,first_lemma_id) with _ -> ());
+ raise e
+
+
+
+
+
+(***********************************************)
+
+(* [revert_graph kn post_tac hid] transforme an hypothesis [hid] having type Ind(kn,num) t1 ... tn res
+ when [kn] denotes a graph block into
+ f_num t1... tn = res (by applying [f_complete] to the first type) before apply post_tac on the result
+
+ if the type of hypothesis has not this form or if we cannot find the completeness lemma then we do nothing
+*)
+let revert_graph kn post_tac hid g =
+ let typ = pf_type_of g (mkVar hid) in
+ match kind_of_term typ with
+ | App(i,args) when isInd i ->
+ let ((kn',num) as ind') = destInd i in
+ if kn = kn'
+ then (* We have generated a graph hypothesis so that we must change it if we can *)
+ let info =
+ try find_Function_of_graph ind'
+ with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*)
+ anomaly "Cannot retrieve infos about a mutual block"
+ in
+ (* if we can find a completeness lemma for this function
+ then we can come back to the functional form. If not, we do nothing
+ *)
+ match info.completeness_lemma with
+ | None -> tclIDTAC g
+ | Some f_complete ->
+ let f_args,res = array_chop (Array.length args - 1) args in
+ tclTHENSEQ
+ [
+ h_generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])];
+ thin [hid];
+ h_intro hid;
+ post_tac hid
+ ]
+ g
+
+ else tclIDTAC g
+ | _ -> tclIDTAC g
+
+
+(*
+ [functional_inversion hid fconst f_correct ] is the functional version of [inversion]
+
+ [hid] is the hypothesis to invert, [fconst] is the function to invert and [f_correct]
+ is the correctness lemma for [fconst].
+
+ The sketch is the follwing~:
+ \begin{enumerate}
+ \item Transforms the hypothesis [hid] such that its type is now $res\ =\ f\ t_1 \ldots t_n$
+ (fails if it is not possible)
+ \item replace [hid] with $R\_f t_1 \ldots t_n res$ using [f_correct]
+ \item apply [inversion] on [hid]
+ \item finally in each branch, replace each hypothesis [R\_f ..] by [f ...] using [f_complete] (whenever
+ such a lemma exists)
+ \end{enumerate}
+*)
+
+let functional_inversion kn hid fconst f_correct : tactic =
+ fun g ->
+ let old_ids = List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty in
+ let type_of_h = pf_type_of g (mkVar hid) in
+ match kind_of_term type_of_h with
+ | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) ->
+ let pre_tac,f_args,res =
+ match kind_of_term args.(1),kind_of_term args.(2) with
+ | App(f,f_args),_ when eq_constr f fconst ->
+ ((fun hid -> h_symmetry (onHyp hid)),f_args,args.(2))
+ |_,App(f,f_args) when eq_constr f fconst ->
+ ((fun hid -> tclIDTAC),f_args,args.(1))
+ | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2)
+ in
+ tclTHENSEQ[
+ pre_tac hid;
+ h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
+ thin [hid];
+ h_intro hid;
+ Inv.inv FullInversion Genarg.IntroAnonymous (Rawterm.NamedHyp hid);
+ (fun g ->
+ let new_ids = List.filter (fun id -> not (Idset.mem id old_ids)) (pf_ids_of_hyps g) in
+ tclMAP (revert_graph kn pre_tac) (hid::new_ids) g
+ );
+ ] g
+ | _ -> tclFAIL 1 (mt ()) g
+
+
+
+let invfun qhyp f =
+ let f =
+ match f with
+ | ConstRef f -> f
+ | _ -> raise (Util.UserError("",str "Not a function"))
+ in
+ try
+ let finfos = find_Function_infos f in
+ let f_correct = mkConst(out_some finfos.correctness_lemma)
+ and kn = fst finfos.graph_ind
+ in
+ Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f) f_correct) qhyp
+ with
+ | Not_found -> error "No graph found"
+ | Failure "out_some" -> error "Cannot use equivalence with graph!"
+
+let invfun qhyp f g =
+ match f with
+ | Some f -> invfun qhyp f g
+ | None ->
+ Tactics.try_intros_until
+ (fun hid g ->
+ let hyp_typ = pf_type_of g (mkVar hid) in
+ match kind_of_term hyp_typ with
+ | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) ->
+ begin
+ let f1,_ = decompose_app args.(1) in
+ try
+ if not (isConst f1) then failwith "";
+ let finfos = find_Function_infos (destConst f1) in
+ let f_correct = mkConst(out_some finfos.correctness_lemma)
+ and kn = fst finfos.graph_ind
+ in
+ functional_inversion kn hid f1 f_correct g
+ with | Failure "" | Failure "out_some" | Not_found ->
+ try
+ let f2,_ = decompose_app args.(2) in
+ if not (isConst f2) then failwith "";
+ let finfos = find_Function_infos (destConst f2) in
+ let f_correct = mkConst(out_some finfos.correctness_lemma)
+ and kn = fst finfos.graph_ind
+ in
+ functional_inversion kn hid f2 f_correct g
+ with
+ | Failure "" ->
+ errorlabstrm "" (Ppconstr.pr_id hid ++ str " must contain at leat one function")
+ | Failure "out_some" ->
+ error "Cannot use equivalence with graph for any side of equality"
+ | Not_found -> error "No graph found for any side of equality"
+ end
+ | _ -> errorlabstrm "" (Ppconstr.pr_id hid ++ str " must be an equality ")
+ )
+ qhyp
+ g
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index b6f26dfd..dbf2f944 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -9,11 +9,11 @@ open Util
open Rawtermops
let observe strm =
- if Tacinterp.get_debug () <> Tactic_debug.DebugOff && false
+ if do_observe ()
then Pp.msgnl strm
else ()
let observennl strm =
- if Tacinterp.get_debug () <> Tactic_debug.DebugOff &&false
+ if do_observe ()
then Pp.msg strm
else ()
@@ -44,12 +44,8 @@ let compose_raw_context =
(*
The main part deals with building a list of raw constructor expressions
from the rhs of a fixpoint equation.
-
-
*)
-
-
type 'a build_entry_pre_return =
{
context : raw_context; (* the binding context of the result *)
@@ -62,7 +58,6 @@ type 'a build_entry_return =
to_avoid : identifier list
}
-
(*
[combine_results combine_fun res1 res2] combine two results [res1] and [res2]
w.r.t. [combine_fun].
@@ -113,8 +108,6 @@ let combine_args arg args =
let ids_of_binder = function
| LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> []
| LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> [id]
-(* | LetTuple(nal,_) -> *)
-(* map_succeed (function Name id -> id | _ -> failwith "ids_of_binder") nal *)
let rec change_vars_in_binder mapping = function
[] -> []
@@ -216,7 +209,6 @@ let combine_app f args =
(* Note that the binding context of [args] MUST be placed before the one of
the applied value in order to preserve possible type dependencies
*)
-
context = args.context@new_ctxt;
value = new_value;
}
@@ -245,10 +237,9 @@ let mk_result ctxt value avoid =
;
to_avoid = avoid
}
-
-
-let make_discr_match_el =
- List.map (fun e -> (e,(Anonymous,None)))
+(*************************************************
+ Some functions to deal with overlapping patterns
+**************************************************)
let coq_True_ref =
lazy (Coqlib.gen_reference "" ["Init";"Logic"] "True")
@@ -256,6 +247,25 @@ let coq_True_ref =
let coq_False_ref =
lazy (Coqlib.gen_reference "" ["Init";"Logic"] "False")
+(*
+ [make_discr_match_el \[e1,...en\]] builds match e1,...,en with
+ (the list of expresions on which we will do the matching)
+ *)
+let make_discr_match_el =
+ List.map (fun e -> (e,(Anonymous,None)))
+
+(*
+ [make_discr_match_brl i \[pat_1,...,pat_n\]] constructs a discrimination pattern matching on the ith expression.
+ that is.
+ match ?????? with \\
+ | pat_1 => False \\
+ | pat_{i-1} => False \\
+ | pat_i => True \\
+ | pat_{i+1} => False \\
+ \vdots
+ | pat_n => False
+ end
+*)
let make_discr_match_brl i =
list_map_i
(fun j (_,idl,patl,_) ->
@@ -264,84 +274,28 @@ let make_discr_match_brl i =
else (dummy_loc,idl,patl, mkRRef (Lazy.force coq_False_ref))
)
0
-
+(*
+ [make_discr_match brl el i] generates an hypothesis such that it reduce to true iff
+ brl_{i} is the first branch matched by [el]
+
+ Used when we want to simulate the coq pattern matching algorithm
+*)
let make_discr_match brl =
fun el i ->
mkRCases(None,
make_discr_match_el el,
make_discr_match_brl i brl)
-
-
-
-let rec make_pattern_eq_precond id e pat : identifier * (binder_type * Rawterm.rawconstr) list =
- match pat with
- | PatVar(_,Anonymous) -> assert false
- | PatVar(_,Name x) ->
- id,[Prod (Name x),mkRHole ();Prod Anonymous,raw_make_eq (mkRVar x) e]
- | PatCstr(_,constr,patternl,_) ->
- let new_id,new_patternl,patternl_eq_precond =
- List.fold_right
- (fun pat' (id,new_patternl,preconds) ->
- match pat' with
- | PatVar (_,Name id) -> (id,id::new_patternl,preconds)
- | _ ->
- let new_id = Nameops.lift_ident id in
- let new_id',pat'_precond =
- make_pattern_eq_precond new_id (mkRVar id) pat'
- in
- (new_id',id::new_patternl,preconds@pat'_precond)
- )
- patternl
- (id,[],[])
- in
- let cst_narg =
- Inductiveops.mis_constructor_nargs_env
- (Global.env ())
- constr
- in
- let implicit_args =
- Array.to_list
- (Array.init
- (cst_narg - List.length patternl)
- (fun _ -> mkRHole ())
- )
- in
- let cst_as_term =
- mkRApp(mkRRef(Libnames.ConstructRef constr),
- implicit_args@(List.map mkRVar new_patternl)
- )
- in
- let precond' =
- (Prod Anonymous, raw_make_eq cst_as_term e)::patternl_eq_precond
- in
- let precond'' =
- List.fold_right
- (fun id acc ->
- (Prod (Name id),(mkRHole ()))::acc
- )
- new_patternl
- precond'
- in
- new_id,precond''
let pr_name = function
| Name id -> Ppconstr.pr_id id
| Anonymous -> str "_"
-let make_pattern_eq_precond id e pat =
- let res = make_pattern_eq_precond id e pat in
- observe
- (prlist_with_sep spc
- (function (Prod na,t) ->
- str "forall " ++ pr_name na ++ str ":" ++ pr_rawconstr t
- | _ -> assert false
- )
- (snd res)
- );
- res
-
+(**********************************************************************)
+(* functions used to build case expression from lettuple and if ones *)
+(**********************************************************************)
-let build_constructors_of_type msg ind' argl =
+(* [build_constructors_of_type] construct the array of pattern of its inductive argument*)
+let build_constructors_of_type ind' argl =
let (mib,ind) = Inductive.lookup_mind_specif (Global.env()) ind' in
let npar = mib.Declarations.mind_nparams in
Array.mapi (fun i _ ->
@@ -366,21 +320,11 @@ let build_constructors_of_type msg ind' argl =
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
-
-
-
+(* [find_type_of] very naive attempts to discover the type of an if or a letin *)
let rec find_type_of nb b =
let f,_ = raw_decompose_app b in
match f with
@@ -412,18 +356,145 @@ let rec find_type_of nb b =
| _ -> 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); *)
+
+
+(******************)
+(* Main functions *)
+(******************)
+
+
+
+let raw_push_named (na,raw_value,raw_typ) env =
+ match na with
+ | Anonymous -> env
+ | Name id ->
+ let value = Util.option_map (Pretyping.Default.understand Evd.empty env) raw_value in
+ let typ = Pretyping.Default.understand_type Evd.empty env raw_typ in
+ Environ.push_named (id,value,typ) env
+
+
+let add_pat_variables pat typ env : Environ.env =
+ let rec add_pat_variables env pat typ : Environ.env =
+ observe (str "new rel env := " ++ Printer.pr_rel_context_of env);
+
+ match pat with
+ | PatVar(_,na) -> Environ.push_rel (na,None,typ) env
+ | PatCstr(_,c,patl,na) ->
+ let Inductiveops.IndType(indf,indargs) =
+ try Inductiveops.find_rectype env Evd.empty typ
+ with Not_found -> assert false
+ in
+ let constructors = Inductiveops.get_constructors env indf in
+ let constructor : Inductiveops.constructor_summary = List.find (fun cs -> cs.Inductiveops.cs_cstr = c) (Array.to_list constructors) in
+ let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
+ List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
+ in
+ let new_env = add_pat_variables env pat typ in
+ let res =
+ fst (
+ Sign.fold_rel_context
+ (fun (na,v,t) (env,ctxt) ->
+ match na with
+ | Anonymous -> assert false
+ | Name id ->
+ let new_t = substl ctxt t in
+ let new_v = option_map (substl ctxt) v in
+ observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
+ str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
+ str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++
+ option_fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++
+ option_fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ())
+ );
+ (Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt)
+ )
+ (Environ.rel_context new_env)
+ ~init:(env,[])
+ )
+ in
+ observe (str "new var env := " ++ Printer.pr_named_context_of res);
+ res
+
+
+
+
+let rec pattern_to_term_and_type env typ = function
+ | PatVar(loc,Anonymous) -> assert false
+ | PatVar(loc,Name id) ->
+ mkRVar id
+ | PatCstr(loc,constr,patternl,_) ->
+ let cst_narg =
+ Inductiveops.mis_constructor_nargs_env
+ (Global.env ())
+ constr
+ in
+ let Inductiveops.IndType(indf,indargs) =
+ try Inductiveops.find_rectype env Evd.empty typ
+ with Not_found -> assert false
+ in
+ let constructors = Inductiveops.get_constructors env indf in
+ let constructor = List.find (fun cs -> cs.Inductiveops.cs_cstr = constr) (Array.to_list constructors) in
+ let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
+ let _,cstl = Inductiveops.dest_ind_family indf in
+ let csta = Array.of_list cstl in
+ let implicit_args =
+ Array.to_list
+ (Array.init
+ (cst_narg - List.length patternl)
+ (fun i -> Detyping.detype false [] (Termops.names_of_rel_context env) csta.(i))
+ )
+ in
+ let patl_as_term =
+ List.map2 (pattern_to_term_and_type env) (List.rev cs_args_types) patternl
+ in
+ mkRApp(mkRRef(Libnames.ConstructRef constr),
+ implicit_args@patl_as_term
+ )
+
+(* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return)
+ of constructors corresponding to [rt] when replacing calls to [funnames] by calls to the
+ corresponding graphs.
+
+
+ The idea to transform a term [t] into a list of constructors [lc] is the following:
+ \begin{itemize}
+ \item if the term is a binder (bind x, body) then first compute [lc'] the list corresponding
+ to [body] and add (bind x. _) to each elements of [lc]
+ \item if the term has the form (g t1 ... ... tn) where g does not appears in (fnames)
+ then compute [lc1] ... [lcn] the lists of constructors corresponding to [t1] ... [tn],
+ then combine those lists and [g] as follows~: for each element [c1,...,cn] of [lc1\times...\times lcn],
+ [g c1 ... cn] is an element of [lc]
+ \item if the term has the form (f t1 .... tn) where [f] appears in [fnames] then
+ compute [lc1] ... [lcn] the lists of constructors corresponding to [t1] ... [tn],
+ then compute those lists and [f] as follows~: for each element [c1,...,cn] of [lc1\times...\times lcn]
+ create a new variable [res] and [forall res, R_f c1 ... cn res] is in [lc]
+ \item if the term is a cast just treat its body part
+ \item
+ if the term is a match, an if or a lettuple then compute the lists corresponding to each branch of the case
+ and concatenate them (informally, each branch of a match produces a new constructor)
+ \end{itemize}
+
+ WARNING: The terms constructed here are only USING the rawconstr syntax but are highly bad formed.
+ We must wait to have complete all the current calculi to set the recursive calls.
+ At this point, each term [f t1 ... tn] (where f appears in [funnames]) is replaced by
+ a pseudo term [forall res, res t1 ... tn, res]. A reconstruction phase is done later.
+ We in fact not create a constructor list since then end of each constructor has not the expected form
+ but only the value of the function
+*)
+
+
+let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return =
+ observe (str " Entering : " ++ Printer.pr_rawconstr rt);
match rt with
| RRef _ | RVar _ | REvar _ | RPatVar _ | RSort _ | RHole _ ->
- mk_result [] rt avoid
+ (* do nothing (except changing type of course) *)
+ mk_result [] rt avoid
| RApp(_,_,_) ->
let f,args = raw_decompose_app rt in
let args_res : (rawconstr list) build_entry_return =
- List.fold_right
+ List.fold_right (* create the arguments lists of constructors and combine them *)
(fun arg ctxt_argsl ->
- let arg_res = build_entry_lc funnames ctxt_argsl.to_avoid arg in
- combine_results combine_args arg_res ctxt_argsl
+ let arg_res = build_entry_lc env funnames ctxt_argsl.to_avoid arg in
+ combine_results combine_args arg_res ctxt_argsl
)
args
(mk_result [] [] avoid)
@@ -431,6 +502,16 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
begin
match f with
| RVar(_,id) when Idset.mem id funnames ->
+ (* if we have [f t1 ... tn] with [f]$\in$[fnames]
+ then we create a fresh variable [res],
+ add [res] and its "value" (i.e. [res v1 ... vn]) to each
+ pseudo constructor build for the arguments (i.e. a pseudo context [ctxt] and
+ a pseudo value "v1 ... vn".
+ The "value" of this branch is then simply [res]
+ *)
+ let rt_as_constr = Pretyping.Default.understand Evd.empty env rt in
+ let rt_typ = Typing.type_of env Evd.empty rt_as_constr in
+ let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in
let res = fresh_id args_res.to_avoid "res" in
let new_avoid = res::args_res.to_avoid in
let res_rt = mkRVar res in
@@ -438,7 +519,7 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
List.map
(fun arg_res ->
let new_hyps =
- [Prod (Name res),mkRHole ();
+ [Prod (Name res),res_raw_type;
Prod Anonymous,mkRApp(res_rt,(mkRVar id)::arg_res.value)]
in
{context = arg_res.context@new_hyps; value = res_rt }
@@ -447,6 +528,11 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
in
{ result = new_result; to_avoid = new_avoid }
| RVar _ | REvar _ | RPatVar _ | RHole _ | RSort _ | RRef _ ->
+ (* if have [g t1 ... tn] with [g] not appearing in [funnames]
+ then
+ foreach [ctxt,v1 ... vn] in [args_res] we return
+ [ctxt, g v1 .... vn]
+ *)
{
args_res with
result =
@@ -455,8 +541,12 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
{args_res with value = mkRApp(f,args_res.value)})
args_res.result
}
- | RApp _ -> assert false (* we have collected all the app *)
+ | RApp _ -> assert false (* we have collected all the app in [raw_decompose_app] *)
| RLetIn(_,n,t,b) ->
+ (* if we have [(let x := v in b) t1 ... tn] ,
+ we discard our work and compute the list of constructor for
+ [let x = v in (b t1 ... tn)] up to alpha conversion
+ *)
let new_n,new_b,new_avoid =
match n with
| Name id when List.exists (is_free_in id) args ->
@@ -473,136 +563,169 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
| _ -> n,b,avoid
in
build_entry_lc
+ env
funnames
avoid
(mkRLetIn(new_n,t,mkRApp(new_b,args)))
| RCases _ | RLambda _ | RIf _ | RLetTuple _ ->
- let f_res = build_entry_lc funnames args_res.to_avoid f in
+ (* we have [(match e1, ...., en with ..... end) t1 tn]
+ we first compute the result from the case and
+ then combine each of them with each of args one
+ *)
+ let f_res = build_entry_lc env funnames args_res.to_avoid f in
combine_results combine_app f_res args_res
- | RDynamic _ ->error "Not handled RDynamic"
+ | RDynamic _ ->error "Not handled RDynamic"
| RCast(_,b,_,_) ->
- build_entry_lc funnames avoid (mkRApp(b,args))
+ (* for an applied cast we just trash the cast part
+ and restart the work.
+
+ WARNING: We need to restart since [b] itself should be an application term
+ *)
+ build_entry_lc env funnames avoid (mkRApp(b,args))
| RRec _ -> error "Not handled RRec"
| RProd _ -> error "Cannot apply a type"
- end
+ end (* end of the application treatement *)
+
| RLambda(_,n,t,b) ->
- let b_res = build_entry_lc funnames avoid b in
- let t_res = build_entry_lc funnames avoid t in
+ (* we first compute the list of constructor
+ corresponding to the body of the function,
+ then the one corresponding to the type
+ and combine the two result
+ *)
+ let t_res = build_entry_lc env funnames avoid t in
let new_n =
match n with
| Name _ -> n
| Anonymous -> Name (Indfun_common.fresh_id [] "_x")
in
+ let new_env = raw_push_named (new_n,None,t) env in
+ let b_res = build_entry_lc new_env funnames avoid b in
combine_results (combine_lam new_n) t_res b_res
| RProd(_,n,t,b) ->
- let b_res = build_entry_lc funnames avoid b in
- let t_res = build_entry_lc funnames avoid t in
+ (* we first compute the list of constructor
+ corresponding to the body of the function,
+ then the one corresponding to the type
+ and combine the two result
+ *)
+ let t_res = build_entry_lc env funnames avoid t in
+ let new_env = raw_push_named (n,None,t) env in
+ let b_res = build_entry_lc new_env funnames avoid b in
combine_results (combine_prod n) t_res b_res
- | RLetIn(_,n,t,b) ->
- let b_res = build_entry_lc funnames avoid b in
- let t_res = build_entry_lc funnames avoid t in
- combine_results (combine_letin n) t_res b_res
+ | RLetIn(_,n,v,b) ->
+ (* we first compute the list of constructor
+ corresponding to the body of the function,
+ then the one corresponding to the value [t]
+ and combine the two result
+ *)
+ let v_res = build_entry_lc env funnames avoid v in
+ let v_as_constr = Pretyping.Default.understand Evd.empty env v in
+ let v_type = Typing.type_of env Evd.empty v_as_constr in
+ let new_env =
+ match n with
+ Anonymous -> env
+ | Name id -> Environ.push_named (id,Some v_as_constr,v_type) env
+ in
+ let b_res = build_entry_lc new_env funnames avoid b in
+ combine_results (combine_letin n) v_res b_res
| RCases(_,_,el,brl) ->
+ (* we create the discrimination function
+ and treat the case itself
+ *)
let make_discr = make_discr_match brl in
- build_entry_lc_from_case funnames make_discr el brl avoid
+ build_entry_lc_from_case env funnames make_discr el brl avoid
| 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
+ let b_as_constr = Pretyping.Default.understand Evd.empty env b in
+ let b_typ = Typing.type_of env Evd.empty b_as_constr in
+ let (ind,_) =
+ try Inductiveops.find_inductive env Evd.empty b_typ
+ with Not_found ->
+ errorlabstrm "" (str "Cannot find the inductive associated to " ++
+ Printer.pr_rawconstr b ++ str " in " ++
+ Printer.pr_rawconstr rt ++ str ". try again with a cast")
+ in
+ let case_pats = build_constructors_of_type ind [] in
+ assert (Array.length case_pats = 2);
+ let brl =
+ list_map_i
+ (fun i x -> (dummy_loc,[],[case_pats.(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 env funnames avoid match_expr
| RLetTuple(_,nal,_,b,e) ->
- begin
- let nal_as_rawconstr =
- List.map
- (function
- Name id -> mkRVar id
+ begin
+ let nal_as_rawconstr =
+ List.map
+ (function
+ Name id -> mkRVar id
| Anonymous -> mkRHole ()
)
- nal
+ 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
-
+ let b_as_constr = Pretyping.Default.understand Evd.empty env b in
+ let b_typ = Typing.type_of env Evd.empty b_as_constr in
+ let (ind,_) =
+ try Inductiveops.find_inductive env Evd.empty b_typ
+ with Not_found ->
+ errorlabstrm "" (str "Cannot find the inductive associated to " ++
+ Printer.pr_rawconstr b ++ str " in " ++
+ Printer.pr_rawconstr rt ++ str ". try again with a cast")
+ in
+ let case_pats = build_constructors_of_type ind nal_as_rawconstr in
+ assert (Array.length case_pats = 1);
+ let br =
+ (dummy_loc,[],[case_pats.(0)],e)
+ in
+ let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in
+ build_entry_lc env funnames avoid match_expr
+
end
| RRec _ -> error "Not handled RRec"
| RCast(_,b,_,_) ->
- build_entry_lc funnames avoid b
+ build_entry_lc env funnames avoid b
| RDynamic _ -> error "Not handled RDynamic"
-and build_entry_lc_from_case funname make_discr
+and build_entry_lc_from_case env funname make_discr
(el:tomatch_tuple)
(brl:Rawterm.cases_clauses) avoid :
rawconstr build_entry_return =
match el with
- | [] -> assert false (* matched on Nothing !*)
+ | [] -> assert false (* this case correspond to match <nothing> with .... !*)
| el ->
+ (* this case correspond to
+ match el with brl end
+ we first compute the list of lists corresponding to [el] and
+ combine them .
+ Then for each elemeent of the combinations,
+ we compute the result we compute one list per branch in [brl] and
+ finally we just concatenate those list
+ *)
let case_resl =
List.fold_right
(fun (case_arg,_) ctxt_argsl ->
- let arg_res = build_entry_lc funname avoid case_arg in
+ let arg_res = build_entry_lc env funname avoid case_arg in
combine_results combine_args arg_res ctxt_argsl
)
el
(mk_result [] [] avoid)
in
+ (****** The next works only if the match is not dependent ****)
+ let types =
+ List.map (fun (case_arg,_) ->
+ let case_arg_as_constr = Pretyping.Default.understand Evd.empty env case_arg in
+ Typing.type_of env Evd.empty case_arg_as_constr
+ ) el
+ in
let results =
List.map
- (build_entry_lc_from_case_term funname (make_discr (List.map fst el)) [] brl case_resl.to_avoid)
+ (build_entry_lc_from_case_term
+ env types
+ funname (make_discr (* (List.map fst el) *))
+ [] brl
+ case_resl.to_avoid)
case_resl.result
in
{
@@ -611,36 +734,54 @@ and build_entry_lc_from_case funname make_discr
List.fold_left (fun acc r -> list_union acc r.to_avoid) [] results
}
-and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avoid
+and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid
matched_expr =
match brl with
| [] -> (* computed_branches *) {result = [];to_avoid = avoid}
| br::brl' ->
+ (* alpha convertion to prevent name clashes *)
let _,idl,patl,return = alpha_br avoid br in
- let new_avoid = idl@avoid in
-(* let e_ctxt,el = (matched_expr.context,matched_expr.value) in *)
-(* if (List.length patl) <> (List.length el) *)
-(* then error ("Pattern matching on product: not yet implemented"); *)
+ let new_avoid = idl@avoid in (* for now we can no more use idl as an indentifier *)
+ (* building a list of precondition stating that we are not in this branch
+ (will be used in the following recursive calls)
+ *)
+ let new_env = List.fold_right2 add_pat_variables patl types env in
let not_those_patterns : (identifier list -> rawconstr -> rawconstr) list =
- List.map
- (fun pat ->
+ List.map2
+ (fun pat typ ->
fun avoid pat'_as_term ->
let renamed_pat,_,_ = alpha_pat avoid pat in
let pat_ids = get_pattern_id renamed_pat in
- List.fold_right
- (fun id acc -> mkRProd (Name id,mkRHole (),acc))
+ let env_with_pat_ids = add_pat_variables pat typ new_env in
+ List.fold_right
+ (fun id acc ->
+ let typ_of_id = Typing.type_of env_with_pat_ids Evd.empty (mkVar id) in
+ let raw_typ_of_id =
+ Detyping.detype false [] (Termops.names_of_rel_context env_with_pat_ids) typ_of_id
+ in
+ mkRProd (Name id,raw_typ_of_id,acc))
pat_ids
(raw_make_neq pat'_as_term (pattern_to_term renamed_pat))
)
patl
+ types
in
+ (* Checking if we can be in this branch
+ (will be used in the following recursive calls)
+ *)
let unify_with_those_patterns : (cases_pattern -> bool*bool) list =
List.map
(fun pat pat' -> are_unifiable pat pat',eq_cases_pattern pat pat')
patl
in
+ (*
+ we first compute the other branch result (in ordrer to keep the order of the matching
+ as much as possible)
+ *)
let brl'_res =
build_entry_lc_from_case_term
+ env
+ types
funname
make_discr
((unify_with_those_patterns,not_those_patterns)::patterns_to_prevent)
@@ -648,48 +789,63 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo
avoid
matched_expr
in
+ (* We know create the precondition of this branch i.e.
+
+ 1- the list of variable appearing in the different patterns of this branch and
+ the list of equation stating than el = patl (List.flatten ...)
+ 2- If there exists a previous branch which pattern unify with the one of this branch
+ then a discrimination precond stating that we are not in a previous branch (if List.exists ...)
+ *)
let those_pattern_preconds =
-( List.flatten
+ (List.flatten
(
- List.map2
- (fun pat e ->
+ list_map3
+ (fun pat e typ_as_constr ->
let this_pat_ids = ids_of_pat pat in
+ let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_as_constr in
let pat_as_term = pattern_to_term pat in
List.fold_right
(fun id acc ->
if Idset.mem id this_pat_ids
- then (Prod (Name id),mkRHole ())::acc
+ then (Prod (Name id),
+ let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in
+ let raw_typ_of_id =
+ Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_of_id
+ in
+ raw_typ_of_id
+ )::acc
else acc
)
idl
- [(Prod Anonymous,raw_make_eq pat_as_term e)]
+ [(Prod Anonymous,raw_make_eq ~typ pat_as_term e)]
)
patl
matched_expr.value
+ types
+ )
)
-)
@
- (if List.exists (function (unifl,neql) ->
- let (unif,eqs) =
- List.split (List.map2 (fun x y -> x y) unifl patl)
- in
- List.for_all (fun x -> x) unif) patterns_to_prevent
- then
- let i = List.length patterns_to_prevent in
- [(Prod Anonymous,make_discr i )]
- else
- []
- )
+ (if List.exists (function (unifl,_) ->
+ let (unif,_) =
+ List.split (List.map2 (fun x y -> x y) unifl patl)
+ in
+ List.for_all (fun x -> x) unif) patterns_to_prevent
+ then
+ let i = List.length patterns_to_prevent in
+ let pats_as_constr = List.map2 (pattern_to_term_and_type new_env) types patl in
+ [(Prod Anonymous,make_discr pats_as_constr i )]
+ else
+ []
+ )
in
- let return_res = build_entry_lc funname new_avoid return in
+ (* We compute the result of the value returned by the branch*)
+ let return_res = build_entry_lc new_env funname new_avoid return in
+ (* and combine it with the preconds computed for this branch *)
let this_branch_res =
List.map
(fun res ->
- { context =
- matched_expr.context@
-(* ids@ *)
- those_pattern_preconds@res.context ;
+ { context = matched_expr.context@those_pattern_preconds@res.context ;
value = res.value}
)
return_res.result
@@ -702,7 +858,9 @@ let is_res id =
String.sub (string_of_id id) 0 3 = "res"
with Invalid_argument _ -> false
-(* rebuild the raw constructors expression.
+(*
+ The second phase which reconstruct the real type of the constructor.
+ rebuild the raw constructors expression.
eliminates some meaningless equalities, applies some rewrites......
*)
let rec rebuild_cons nb_args relname args crossed_types depth rt =
@@ -722,6 +880,10 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
args new_crossed_types
(depth + 1) b
in
+ (*i The next call to mk_rel_id is valid since we are constructing the graph
+ Ensures by: obvious
+ i*)
+
let new_t =
mkRApp(mkRVar(mk_rel_id this_relname),args'@[res_rt])
in mkRProd(n,new_t,new_b),
@@ -730,7 +892,7 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
assert false
end
| RApp(_,RRef(_,eq_as_ref),[_;RVar(_,id);rt])
- when eq_as_ref = Lazy.force Coqlib.coq_eq_ref
+ when eq_as_ref = Lazy.force Coqlib.coq_eq_ref && n = Anonymous
->
let is_in_b = is_free_in id b in
let _keep_eq =
@@ -748,9 +910,11 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
(depth + 1) subst_b
in
mkRProd(n,t,new_b),id_to_exclude
-(* if keep_eq then *)
-(* mkRProd(n,t,new_b),id_to_exclude *)
-(* else new_b, Idset.add id id_to_exclude *)
+ (* J.F:. keep this comment it explain how to remove some meaningless equalities
+ if keep_eq then
+ mkRProd(n,t,new_b),id_to_exclude
+ else new_b, Idset.add id id_to_exclude
+ *)
| _ ->
let new_b,id_to_exclude =
rebuild_cons
@@ -766,18 +930,8 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
end
| RLambda(_,n,t,b) ->
begin
-(* let not_free_in_t id = not (is_free_in id t) in *)
-(* let new_crossed_types = t :: crossed_types in *)
-(* let new_b,id_to_exclude = rebuild_cons relname args new_crossed_types b in *)
-(* match n with *)
-(* | Name id when Idset.mem id id_to_exclude -> *)
-(* new_b, *)
-(* Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *)
-(* | _ -> *)
-(* RProd(dummy_loc,n,t,new_b),Idset.filter not_free_in_t id_to_exclude *)
let not_free_in_t id = not (is_free_in id t) in
let new_crossed_types = t :: crossed_types in
-(* let new_b,id_to_exclude = rebuild_cons relname (args new_crossed_types b in *)
match n with
| Name id ->
let new_b,id_to_exclude =
@@ -838,15 +992,24 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
| _ -> mkRApp(mkRVar relname,args@[rt]),Idset.empty
+(* debuging wrapper *)
let rebuild_cons nb_args relname args crossed_types rt =
- observennl (str "rebuild_cons : rt := "++ pr_rawconstr rt ++
- str "nb_args := " ++ str (string_of_int nb_args));
+(* observennl (str "rebuild_cons : rt := "++ pr_rawconstr rt ++ *)
+(* str "nb_args := " ++ str (string_of_int nb_args)); *)
let res =
rebuild_cons nb_args relname args crossed_types 0 rt
in
- observe (str " leads to "++ pr_rawconstr (fst res));
+(* observe (str " leads to "++ pr_rawconstr (fst res)); *)
res
+
+(* naive implementation of parameter detection.
+
+ A parameter is an argument which is only preceded by parameters and whose
+ calls are all syntaxically equal.
+
+ TODO: Find a valid way to deal with implicit arguments here!
+*)
let rec compute_cst_params relnames params = function
| RRef _ | RVar _ | REvar _ | RPatVar _ -> params
| RApp(_,RVar(_,relname'),rtl) when Idset.mem relname' relnames ->
@@ -900,13 +1063,6 @@ let compute_params_name relnames (args : (Names.name * Rawterm.rawconstr * bool)
in
List.rev !l
-(* (Topconstr.CProdN
- (dummy_loc,
- [[(dummy_loc,Anonymous)],returned_types.(i)],
- Topconstr.CSort(dummy_loc, RProp Null )
- )
- )
-*)
let rec rebuild_return_type rt =
match rt with
| Topconstr.CProdN(loc,n,t') ->
@@ -915,36 +1071,58 @@ let rec rebuild_return_type rt =
Topconstr.CArrow(loc,t,rebuild_return_type t')
| Topconstr.CLetIn(loc,na,t,t') ->
Topconstr.CLetIn(loc,na,t,rebuild_return_type t')
- | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc, RProp Null))
+ | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc,RType None))
-let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bool) list list) returned_types (rtl:rawconstr list) =
+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
let funsargs = Array.of_list funsargs in
let returned_types = Array.of_list returned_types in
+ (* alpha_renaming of the body to prevent variable capture during manipulation *)
let rtl_alpha = List.map (function rt -> (alpha_rt [] rt) ) rtl in
let rta = Array.of_list rtl_alpha in
+ (*i The next call to mk_rel_id is valid since we are constructing the graph
+ Ensures by: obvious
+ i*)
let relnames = Array.map mk_rel_id funnames in
let relnames_as_set = Array.fold_right Idset.add relnames Idset.empty in
- let resa = Array.map (build_entry_lc funnames_as_set []) rta in
+ (* Construction of the pseudo constructors *)
+ let env =
+ Array.fold_right
+ (fun id env ->
+ Environ.push_named (id,None,Typing.type_of env Evd.empty (Tacinterp.constr_of_id env id)) env
+ )
+ funnames
+ (Global.env ())
+ in
+ let resa = Array.map (build_entry_lc env funnames_as_set []) rta in
+ (* and of the real constructors*)
let constr i res =
List.map
(function result (* (args',concl') *) ->
let rt = compose_raw_context result.context result.value in
let nb_args = List.length funsargs.(i) in
-(* Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *)
+(* let old_implicit_args = Impargs.is_implicit_args () *)
+(* and old_strict_implicit_args = Impargs.is_strict_implicit_args () *)
+(* and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in *)
+(* let old_rawprint = !Options.raw_print in *)
+(* Options.raw_print := true; *)
+(* Impargs.make_implicit_args false; *)
+(* Impargs.make_strict_implicit_args false; *)
+(* Impargs.make_contextual_implicit_args false; *)
+(* Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *)
+(* 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; *)
fst (
rebuild_cons nb_args relnames.(i)
-(* (List.map *)
-(* (function *)
-(* (Anonymous,_,_) -> mkRVar(fresh_id res.to_avoid "x__") *)
-(* | Name id, _,_ -> mkRVar id *)
-(* ) *)
-(* funsargs.(i) *)
-(* ) *)
[]
[]
rt
@@ -952,15 +1130,21 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo
)
res.result
in
- let next_constructor_id = ref (-1) in
+ (* adding names to constructors *)
+ let next_constructor_id = ref (-1) in
let mk_constructor_id i =
incr next_constructor_id;
+ (*i The next call to mk_rel_id is valid since we are constructing the graph
+ Ensures by: obvious
+ i*)
id_of_string ((string_of_id (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id))
in
let rel_constructors i rt : (identifier*rawconstr) list =
+ next_constructor_id := (-1);
List.map (fun constr -> (mk_constructor_id i),constr) (constr i rt)
in
let rel_constructors = Array.mapi rel_constructors resa in
+ (* Computing the set of parameters if asked *)
let rels_params =
if parametrize
then
@@ -968,12 +1152,12 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo
else []
in
let nrel_params = List.length rels_params in
- let rel_constructors =
+ let rel_constructors = (* Taking into account the parameters in constructors *)
Array.map (List.map
(fun (id,rt) -> (id,snd (chop_rprod_n nrel_params rt))))
rel_constructors
in
- let rel_arity i funargs =
+ let rel_arity i funargs = (* Reduilding arities (with parameters) *)
let rel_first_args :(Names.name * Rawterm.rawconstr * bool ) list =
(snd (list_chop nrel_params funargs))
in
@@ -992,13 +1176,11 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo
)
rel_first_args
(rebuild_return_type returned_types.(i))
-(* (Topconstr.CProdN *)
-(* (dummy_loc, *)
-(* [[(dummy_loc,Anonymous)],returned_types.(i)], *)
-(* Topconstr.CSort(dummy_loc, RProp Null ) *)
-(* ) *)
-(* ) *)
in
+ (* We need to lift back our work topconstr but only with all information
+ We mimick a Set Printing All.
+ Then save the graphs and reset Printing options to their primitive values
+ *)
let rel_arities = Array.mapi rel_arity funsargs in
let old_rawprint = !Options.raw_print in
Options.raw_print := true;
@@ -1017,9 +1199,9 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo
let ext_rels_constructors =
Array.map (List.map
(fun (id,t) ->
- false,((dummy_loc,id),Constrextern.extern_rawtype Idset.empty t)
+ false,((dummy_loc,id),Constrextern.extern_rawtype Idset.empty ((* zeta_normalize *) t))
))
- rel_constructors
+ (rel_constructors)
in
let rel_ind i ext_rel_constructors =
(dummy_loc,relnames.(i)),
@@ -1030,26 +1212,26 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo
in
let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in
let rel_inds = Array.to_list ext_rel_constructors in
- let _ =
- observe (
- str "Inductive" ++ spc () ++
- prlist_with_sep
- (fun () -> fnl ()++spc () ++ str "with" ++ spc ())
- (function ((_,id),_,params,ar,constr) ->
- Ppconstr.pr_id id ++ spc () ++
- Ppconstr.pr_binders params ++ spc () ++
- str ":" ++ spc () ++
- Ppconstr.pr_lconstr_expr ar ++ spc () ++
- prlist_with_sep
- (fun _ -> fnl () ++ spc () ++ str "|" ++ spc ())
- (function (_,((_,id),t)) ->
- Ppconstr.pr_id id ++ spc () ++ str ":" ++ spc () ++
- Ppconstr.pr_lconstr_expr t)
- constr
- )
- rel_inds
- )
- in
+(* let _ = *)
+(* Pp.msgnl (\* observe *\) ( *)
+(* str "Inductive" ++ spc () ++ *)
+(* prlist_with_sep *)
+(* (fun () -> fnl ()++spc () ++ str "with" ++ spc ()) *)
+(* (function ((_,id),_,params,ar,constr) -> *)
+(* Ppconstr.pr_id id ++ spc () ++ *)
+(* Ppconstr.pr_binders params ++ spc () ++ *)
+(* str ":" ++ spc () ++ *)
+(* Ppconstr.pr_lconstr_expr ar ++ spc () ++ str ":=" ++ *)
+(* prlist_with_sep *)
+(* (fun _ -> fnl () ++ spc () ++ str "|" ++ spc ()) *)
+(* (function (_,((_,id),t)) -> *)
+(* Ppconstr.pr_id id ++ spc () ++ str ":" ++ spc () ++ *)
+(* Ppconstr.pr_lconstr_expr t) *)
+(* constr *)
+(* ) *)
+(* rel_inds *)
+(* ) *)
+(* in *)
let old_implicit_args = Impargs.is_implicit_args ()
and old_strict_implicit_args = Impargs.is_strict_implicit_args ()
and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
diff --git a/contrib/funind/rawterm_to_relation.mli b/contrib/funind/rawterm_to_relation.mli
index 0cda56df..9cd04123 100644
--- a/contrib/funind/rawterm_to_relation.mli
+++ b/contrib/funind/rawterm_to_relation.mli
@@ -1,16 +1,16 @@
-(* val new_build_entry_lc : *)
-(* Names.identifier list -> *)
-(* (Names.name*Rawterm.rawconstr) list list -> *)
-(* Topconstr.constr_expr list -> *)
-(* Rawterm.rawconstr list -> *)
-(* unit *)
+
+(*
+ [build_inductive parametrize funnames funargs returned_types bodies]
+ constructs and saves the graphs of the functions [funnames] taking [funargs] as arguments
+ and returning [returned_types] using bodies [bodies]
+*)
val build_inductive :
- bool ->
- Names.identifier list ->
- (Names.name*Rawterm.rawconstr*bool) list list ->
- Topconstr.constr_expr list ->
- Rawterm.rawconstr list ->
+ bool -> (* if true try to detect parameter. Always use it as true except for debug *)
+ Names.identifier list -> (* The list of function name *)
+ (Names.name*Rawterm.rawconstr*bool) list list -> (* The list of function args *)
+ Topconstr.constr_expr list -> (* The list of function returned type *)
+ Rawterm.rawconstr list -> (* the list of body *)
unit
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index c6406468..14805cf4 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -18,7 +18,7 @@ let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl)
let mkRSort s = RSort(dummy_loc,s)
let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous)
-
+let mkRCast(b,t) = RCast(dummy_loc,b,CastCoerce,t)
(*
Some basic functions to decompose rawconstrs
@@ -49,8 +49,8 @@ let raw_decompose_app =
(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *)
-let raw_make_eq t1 t2 =
- mkRApp(mkRRef (Lazy.force Coqlib.coq_eq_ref),[mkRHole ();t2;t1])
+let raw_make_eq ?(typ= mkRHole ()) t1 t2 =
+ mkRApp(mkRRef (Lazy.force Coqlib.coq_eq_ref),[typ;t2;t1])
(* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *)
let raw_make_neq t1 t2 =
@@ -321,7 +321,7 @@ let rec alpha_rt excluded rt =
List.map (alpha_rt excluded) args
)
in
- if Tacinterp.get_debug () <> Tactic_debug.DebugOff && false
+ if Indfun_common.do_observe () && false
then
Pp.msgnl (str "debug: alpha_rt(" ++ str "[" ++
prlist_with_sep (fun _ -> str";") Ppconstr.pr_id excluded ++
@@ -386,30 +386,32 @@ let is_free_in id =
-let rec pattern_to_term = function
+let rec pattern_to_term = function
| PatVar(loc,Anonymous) -> assert false
- | PatVar(loc,Name id) ->
+ | PatVar(loc,Name id) ->
mkRVar id
- | PatCstr(loc,constr,patternl,_) ->
- let cst_narg =
+ | PatCstr(loc,constr,patternl,_) ->
+ let cst_narg =
Inductiveops.mis_constructor_nargs_env
(Global.env ())
constr
in
- let implicit_args =
- Array.to_list
- (Array.init
+ let implicit_args =
+ Array.to_list
+ (Array.init
(cst_narg - List.length patternl)
(fun _ -> mkRHole ())
)
in
- let patl_as_term =
+ let patl_as_term =
List.map pattern_to_term patternl
in
mkRApp(mkRRef(Libnames.ConstructRef constr),
implicit_args@patl_as_term
)
+
+
let replace_var_by_term x_id term =
let rec replace_var_by_pattern rt =
match rt with
@@ -539,3 +541,63 @@ let ids_of_pat =
in
ids_of_pat Idset.empty
+
+
+
+
+let zeta_normalize =
+ let rec zeta_normalize_term rt =
+ match rt with
+ | RRef _ -> rt
+ | RVar _ -> rt
+ | REvar _ -> rt
+ | RPatVar _ -> rt
+ | RApp(loc,rt',rtl) ->
+ RApp(loc,
+ zeta_normalize_term rt',
+ List.map zeta_normalize_term rtl
+ )
+ | RLambda(loc,name,t,b) ->
+ RLambda(loc,
+ name,
+ zeta_normalize_term t,
+ zeta_normalize_term b
+ )
+ | RProd(loc,name,t,b) ->
+ RProd(loc,
+ name,
+ zeta_normalize_term t,
+ zeta_normalize_term b
+ )
+ | RLetIn(_,Name id,def,b) ->
+ zeta_normalize_term (replace_var_by_term id def b)
+ | RLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b
+ | RLetTuple(loc,nal,(na,rto),def,b) ->
+ RLetTuple(loc,
+ nal,
+ (na,option_map zeta_normalize_term rto),
+ zeta_normalize_term def,
+ zeta_normalize_term b
+ )
+ | RCases(loc,infos,el,brl) ->
+ RCases(loc,
+ infos,
+ List.map (fun (e,x) -> (zeta_normalize_term e,x)) el,
+ List.map zeta_normalize_br brl
+ )
+ | RIf(loc,b,(na,e_option),lhs,rhs) ->
+ RIf(loc, zeta_normalize_term b,
+ (na,option_map zeta_normalize_term e_option),
+ zeta_normalize_term lhs,
+ zeta_normalize_term rhs
+ )
+ | RRec _ -> raise (UserError("",str "Not handled RRec"))
+ | RSort _ -> rt
+ | RHole _ -> rt
+ | RCast(loc,b,k,t) ->
+ RCast(loc,zeta_normalize_term b,k,zeta_normalize_term t)
+ | RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
+ and zeta_normalize_br (loc,idl,patl,res) =
+ (loc,idl,patl,zeta_normalize_term res)
+ in
+ zeta_normalize_term
diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli
index 5dcdb15c..aa355485 100644
--- a/contrib/funind/rawtermops.mli
+++ b/contrib/funind/rawtermops.mli
@@ -25,7 +25,7 @@ val mkRLetIn : Names.name*rawconstr*rawconstr -> 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 *)
-
+val mkRCast : rawconstr* rawconstr -> rawconstr
(*
Some basic functions to decompose rawconstrs
These are analogous to the ones constrs
@@ -36,7 +36,7 @@ val raw_decompose_app : rawconstr -> rawconstr*(rawconstr list)
(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *)
-val raw_make_eq : rawconstr -> rawconstr -> rawconstr
+val raw_make_eq : ?typ:rawconstr -> rawconstr -> rawconstr -> rawconstr
(* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *)
val raw_make_neq : rawconstr -> rawconstr -> rawconstr
(* [raw_make_or P1 P2] build the rawconstr corresponding to [P1 \/ P2] *)
@@ -106,3 +106,9 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool
returns the set of variables appearing in a pattern
*)
val ids_of_pat : cases_pattern -> Names.Idset.t
+
+
+(*
+ removing let_in construction in a rawterm
+*)
+val zeta_normalize : Rawterm.rawconstr -> Rawterm.rawconstr
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index 2c7e4d33..5d19079b 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -1,16 +1,10 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
(*s FunInv Tactic: inversion following the shape of a function. *)
-(* Use:
- \begin{itemize}
- \item The Tacinv directory must be in the path (-I <path> option)
- \item use the bytecode version of coqtop or coqc (-byte option), or make a
- coqtop
- \item Do [Require Tacinv] to be able to use it.
- \item For syntax see Tacinv.v
- \end{itemize}
-*)
+(* Deprecated: see indfun_main.ml4 instead *)
+
+(* Don't delete this file yet, it may be used for other purposes *)
(*i*)
open Termops
@@ -862,7 +856,6 @@ END
(*
*** Local Variables: ***
*** compile-command: "make -C ../.. contrib/funind/tacinv.cmo" ***
-*** tab-width: 1 ***
*** tuareg-default-indent:1 ***
*** tuareg-begin-indent:1 ***
*** tuareg-let-indent:1 ***
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index ecb04e07..024cb599 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -336,8 +336,8 @@ and
| a::l -> CT_match_pattern_ne_list(xlate_match_pattern a,
List.map xlate_match_pattern l)
and translate_one_equation = function
- (_,lp, a) -> CT_eqn ( xlate_match_pattern_ne_list lp,
- xlate_formula a)
+ (_,[lp], a) -> CT_eqn (xlate_match_pattern_ne_list lp, xlate_formula a)
+ | _ -> xlate_error "TODO: disjunctive multiple patterns"
and
xlate_binder_ne_list = function
[] -> assert false
@@ -978,7 +978,7 @@ and xlate_tac =
let id_opt =
match out_gen Extratactics.rawwit_in_arg_hyp id_opt with
| None -> ctv_ID_OPT_NONE
- | Some id -> ctf_ID_OPT_SOME (xlate_ident id)
+ | Some (_,id) -> ctf_ID_OPT_SOME (xlate_ident id)
in
let tac_opt =
match out_gen (Extratactics.rawwit_by_arg_tac) tac_opt with
@@ -2035,7 +2035,6 @@ let rec xlate_vernac =
| VernacExtend (s, l) ->
CT_user_vernac
(CT_ident s, CT_varg_list (List.map coerce_genarg_to_VARG l))
- | VernacDebug b -> xlate_error "Debug On/Off not supported"
| VernacList((_, a)::l) ->
CT_coerce_COMMAND_LIST_to_COMMAND
(CT_command_list(xlate_vernac a,
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index 2aa3516f..83ea5b63 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -49,6 +49,11 @@ Inductive term : Set :=
| Tvar : nat -> term.
Delimit Scope romega_scope with term.
+Arguments Scope Tplus [romega_scope romega_scope].
+Arguments Scope Tmult [romega_scope romega_scope].
+Arguments Scope Tminus [romega_scope romega_scope].
+Arguments Scope Topp [romega_scope romega_scope].
+
Infix "+" := Tplus : romega_scope.
Infix "*" := Tmult : romega_scope.
Infix "-" := Tminus : romega_scope.
diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v
index bbf722db..ded069bf 100644
--- a/contrib/subtac/FixSub.v
+++ b/contrib/subtac/FixSub.v
@@ -20,3 +20,27 @@ Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
End FixPoint.
End Well_founded.
+
+Require Import Wf_nat.
+Require Import Lt.
+
+Section Well_founded_measure.
+Variable A : Set.
+Variable f : A -> nat.
+Definition R := fun x y => f x < f y.
+
+Section FixPoint.
+
+Variable P : A -> Set.
+
+Variable F_sub : forall x:A, (forall y: { y : A | f y < f x }, P (proj1_sig y)) -> P x.
+
+Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (f x)) {struct r} : P x :=
+ F_sub x (fun y: { y : A | f y < f x} => Fix_measure_F_sub (proj1_sig y)
+ (Acc_inv r (f (proj1_sig y)) (proj2_sig y))).
+
+Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (f x)).
+
+End FixPoint.
+
+End Well_founded_measure.
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index db10cb2a..b1694d7c 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -34,3 +34,13 @@ induction t.
simpl ; auto.
Qed.
+Ltac destruct_one_pair :=
+ match goal with
+ | [H : (ex _) |- _] => destruct H
+ | [H : (ex2 _) |- _] => destruct H
+ | [H : (sig _) |- _] => destruct H
+ | [H : (_ /\ _) |- _] => destruct H
+end.
+
+Ltac destruct_exists := repeat (destruct_one_pair) .
+
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 382ae2d5..859f9013 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -16,7 +16,7 @@ let reverse_array arr =
Array.of_list (List.rev (Array.to_list arr))
let trace s =
- if !Options.debug then msgnl s
+ if !Options.debug then (msgnl s; msgerr s)
else ()
(** Utilities to find indices in lists *)
@@ -37,7 +37,9 @@ let list_assoc_index x l =
let subst_evars evs n t =
let evar_info id =
let rec aux i = function
- (k, h, v) :: tl -> if k = id then (i, h, v) else aux (succ i) tl
+ (k, h, v) :: tl ->
+ trace (str "Searching for " ++ int id ++ str " found: " ++ int k);
+ if k = id then (i, h, v) else aux (succ i) tl
| [] -> raise Not_found
in
let (idx, hyps, v) = aux 0 evs in
@@ -45,29 +47,29 @@ let subst_evars evs n t =
in
let rec substrec depth c = match kind_of_term c with
| Evar (k, args) ->
- (try
- let index, hyps = evar_info k in
- (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
- int (List.length hyps) ++ str " hypotheses"); with _ -> () );
-
- let ex = mkRel (index + depth) in
- (* Evar arguments are created in inverse order,
- and we must not apply to defined ones (i.e. LetIn's)
- *)
- let args =
- let rec aux hyps args acc =
- match hyps, args with
- ((_, None, _) :: tlh), (c :: tla) ->
- aux tlh tla ((map_constr_with_binders succ substrec depth c) :: acc)
- | ((_, Some _, _) :: tlh), (_ :: tla) ->
- aux tlh tla acc
- | [], [] -> acc
- | _, _ -> failwith "subst_evars: invalid argument"
- in aux hyps (Array.to_list args) []
- in
- mkApp (ex, Array.of_list args)
- with Not_found ->
- anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found"))
+ (let index, hyps =
+ try evar_info k
+ with Not_found ->
+ anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
+ in
+ (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
+ int (List.length hyps) ++ str " hypotheses"); with _ -> () );
+ let ex = mkRel (index + depth) in
+ (* Evar arguments are created in inverse order,
+ and we must not apply to defined ones (i.e. LetIn's)
+ *)
+ let args =
+ let rec aux hyps args acc =
+ match hyps, args with
+ ((_, None, _) :: tlh), (c :: tla) ->
+ aux tlh tla ((map_constr_with_binders succ substrec depth c) :: acc)
+ | ((_, Some _, _) :: tlh), (_ :: tla) ->
+ aux tlh tla acc
+ | [], [] -> acc
+ | _, _ -> failwith "subst_evars: invalid argument"
+ in aux hyps (Array.to_list args) []
+ in
+ mkApp (ex, Array.of_list args))
| _ -> map_constr_with_binders succ substrec depth c
in
substrec 0 t
@@ -106,11 +108,13 @@ open Tacticals
let eterm_term evm t tycon =
(* 'Serialize' the evars, we assume that the types of the existentials
refer to previous existentials in the list only *)
- let evl = to_list evm in
+ let evl = List.rev (to_list evm) in
+ trace (str "Eterm, transformed to list");
let evts =
(* Remove existential variables in types and build the corresponding products *)
fold_right
(fun (id, ev) l ->
+ trace (str "Eterm: " ++ str "treating evar: " ++ int id);
let hyps = Environ.named_context_of_val ev.evar_hyps in
let y' = (id, hyps, etype_of_evar l ev hyps) in
y' :: l)
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index cd2e7c43..ffb16a19 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac.ml 8889 2006-06-01 20:23:56Z msozeau $ *)
+(* $Id: subtac.ml 8964 2006-06-20 13:52:21Z msozeau $ *)
open Global
open Pp
@@ -43,7 +43,7 @@ open Eterm
let require_library dirpath =
let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
Library.require_library [qualid] None
-
+(*
let subtac_one_fixpoint env isevars (f, decl) =
let ((id, n, bl, typ, body), decl) =
Subtac_interp_fixpoint.rewrite_fixpoint env [] (f, decl)
@@ -53,7 +53,7 @@ let subtac_one_fixpoint env isevars (f, decl) =
Ppconstr.pr_constr_expr body)
with _ -> ()
in ((id, n, bl, typ, body), decl)
-
+*)
let subtac_fixpoint isevars l =
(* TODO: Copy command.build_recursive *)
diff --git a/contrib/subtac/subtac.mli b/contrib/subtac/subtac.mli
index a0d2fb2b..25922782 100644
--- a/contrib/subtac/subtac.mli
+++ b/contrib/subtac/subtac.mli
@@ -1,14 +1,3 @@
val require_library : string -> unit
-val subtac_one_fixpoint :
- 'a ->
- 'b ->
- (Names.identifier * (int * Topconstr.recursion_order_expr) *
- Topconstr.local_binder list * Topconstr.constr_expr *
- Topconstr.constr_expr) *
- 'c ->
- (Names.identifier * (int * Topconstr.recursion_order_expr) *
- Topconstr.local_binder list * Topconstr.constr_expr *
- Topconstr.constr_expr) *
- 'c
val subtac_fixpoint : 'a -> 'b -> unit
val subtac : Util.loc * Vernacexpr.vernac_expr -> unit
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 7428e1ed..78c3c70b 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac_coercion.ml 8889 2006-06-01 20:23:56Z msozeau $ *)
+(* $Id: subtac_coercion.ml 8964 2006-06-20 13:52:21Z msozeau $ *)
open Util
open Names
@@ -106,25 +106,25 @@ module Coercion = struct
: (Term.constr -> Term.constr) option
=
let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in
- (try trace (str "Coerce called for " ++ (my_print_constr env x) ++
+ (try debug 1 (str "Coerce called for " ++ (my_print_constr env x) ++
str " and "++ my_print_constr env y ++
str " with evars: " ++ spc () ++
my_print_evardefs !isevars);
with _ -> ());
let rec coerce_unify env x y =
- (try trace (str "coerce_unify from " ++ (my_print_constr env x) ++
+ (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++
str " to "++ my_print_constr env y)
with _ -> ());
try
isevars := the_conv_x_leq env x y !isevars;
- (try (trace (str "Unified " ++ (my_print_constr env x) ++
- str " and "++ my_print_constr env y));
+ (try debug 1 (str "Unified " ++ (my_print_constr env x) ++
+ str " and "++ my_print_constr env y);
with _ -> ());
None
with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars y)
and coerce' env x y : (Term.constr -> Term.constr) option =
let subco () = subset_coerce env isevars x y in
- (try trace (str "coerce' from " ++ (my_print_constr env x) ++
+ (try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++
str " to "++ my_print_constr env y);
with _ -> ());
match (kind_of_term x, kind_of_term y) with
@@ -370,7 +370,7 @@ module Coercion = struct
let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
(try
- trace (str "inh_conv_coerce_to_fail called for " ++
+ debug 1 (str "inh_conv_coerce_to_fail called for " ++
Termops.print_constr_env env t ++ str " and "++ spc () ++
Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++
Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
@@ -436,7 +436,7 @@ module Coercion = struct
(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
let inh_conv_coerce_to loc env isevars cj ((n, t) as tycon) =
(try
- trace (str "Subtac_coercion.inh_conv_coerce_to called for " ++
+ debug 1 (str "Subtac_coercion.inh_conv_coerce_to called for " ++
Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++
Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
@@ -461,7 +461,7 @@ module Coercion = struct
let inh_conv_coerces_to loc env isevars t ((abs, t') as tycon) =
(try
- trace (str "Subtac_coercion.inh_conv_coerces_to called for " ++
+ debug 1 (str "Subtac_coercion.inh_conv_coerces_to called for " ++
Termops.print_constr_env env t ++ str " and "++ spc () ++
Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index b09228c0..c738d7a6 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -117,7 +117,8 @@ let interp_context sigma env params =
let list_chop_hd i l = match list_chop i l with
| (l1,x::l2) -> (l1,x,l2)
- | _ -> assert false
+ | (x :: [], l2) -> ([], x, [])
+ | _ -> assert(false)
let collect_non_rec env =
let rec searchrec lnonrec lnamerec ldefrec larrec nrec =
@@ -173,82 +174,189 @@ let list_of_local_binders l =
| [] -> List.rev acc
in aux [] l
-let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
+let lift_binders k n l =
+ let rec aux n = function
+ | (id, t, c) :: tl -> (id, option_map (liftn k n) t, liftn k n c) :: aux (pred n) tl
+ | [] -> []
+ in aux n l
+
+let rec gen_rels = function
+ 0 -> []
+ | n -> mkRel n :: gen_rels (pred n)
+
+let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
+ let sigma = Evd.empty in
+ let isevars = ref (Evd.create_evar_defs sigma) in
+ let env = Global.env() in
+ let pr c = my_print_constr env c in
+ let prr = Printer.pr_rel_context env in
+ let pr_rel env = Printer.pr_rel_context env in
+ let _ =
+ try debug 2 (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++
+ Ppconstr.pr_binders bl ++ str " : " ++
+ Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
+ Ppconstr.pr_constr_expr body)
+ with _ -> ()
+ in
+ let env', binders_rel = interp_context isevars env bl in
+ let after, ((argname, _, argtyp) as arg), before = list_chop_hd (succ n) binders_rel in
+ let before_length, after_length = List.length before, List.length after in
+ let argid = match argname with Name n -> n | _ -> assert(false) in
+ let _liftafter = lift_binders 1 after_length after in
+ let envwf = push_rel_context before env in
+ let wf_rel, measure_fn =
+ let rconstr = interp_constr isevars envwf r in
+ if measure then
+ let lt_rel = constr_of_global (Lazy.force lt_ref) in
+ let name s = Name (id_of_string s) in
+ mkLambda (name "x", argtyp,
+ mkLambda (name "y", argtyp,
+ mkApp (lt_rel,
+ [| mkApp (rconstr, [| mkRel 2 |]) ;
+ mkApp (rconstr, [| mkRel 1 |]) |]))),
+ Some rconstr
+ else rconstr, None
+ in
+ let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |])
+ in
+ let argid' = id_of_string (string_of_id argid ^ "'") in
+ let wfarg len = (Name argid', None,
+ mkSubset (Name argid') argtyp
+ (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|])))
+ in
+ let top_bl = after @ (arg :: before) in
+ let intern_bl = after @ (wfarg 1 :: arg :: before) in
+ let top_env = push_rel_context top_bl env in
+ let intern_env = push_rel_context intern_bl env in
+ let top_arity = interp_type isevars top_env arityc in
+ (try debug 2 (str "Intern bl: " ++ prr intern_bl) with _ -> ());
+ let proj = (Lazy.force sig_).Coqlib.proj1 in
+ let projection =
+ mkApp (proj, [| argtyp ;
+ (mkLambda (Name argid', argtyp,
+ (mkApp (wf_rel, [|mkRel 1; mkRel 3|])))) ;
+ mkRel 1
+ |])
+ in
+ (try debug 2 (str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ());
+ let intern_arity = substnl [projection] after_length top_arity in
+ (try debug 2 (str "Top arity after subst: " ++ my_print_constr intern_env intern_arity) with _ -> ());
+ let intern_before_env = push_rel_context before env in
+ let intern_fun_bl = after @ [wfarg 1] in
+ (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ());
+ let intern_fun_arity = intern_arity in
+ (try debug 2 (str "Intern fun arity: " ++
+ my_print_constr intern_env intern_fun_arity) with _ -> ());
+ let intern_fun_arity_prod = it_mkProd_or_LetIn intern_fun_arity intern_fun_bl in
+ let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in
+ let fun_bl = after @ (intern_fun_binder :: [arg]) in
+ (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ());
+ let fun_env = push_rel_context fun_bl intern_before_env in
+ let fun_arity = interp_type isevars fun_env arityc in
+ let intern_body = interp_casted_constr isevars fun_env body fun_arity in
+ let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in
+ let _ =
+ try debug 2 (str "Fun bl: " ++ prr fun_bl ++ spc () ++
+ str "Intern bl" ++ prr intern_bl ++ spc () ++
+ str "Top bl" ++ prr top_bl ++ spc () ++
+ str "Intern arity: " ++ pr intern_arity ++
+ str "Top arity: " ++ pr top_arity ++ spc () ++
+ str "Intern body " ++ pr intern_body_lam)
+ with _ -> ()
+ in
+ let _impl =
+ if Impargs.is_implicit_args()
+ then Impargs.compute_implicits top_env top_arity
+ else []
+ in
+ let prop = mkLambda (Name argid, argtyp, it_mkProd_or_LetIn top_arity after) in
+ let fix_def =
+ match measure_fn with
+ None ->
+ mkApp (constr_of_reference (Lazy.force fix_sub_ref),
+ [| argtyp ;
+ wf_rel ;
+ make_existential dummy_loc intern_before_env isevars wf_proof ;
+ prop ;
+ intern_body_lam |])
+ | Some f ->
+ mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref),
+ [| argtyp ; f ; prop ;
+ intern_body_lam |])
+ in
+ let def_appl = applist (fix_def, gen_rels (after_length + 1)) in
+ let def = it_mkLambda_or_LetIn def_appl binders_rel in
+ let typ = it_mkProd_or_LetIn top_arity binders_rel in
+ debug 2 (str "Constructed def");
+ debug 2 (my_print_constr intern_before_env def);
+ debug 2 (str "Type: " ++ my_print_constr env typ);
+ let fullcoqc = Evarutil.nf_isevar !isevars def in
+ let fullctyp = Evarutil.nf_isevar !isevars typ in
+ let _ = try trace (str "After evar normalization: " ++ spc () ++
+ str "Coq term: " ++ my_print_constr env fullcoqc ++ spc ()
+ ++ str "Coq type: " ++ my_print_constr env fullctyp)
+ with _ -> ()
+ in
+ let evm = non_instanciated_map env isevars in
+ let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in
+ let evars_def, evars_typ, evars = Eterm.eterm_term evm fullcoqc (Some fullctyp) in
+ let evars_typ = out_some evars_typ in
+ (try trace (str "Building evars sum for : ");
+ List.iter
+ (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t))
+ evars;
+ with _ -> ());
+ let (sum_tac, sumg) = Subtac_utils.build_dependent_sum evars in
+ (try trace (str "Evars sum: " ++ my_print_constr env sumg);
+ trace (str "Evars type: " ++ my_print_constr env evars_typ);
+ with _ -> ());
+ let proofid = id_of_string (string_of_id recname ^ "_evars_proof") in
+ Command.start_proof proofid goal_proof_kind sumg
+ (fun strength gr ->
+ debug 2 (str "Proof finished");
+ let def = constr_of_global gr in
+ let args = Subtac_utils.destruct_ex def sumg in
+ let _, newdef = decompose_lam_n (List.length args) evars_def in
+ let constr = Term.substl (List.rev args) newdef in
+ debug 2 (str "Applied existentials : " ++ my_print_constr env constr);
+ let ce =
+ { const_entry_body = constr;
+ const_entry_type = Some fullctyp;
+ const_entry_opaque = false;
+ const_entry_boxed = boxed}
+ in
+ let _constant = Declare.declare_constant
+ recname (DefinitionEntry ce,IsDefinition Definition)
+ in
+ definition_message recname);
+ trace (str "Started existentials proof");
+ Pfedit.by sum_tac;
+ trace (str "Applied sum tac")
+
+let build_mutrec l boxed =
let sigma = Evd.empty
and env0 = Global.env()
in
let lnameargsardef =
(*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))*)
- lnameargsardef
+ l
in
let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef
and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef
in
- (* Build the recursive context and notations for the recursive types *)
+ (* Build the recursive context and notations for the recursive types *)
let (rec_sign,rec_impls,arityl) =
List.fold_left
- (fun (env,impls,arl) ((recname,(n, ro),bl,arityc,body),_) ->
- let isevars = ref (Evd.create_evar_defs sigma) in
- match ro with
- CStructRec ->
- let arityc = Command.generalize_constr_expr arityc bl in
- let arity = interp_type isevars env0 arityc in
- let impl =
- if Impargs.is_implicit_args()
- then Impargs.compute_implicits env0 arity
- else [] in
- let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
- (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl)
- | CWfRec r ->
- let n = out_some n in
- let _ =
- try trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++
- Ppconstr.pr_binders bl ++ str " : " ++
- Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
- Ppconstr.pr_constr_expr body)
- with _ -> ()
- in
- let env', binders_rel = interp_context isevars env0 bl in
- let after, ((argname, _, argtyp) as arg), before = list_chop_hd n binders_rel in
- let argid = match argname with Name n -> n | _ -> assert(false) in
- let after' = List.map (fun (n, c, t) -> (n, option_map (lift 1) c, lift 1 t)) after in
- let envwf = push_rel_context before env0 in
- let wf_rel = interp_constr isevars envwf r in
- let accarg_id = id_of_string ("Acc_" ^ string_of_id argid) in
- let accarg = (Name accarg_id, None, mkApp (Lazy.force acc_inv, [| argtyp; wf_rel; mkRel 1 |])) in
- let argid' = id_of_string (string_of_id argid ^ "'") in
- let before_length, after_length = List.length before, List.length after in
- let full_length = before_length + 1 + after_length in
- let wfarg len = (Name argid, None,
- mkSubset (Name argid') argtyp
- (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|])))
- in
- let new_bl = after' @ (accarg :: arg :: before)
- and intern_bl = after @ (wfarg (before_length + 1) :: before)
- in
- let intern_env = push_rel_context intern_bl env0 in
- let env' = push_rel_context new_bl env0 in
- let arity = interp_type isevars intern_env arityc in
- let intern_arity = it_mkProd_or_LetIn arity intern_bl in
- let arity' = interp_type isevars env' arityc in
- let arity' = it_mkProd_or_LetIn arity' new_bl in
- let fun_bl = after @ ((Name recname, None, intern_arity) :: arg :: before) in
- let _ =
- let pr c = my_print_constr env c in
- let prr = Printer.pr_rel_context env in
- try trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++
- str "Intern bl" ++ prr intern_bl ++ spc () ++
- str "Extern bl" ++ prr new_bl ++ spc () ++
- str "Intern arity: " ++ pr intern_arity)
- with _ -> ()
- in
- let impl =
- if Impargs.is_implicit_args()
- then Impargs.compute_implicits intern_env arity'
- else [] in
- let impls' = (recname,([],impl,compute_arguments_scope arity'))::impls in
- (Environ.push_named (recname,None,arity') env, impls',
- (isevars, Some (full_length - n, argtyp, wf_rel, fun_bl, intern_bl, intern_arity), arity')::arl))
+ (fun (env,impls,arl) ((recname, n, bl,arityc,body),_) ->
+ let isevars = ref (Evd.create_evar_defs sigma) in
+ let arityc = Command.generalize_constr_expr arityc bl in
+ let arity = interp_type isevars env0 arityc in
+ let impl =
+ if Impargs.is_implicit_args()
+ then Impargs.compute_implicits env0 arity
+ else [] in
+ let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
+ (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl))
(env0,[],[]) lnameargsardef in
let arityl = List.rev arityl in
let notations =
@@ -283,7 +391,6 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
let (lnonrec,(namerec,defrec,arrec,nvrec)) =
collect_non_rec env0 lrecnames recdef arityl nv in
- let nvrec' = Array.map (function (Some n,_) -> n | _ -> 0) nvrec in(* ignore rec order *)
let declare arrec defrec =
let recvec =
Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
@@ -293,7 +400,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
my_print_constr env0 (recvec.(i)));
with _ -> ());
let ce =
- { const_entry_body = mkFix ((nvrec',i),recdecls);
+ { const_entry_body = mkFix ((nvrec,i),recdecls);
const_entry_type = Some arrec.(i);
const_entry_opaque = false;
const_entry_boxed = boxed} in
@@ -384,6 +491,11 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
match sum with Some (sumtac, sumg) -> Some (id, kn, sumg, sumtac) | None -> None)
defs
in
+ match real_evars with
+ [] -> declare (List.rev_map (fun (id, c, _) ->
+ snd (decompose_lam_n recdefs c)) defs)
+ | l ->
+
Subtac_utils.and_tac real_evars
(fun f _ gr ->
let _ = trace (str "Got a proof of: " ++ pr_global gr ++
@@ -431,5 +543,28 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
Environ.NoBody -> trace (str "Constant has no body")
| Environ.Opaque -> trace (str "Constant is opaque")
)
+
+let out_n = function
+ Some n -> n
+ | None -> 0
+
+let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
+ match lnameargsardef with
+ | ((id, (n, CWfRec r), bl, typ, body), no) :: [] ->
+ build_wellfounded (id, out_n n, bl, typ, body) r false no boxed
+ | ((id, (n, CMeasureRec r), bl, typ, body), no) :: [] ->
+ build_wellfounded (id, out_n n, bl, typ, body) r true no boxed
+ | l ->
+ let lnameargsardef =
+ List.map (fun ((id, (n, ro), bl, typ, body), no) ->
+ match ro with
+ CStructRec -> (id, out_n n, bl, typ, body), no
+ | CWfRec _ | CMeasureRec _ ->
+ errorlabstrm "Subtac_command.build_recursive"
+ (str "Well-founded fixpoints not allowed in mutually recursive blocks"))
+ lnameargsardef
+ in
+ build_mutrec lnameargsardef boxed;
+ assert(false)
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
index e1bbbbb5..90ffb892 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/contrib/subtac/subtac_command.mli
@@ -38,5 +38,6 @@ val interp_constr_judgment :
constr_expr -> unsafe_judgment
val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
val recursive_message : global_reference array -> std_ppcmds
+
val build_recursive :
(fixpoint_expr * decl_notation) list -> bool -> unit
diff --git a/contrib/subtac/subtac_interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml
index 858fad1a..bb35833f 100644
--- a/contrib/subtac/subtac_interp_fixpoint.ml
+++ b/contrib/subtac/subtac_interp_fixpoint.ml
@@ -60,7 +60,7 @@ let pr_binder_list b =
let rec rewrite_rec_calls l c = c
-
+(*
let rewrite_fixpoint env l (f, decl) =
let (id, (n, ro), bl, typ, body) = f in
let body = rewrite_rec_calls l body in
@@ -151,3 +151,4 @@ let rewrite_fixpoint env l (f, decl) =
Ppconstr.pr_constr_expr body')
in (id, (succ n, ro), bl', typ, body'), decl
+*)
diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli
index fafbb2da..149e7580 100644
--- a/contrib/subtac/subtac_interp_fixpoint.mli
+++ b/contrib/subtac/subtac_interp_fixpoint.mli
@@ -15,14 +15,3 @@ val list_of_local_binders :
val pr_binder_list :
(('a * Names.name) * Topconstr.constr_expr) list -> Pp.std_ppcmds
val rewrite_rec_calls : 'a -> 'b -> 'b
-val rewrite_fixpoint :
- 'a ->
- 'b ->
- (Names.identifier * (int * Topconstr.recursion_order_expr) *
- Topconstr.local_binder list * Topconstr.constr_expr *
- Topconstr.constr_expr) *
- 'c ->
- (Names.identifier * (int * Topconstr.recursion_order_expr) *
- Topconstr.local_binder list * Topconstr.constr_expr *
- Topconstr.constr_expr) *
- 'c
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 59c858a6..d4db7c27 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -22,12 +22,16 @@ let fixsub = lazy (init_constant fixsub_module "Fix_sub")
let ex_pi1 = lazy (init_constant utils_module "ex_pi1")
let ex_pi2 = lazy (init_constant utils_module "ex_pi2")
-let make_ref s = Qualid (dummy_loc, (qualid_of_string s))
-let well_founded_ref = make_ref "Init.Wf.Well_founded"
-let acc_ref = make_ref "Init.Wf.Acc"
-let acc_inv_ref = make_ref "Init.Wf.Acc_inv"
-let fix_sub_ref = make_ref "Coq.subtac.FixSub.Fix_sub"
-let lt_wf_ref = make_ref "Coq.Wf_nat.lt_wf"
+let make_ref l s = lazy (init_reference l s)
+let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
+let acc_ref = make_ref ["Init";"Wf"] "Acc"
+let acc_inv_ref = make_ref ["Init";"Wf"] "Acc_inv"
+let fix_sub_ref = make_ref ["subtac";"FixSub"] "Fix_sub"
+let fix_measure_sub_ref = make_ref ["subtac";"FixSub"] "Fix_measure_sub"
+let lt_ref = make_ref ["Init";"Peano"] "lt"
+let lt_wf_ref = make_ref ["Wf_nat"] "lt_wf"
+
+let make_ref s = Qualid (dummy_loc, qualid_of_string s)
let sig_ref = make_ref "Init.Specif.sig"
let proj1_sig_ref = make_ref "Init.Specif.proj1_sig"
let proj2_sig_ref = make_ref "Init.Specif.proj2_sig"
@@ -82,18 +86,19 @@ let my_print_evardefs = Evd.pr_evar_defs
let my_print_tycon_type = Evarutil.pr_tycon_type
+let debug_level = 2
let debug n s =
- if !Options.debug then
+ if !Options.debug && n >= debug_level then
msgnl s
else ()
let debug_msg n s =
- if !Options.debug then s
+ if !Options.debug && n >= debug_level then s
else mt ()
let trace s =
- if !Options.debug then msgnl s
+ if !Options.debug && debug_level > 0 then msgnl s
else ()
let wf_relations = Hashtbl.create 10
@@ -153,6 +158,9 @@ let non_instanciated_map env evd =
let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
+let global_proof_kind = Decl_kinds.IsProof Decl_kinds.Lemma
+let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma
+
let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint
let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint
@@ -164,7 +172,7 @@ let build_dependent_sum l =
(n, t) :: tl ->
let t' = mkLambda (Name n, t, typ) in
trace (spc () ++ str ("treating evar " ^ string_of_id n));
- (try trace (str " assert: " ++ my_print_constr (Global.env ()) t)
+ (try trace (str " assert: " ++ my_print_constr (Global.env ()) t)
with _ -> ());
let tac' =
tclTHENS (assert_tac true (Name n) t)
@@ -183,6 +191,39 @@ let build_dependent_sum l =
(_, hd) :: tl -> aux (intros, hd) tl
| [] -> raise (Invalid_argument "build_dependent_sum")
+let id x = x
+
+let build_dependent_sum l =
+ let rec aux names conttac conttype = function
+ (n, t) :: ((_ :: _) as tl) ->
+ let hyptype = substl names t in
+ trace (spc () ++ str ("treating evar " ^ string_of_id n));
+ (try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype)
+ with _ -> ());
+ let tac = assert_tac true (Name n) hyptype in
+ let conttac =
+ (fun cont ->
+ conttac
+ (tclTHENS tac
+ ([intros;
+ (tclTHENSEQ
+ [constructor_tac (Some 1) 1
+ (Rawterm.ImplicitBindings [mkVar n]);
+ cont]);
+ ])))
+ in
+ let conttype =
+ (fun typ ->
+ let tex = mkLambda (Name n, t, typ) in
+ conttype
+ (mkApp (Lazy.force ex_ind, [| t; tex |])))
+ in
+ aux (mkVar n :: names) conttac conttype tl
+ | (n, t) :: [] ->
+ (conttac intros, conttype t)
+ | [] -> raise (Invalid_argument "build_dependent_sum")
+ in aux [] id id (List.rev l)
+
open Proof_type
open Tacexpr
@@ -251,6 +292,75 @@ let destruct_ex ext ex =
| _ -> [acc]
in aux ex ext
+open Rawterm
+
+
+let list_mapi f =
+ let rec aux i = function
+ hd :: tl -> f i hd :: aux (succ i) tl
+ | [] -> []
+ in aux 0
+
+let rewrite_cases_aux (loc, po, tml, eqns) =
+ let tml = list_mapi (fun i (c, (n, opt)) -> c,
+ ((match n with
+ Name id -> (match c with
+ | RVar (_, id') when id = id' ->
+ Name (id_of_string (string_of_id id ^ "'"))
+ | _ -> n)
+ | Anonymous -> Name (id_of_string ("x" ^ string_of_int i))),
+ opt)) tml
+ in
+ let mkHole = RHole (dummy_loc, InternalHole) in
+ let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)),
+ [mkHole; c; n])
+ in
+ let eqs_types =
+ List.map
+ (fun (c, (n, _)) ->
+ let id = match n with Name id -> id | _ -> assert false in
+ let heqid = id_of_string ("Heq" ^ string_of_id id) in
+ Name heqid, mkeq c (RVar (dummy_loc, id)))
+ tml
+ in
+ let po =
+ List.fold_right
+ (fun (n,t) acc ->
+ RProd (dummy_loc, Anonymous, t, acc))
+ eqs_types (match po with
+ Some e -> e
+ | None -> mkHole)
+ in
+ let eqns =
+ List.map (fun (loc, idl, cpl, c) ->
+ let c' =
+ List.fold_left
+ (fun acc (n, t) ->
+ RLambda (dummy_loc, n, mkHole, acc))
+ c eqs_types
+ in (loc, idl, cpl, c'))
+ eqns
+ in
+ let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref),
+ [mkHole; c])
+ in
+ let refls = List.map (fun (c, _) -> mk_refl_equal c) tml in
+ let case = RCases (loc,Some po,tml,eqns) in
+ let app = RApp (dummy_loc, case, refls) in
+ app
+
+let rec rewrite_cases c =
+ match c with
+ RCases _ -> let c' = map_rawconstr rewrite_cases c in
+ (match c' with
+ | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w)
+ | _ -> assert(false))
+ | _ -> map_rawconstr rewrite_cases c
+
+let rewrite_cases env c =
+ let c' = rewrite_cases c in
+ let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in
+ c'
let list_mapi f =
let rec aux i = function
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index a90f281f..4a7e8177 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -18,12 +18,13 @@ val fixsub_module : string list
val init_constant : string list -> string -> constr
val init_reference : string list -> string -> global_reference
val fixsub : constr lazy_t
-val make_ref : string -> reference
-val well_founded_ref : reference
-val acc_ref : reference
-val acc_inv_ref : reference
-val fix_sub_ref : reference
-val lt_wf_ref : reference
+val well_founded_ref : global_reference lazy_t
+val acc_ref : global_reference lazy_t
+val acc_inv_ref : global_reference lazy_t
+val fix_sub_ref : global_reference lazy_t
+val fix_measure_sub_ref : global_reference lazy_t
+val lt_ref : global_reference lazy_t
+val lt_wf_ref : global_reference lazy_t
val sig_ref : reference
val proj1_sig_ref : reference
val proj2_sig_ref : reference
@@ -69,6 +70,8 @@ val string_of_hole_kind : hole_kind -> string
val non_instanciated_map : env -> evar_defs ref -> evar_map
val global_kind : logical_kind
val goal_kind : locality_flag * goal_object_kind
+val global_proof_kind : logical_kind
+val goal_proof_kind : locality_flag * goal_object_kind
val global_fix_kind : logical_kind
val goal_fix_kind : locality_flag * goal_object_kind
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
index a29cd039..8429c267 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/contrib/subtac/test/ListsTest.v
@@ -5,12 +5,13 @@ Variable A : Set.
Program Definition myhd : forall { l : list A | length l <> 0 }, A :=
fun l =>
- match l with
+ match `l with
| nil => _
| hd :: tl => hd
end.
Proof.
- destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition.
+ destruct l ; simpl ; intro H.
+ rewrite H in n ; intuition.
Defined.
@@ -24,7 +25,7 @@ Program Definition mytail : forall { l : list A | length l <> 0 }, list A :=
| hd :: tl => tl
end.
Proof.
-destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition.
+destruct l ; simpl ; intro H ; rewrite H in n ; intuition.
Defined.
Extraction mytail.
@@ -50,7 +51,6 @@ Program Fixpoint append (l : list A) (l' : list A) { struct l } :
| nil => l'
| hd :: tl => hd :: (append tl l')
end.
-simpl.
subst ; auto.
simpl ; rewrite (subset_simpl (append tl0 l')).
simpl ; subst.
diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v
index ab200354..0b40ef82 100644
--- a/contrib/subtac/test/Mutind.v
+++ b/contrib/subtac/test/Mutind.v
@@ -1,7 +1,13 @@
-Fixpoint f (a : nat) : nat := match a with 0 => 0
-| S a' => g a a'
+Program Fixpoint f (a : nat) : nat :=
+ match a with
+ | 0 => 0
+ | S a' => g a a'
end
with g (a b : nat) { struct b } : nat :=
- match b with 0 => 0
+ match b with
+ | 0 => 0
| S b' => f b'
- end. \ No newline at end of file
+ end.
+
+Check f.
+Check g. \ No newline at end of file
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index 481b6708..ba5bdf23 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -12,8 +12,8 @@ reflexivity.
Defined.
Extraction testsig.
-Extraction sigS.
-Extract Inductive sigS => "" [ "" ].
+Extraction sig.
+Extract Inductive sig => "" [ "" ].
Extraction testsig.
Require Import Coq.Arith.Compare_dec.
diff --git a/contrib/subtac/test/measure.v b/contrib/subtac/test/measure.v
new file mode 100644
index 00000000..4764037d
--- /dev/null
+++ b/contrib/subtac/test/measure.v
@@ -0,0 +1,24 @@
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+Unset Printing All.
+Require Import Coq.Arith.Compare_dec.
+
+Require Import Coq.subtac.Utils.
+
+Fixpoint size (a : nat) : nat :=
+ match a with
+ 0 => 1
+ | S n => S (size n)
+ end.
+
+Program Fixpoint test_measure (a : nat) {measure a size} : nat :=
+ match a with
+ | S (S n) => S (test_measure n)
+ | x => x
+ end.
+subst.
+unfold n0.
+auto with arith.
+Qed.
+
+Check test_measure.
+Print test_measure. \ No newline at end of file
diff --git a/contrib/subtac/test/wf.v b/contrib/subtac/test/wf.v
new file mode 100644
index 00000000..49fec2b8
--- /dev/null
+++ b/contrib/subtac/test/wf.v
@@ -0,0 +1,48 @@
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+Unset Printing All.
+Require Import Coq.Arith.Compare_dec.
+
+Require Import Coq.subtac.Utils.
+
+Ltac one_simpl_hyp :=
+ match goal with
+ | [H : (`exist _ _ _) = _ |- _] => simpl in H
+ | [H : _ = (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) < _ |- _] => simpl in H
+ | [H : _ < (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) <= _ |- _] => simpl in H
+ | [H : _ <= (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) > _ |- _] => simpl in H
+ | [H : _ > (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) >= _ |- _] => simpl in H
+ | [H : _ >= (`exist _ _ _) |- _] => simpl in H
+ end.
+
+Ltac one_simpl_subtac :=
+ destruct_exists ;
+ repeat one_simpl_hyp ; simpl.
+
+Ltac simpl_subtac := do 3 one_simpl_subtac ; simpl.
+
+Require Import Omega.
+Require Import Wf_nat.
+
+Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt} :
+ { q : nat & { r : nat | a = b * q + r /\ r < b } } :=
+ if le_lt_dec b a then let (q', r) := euclid (a - b) b in
+ (S q' & r)
+ else (O & a).
+destruct b ; simpl_subtac.
+omega.
+simpl_subtac.
+assert(x0 * S q' = x0 + x0 * q').
+rewrite <- mult_n_Sm.
+omega.
+rewrite H2 ; omega.
+simpl_subtac.
+split ; auto with arith.
+omega.
+apply lt_wf.
+Defined.
+
+Check euclid_evars_proof. \ No newline at end of file
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 2235be4a..b6b1c7b6 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -474,7 +474,7 @@ let kind_of_global r =
match r with
| Ln.IndRef kn | Ln.ConstructRef (kn,_) ->
let isrecord =
- try let _ = Recordops.lookup_structure kn in true
+ try let _ = Recordops.lookup_projections kn in true
with Not_found -> false in
kind_of_inductive isrecord (fst kn)
| Ln.VarRef id -> kind_of_variable id