diff options
Diffstat (limited to 'contrib/funind')
| -rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 188 | ||||
| -rw-r--r-- | contrib/funind/functional_principles_proofs.mli | 3 | ||||
| -rw-r--r-- | contrib/funind/functional_principles_types.ml | 531 | ||||
| -rw-r--r-- | contrib/funind/functional_principles_types.mli | 11 | ||||
| -rw-r--r-- | contrib/funind/indfun.ml | 218 | ||||
| -rw-r--r-- | contrib/funind/indfun_common.ml | 495 | ||||
| -rw-r--r-- | contrib/funind/indfun_common.mli | 64 | ||||
| -rw-r--r-- | contrib/funind/indfun_main.ml4 | 302 | ||||
| -rw-r--r-- | contrib/funind/invfun.ml | 1068 | ||||
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 752 | ||||
| -rw-r--r-- | contrib/funind/rawterm_to_relation.mli | 22 | ||||
| -rw-r--r-- | contrib/funind/rawtermops.ml | 86 | ||||
| -rw-r--r-- | contrib/funind/rawtermops.mli | 10 | ||||
| -rw-r--r-- | contrib/funind/tacinv.ml4 | 13 |
14 files changed, 2715 insertions, 1048 deletions
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 *** |