diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/Recdef.v | 2 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 62 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 61 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.mli | 6 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 118 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml (renamed from plugins/funind/rawterm_to_relation.ml) | 298 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.mli (renamed from plugins/funind/rawterm_to_relation.mli) | 4 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.ml (renamed from plugins/funind/rawtermops.ml) | 438 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.mli | 126 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 549 | ||||
| -rw-r--r-- | plugins/funind/indfun.mli | 24 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 63 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 15 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 78 | ||||
| -rw-r--r-- | plugins/funind/merge.ml | 133 | ||||
| -rw-r--r-- | plugins/funind/rawtermops.mli | 126 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 229 | ||||
| -rw-r--r-- | plugins/funind/recdef_plugin.mllib | 4 |
18 files changed, 1187 insertions, 1149 deletions
diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v index 763ed82f..b29b8362 100644 --- a/plugins/funind/Recdef.v +++ b/plugins/funind/Recdef.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 3590e698..1d1e4a2a 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1,7 +1,6 @@ open Printer open Util open Term -open Termops open Namegen open Names open Declarations @@ -35,9 +34,10 @@ let observennl strm = let do_observe_tac s tac g = try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v with e -> - let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in + let e = Cerrors.process_vernac_interp_error e in + let goal = begin try (Printer.pr_goal g) with _ -> assert false end in msgnl (str "observation "++ s++str " raised exception " ++ - Cerrors.explain_exn e ++ str " on goal " ++ goal ); + Errors.print e ++ str " on goal " ++ goal ); raise e;; let observe_tac_stream s tac g = @@ -263,7 +263,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = in let sub = compute_substitution Intmap.empty (snd t1) (snd t2) in let sub = compute_substitution sub (fst t1) (fst t2) in - let end_of_type_with_pop = pop end_of_type in (*the equation will be removed *) + let end_of_type_with_pop = Termops.pop end_of_type in (*the equation will be removed *) let new_end_of_type = (* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4 Can be safely replaced by the next comment for Ocaml >= 3.08.4 @@ -286,7 +286,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = try let witness = Intmap.find i sub in if b' <> None then anomaly "can not redefine a rel!"; - (pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun)) + (Termops.pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun)) with Not_found -> (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) ) @@ -350,9 +350,9 @@ let isLetIn t = let h_reduce_with_zeta = h_reduce - (Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; + (Glob_term.Cbv + {Glob_term.all_flags + with Glob_term.rDelta = false; }) @@ -388,7 +388,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = let coq_I = Coqlib.build_coq_I () in let rec scan_type context type_of_hyp : tactic = if isLetIn type_of_hyp then - let real_type_of_hyp = it_mkProd_or_LetIn ~init:type_of_hyp context in + let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in (* length of context didn't change ? *) let new_context,new_typ_of_hyp = @@ -406,13 +406,13 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = then begin let (x,t_x,t') = destProd type_of_hyp in - let actual_real_type_of_hyp = it_mkProd_or_LetIn ~init:t' context in + let actual_real_type_of_hyp = it_mkProd_or_LetIn t' context in if is_property ptes_infos t_x actual_real_type_of_hyp then begin let pte,pte_args = (destApp t_x) in let (* fix_info *) prove_rec_hyp = (Idmap.find (destVar pte) ptes_infos).proving_tac in - let popped_t' = pop t' in - let real_type_of_hyp = it_mkProd_or_LetIn ~init:popped_t' context in + let popped_t' = Termops.pop t' in + let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in let prove_new_type_of_hyp = let context_length = List.length context in tclTHENLIST @@ -461,9 +461,9 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = (* observe (str "In "++Ppconstr.pr_id hyp_id++ *) (* str " removing useless precond True" *) (* ); *) - let popped_t' = pop t' in + let popped_t' = Termops.pop t' in let real_type_of_hyp = - it_mkProd_or_LetIn ~init:popped_t' context + it_mkProd_or_LetIn popped_t' context in let prove_trivial = let nb_intro = List.length context in @@ -489,9 +489,9 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = ] else if is_trivial_eq t_x then (* t_x := t = t => we remove this precond *) - let popped_t' = pop t' in + let popped_t' = Termops.pop t' in let real_type_of_hyp = - it_mkProd_or_LetIn ~init:popped_t' context + it_mkProd_or_LetIn popped_t' context in let hd,args = destApp t_x in let get_args hd args = @@ -589,7 +589,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = let fun_body = mkLambda(Anonymous, pf_type_of g' term, - replace_term term (mkRel 1) dyn_infos.info + Termops.replace_term term (mkRel 1) dyn_infos.info ) in let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in @@ -609,7 +609,7 @@ let my_orelse tac1 tac2 g = try tac1 g with e -> -(* observe (str "using snd tac since : " ++ Cerrors.explain_exn e); *) +(* observe (str "using snd tac since : " ++ Errors.print e); *) tac2 g let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id = @@ -909,8 +909,8 @@ let generalize_non_dep hyp g = let to_revert,_ = Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) -> if List.mem hyp hyps - or List.exists (occur_var_in_decl env hyp) keep - or occur_var env hyp hyp_typ + or List.exists (Termops.occur_var_in_decl env hyp) keep + or Termops.occur_var env hyp hyp_typ or Termops.is_section_variable hyp (* should be dangerous *) then (clear,decl::keep) else (hyp::clear,keep)) @@ -936,7 +936,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = 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 (Option.get f_def.const_body) + force (Option.get (body_of_constant f_def)) in let params,f_body_with_params = decompose_lam_n nb_params f_body in let (_,num),(_,_,bodies) = destFix f_body_with_params in @@ -954,7 +954,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let type_ctxt,type_of_f = decompose_prod_n_assum (nb_params + nb_args) (Typeops.type_of_constant_type (Global.env()) 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 lemma_type = it_mkProd_or_LetIn eqn type_ctxt in let f_id = id_of_label (con_label (destConst f)) in let prove_replacement = tclTHENSEQ @@ -964,7 +964,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = 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 false (mkVar rec_id,Rawterm.NoBindings)); + (* observe_tac "h_case" *) (h_case false (mkVar rec_id,Glob_term.NoBindings)); intros_reflexivity] g ) ] @@ -1009,7 +1009,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = | _ -> () in - Tacinterp.constr_of_id (pf_env g) equation_lemma_id + Constrintern.construct_reference (pf_hyps g) equation_lemma_id in let nb_intro_to_do = nb_prod (pf_concl g) in tclTHEN @@ -1052,7 +1052,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : } in let get_body const = - match (Global.lookup_constant const ).const_body with + match body_of_constant (Global.lookup_constant const) with | Some b -> let body = force b in Tacred.cbv_norm_flags @@ -1300,7 +1300,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in tclTHENSEQ - [unfold_in_concl [(all_occurrences,Names.EvalConstRef fname)]; + [unfold_in_concl [(Termops.all_occurrences, Names.EvalConstRef fname)]; let do_prove = build_proof interactive_proof @@ -1400,10 +1400,10 @@ let build_clause eqs = { Tacexpr.onhyps = Some (List.map - (fun id -> (Rawterm.all_occurrences_expr,id),InHyp) + (fun id -> (Glob_term.all_occurrences_expr, id), Termops.InHyp) eqs ); - Tacexpr.concl_occs = Rawterm.no_occurrences_expr + Tacexpr.concl_occs = Glob_term.no_occurrences_expr } let rec rewrite_eqs_in_eqs eqs = @@ -1416,7 +1416,7 @@ let rec rewrite_eqs_in_eqs eqs = (fun id gl -> observe_tac (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id)) - (tclTRY (Equality.general_rewrite_in true all_occurrences (* dep proofs also: *) true id (mkVar eq) false)) + (tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true (* dep proofs also: *) true id (mkVar eq) false)) gl ) eqs @@ -1438,7 +1438,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = (fun g -> if is_mes then - unfold_in_concl [(all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g + unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g else tclIDTAC g ); observe_tac "rew_and_finish" @@ -1451,7 +1451,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = Eauto.eauto_with_bases false (true,5) - [Lazy.force refl_equal] + [Evd.empty,Lazy.force refl_equal] [Auto.Hint_db.empty empty_transparent_state false] ) ) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index b756492b..6df9d574 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -1,7 +1,6 @@ open Printer open Util open Term -open Termops open Namegen open Names open Declarations @@ -114,9 +113,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = in let pre_princ = it_mkProd_or_LetIn - ~init: (it_mkProd_or_LetIn - ~init:(Option.fold_right + (Option.fold_right mkProd_or_LetIn princ_type_info.indarg princ_type_info.concl @@ -140,7 +138,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = in let dummy_var = mkVar (id_of_string "________") in let mk_replacement c i args = - let res = mkApp(rel_to_fun.(i),Array.map pop (array_get_start args)) in + let res = mkApp(rel_to_fun.(i), Array.map Termops.pop (array_get_start args)) in (* observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); *) res in @@ -199,58 +197,58 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = begin try let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in - let new_x : name = get_name (ids_of_context env) x in + let new_x : name = get_name (Termops.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 + then (Termops.pop new_b), filter_map (eq_constr (mkRel 1)) Termops.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) + (List.map Termops.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 + new_b, List.map Termops.pop binders_to_remove_from_b | Toberemoved_with_rel (n,c) -> (* 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) + new_b, list_add_set_eq eq_constr (mkRel n) (List.map Termops.pop binders_to_remove_from_b) end and compute_new_princ_type_for_letin remove env x v t b = begin try let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in - let new_x : name = get_name (ids_of_context env) x in + let new_x : name = get_name (Termops.ids_of_context env) x in let new_env = Environ.push_rel (x,Some v,t) env in let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b - then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b + then (Termops.pop new_b),filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b else ( mkLetIn(new_x,new_v,new_t,new_b), list_union_eq eq_constr (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v) - (List.map pop binders_to_remove_from_b) + (List.map Termops.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 + new_b, List.map Termops.pop binders_to_remove_from_b | Toberemoved_with_rel (n,c) -> (* 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) + new_b, list_add_set_eq eq_constr (mkRel n) (List.map Termops.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 @@ -267,10 +265,10 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = (lift (List.length ptes_vars) pre_res) in it_mkProd_or_LetIn - ~init:(it_mkProd_or_LetIn - ~init:pre_res (List.map (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b) - new_predicates) - ) + (it_mkProd_or_LetIn + pre_res (List.map (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b) + new_predicates) + ) princ_type_info.params @@ -283,7 +281,7 @@ let change_property_sort toSort princ princName = compose_prod args (mkSort toSort) ) in - let princName_as_constr = Tacinterp.constr_of_id (Global.env ()) princName in + let princName_as_constr = Constrintern.global_reference princName in let init = let nargs = (princ_info.nparams + (List.length princ_info.predicates)) in mkApp(princName_as_constr, @@ -291,8 +289,7 @@ let change_property_sort toSort princ princName = (fun i -> mkRel (nargs - i ))) in it_mkLambda_or_LetIn - ~init: - (it_mkLambda_or_LetIn ~init + (it_mkLambda_or_LetIn init (List.map change_sort_in_predicate princ_info.predicates) ) princ_info.params @@ -384,10 +381,9 @@ let generate_functional_principle (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) let ce = { const_entry_body = value; + const_entry_secctx = None; const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() - } + const_entry_opaque = false } in ignore( Declare.declare_constant @@ -450,7 +446,7 @@ let get_funs_constant mp dp = in function const -> let find_constant_body const = - match (Global.lookup_constant const ).const_body with + match body_of_constant (Global.lookup_constant const) with | Some b -> let body = force b in let body = Tacred.cbv_norm_flags @@ -475,7 +471,7 @@ let get_funs_constant mp dp = let first_params = List.hd l_params in List.iter (fun params -> - if not ((=) first_params params) + if not (list_equal (fun (n1, c1) (n2, c2) -> n1 = n2 && eq_constr c1 c2) first_params params) then error "Not a mutal recursive block" ) l_params @@ -493,7 +489,10 @@ let get_funs_constant mp dp = in let first_infos = extract_info true (List.hd l_bodies) in let check body = (* Hope this is correct *) - if not (first_infos = (extract_info false body)) + let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) = + ia1 = ia2 && na1 = na2 && array_equal eq_constr ta1 ta2 && array_equal eq_constr ca1 ca2 + in + if not (eq_infos first_infos (extract_info false body)) then error "Not a mutal recursive block" in List.iter check l_bodies @@ -504,7 +503,7 @@ let get_funs_constant mp dp = exception No_graph_found exception Found_type of int -let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_entry list = +let make_scheme (fas : (constant*Glob_term.glob_sort) list) : Entries.definition_entry list = let env = Global.env () and sigma = Evd.empty in let funs = List.map fst fas in @@ -584,7 +583,7 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent let finfos = find_Function_infos this_block_funs.(0) in try let equation = Option.get finfos.equation_lemma in - (Global.lookup_constant equation).Declarations.const_opaque + Declarations.is_opaque (Global.lookup_constant equation) with Option.IsNone -> (* non recursive definition *) false in @@ -639,7 +638,7 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent const with Found_type i -> let princ_body = - Termops.it_mkLambda_or_LetIn ~init:(mkFix((idxs,i),decl)) ctxt + Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt in {const with Entries.const_entry_body = princ_body; @@ -688,7 +687,7 @@ 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 *) +(* Constrintern.global_reference id *) (* in *) let funs = (fun (_,f,_) -> try Libnames.constr_of_global (Nametab.global f) diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index fb04c6ec..1c02c16e 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -27,8 +27,8 @@ val compute_new_princ_type_from_rel : constr array -> sorts array -> exception No_graph_found -val make_scheme : (constant*Rawterm.rawsort) list -> Entries.definition_entry list +val make_scheme : (constant*Glob_term.glob_sort) 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 +val build_scheme : (identifier*Libnames.reference*Glob_term.glob_sort) list -> unit +val build_case_scheme : (identifier*Libnames.reference*Glob_term.glob_sort) -> unit diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 41fafdf1..123399d5 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,19 +16,20 @@ open Indfun open Genarg open Pcoq open Tacticals +open Constr let pr_binding prc = function - | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) - | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) + | loc, Glob_term.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) + | loc, Glob_term.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) let pr_bindings prc prlc = function - | Rawterm.ImplicitBindings l -> + | Glob_term.ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ Util.prlist_with_sep spc prc l - | Rawterm.ExplicitBindings l -> + | Glob_term.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 () + | Glob_term.NoBindings -> mt () let pr_with_bindings prc prlc (c,bl) = prc c ++ hv 0 (pr_bindings prc prlc bl) @@ -55,7 +56,6 @@ let pr_fun_ind_using_typed prc prlc _ opt_c = ARGUMENT EXTEND fun_ind_using - TYPED AS constr_with_bindings_opt PRINTED BY pr_fun_ind_using_typed RAW_TYPED AS constr_with_bindings_opt RAW_PRINTED BY pr_fun_ind_using @@ -129,85 +129,36 @@ ARGUMENT EXTEND auto_using' | [ ] -> [ [] ] END -let pr_rec_annotation2_aux s r id l = - str ("{"^s^" ") ++ Ppconstr.pr_constr_expr r ++ - Util.pr_opt Nameops.pr_id id ++ - Pptactic.pr_auto_using Ppconstr.pr_constr_expr l ++ str "}" - -let pr_rec_annotation2 = function - | Struct id -> str "{struct" ++ Nameops.pr_id id ++ str "}" - | Wf(r,id,l) -> pr_rec_annotation2_aux "wf" r id l - | Mes(r,id,l) -> pr_rec_annotation2_aux "measure" r id l - -VERNAC ARGUMENT EXTEND rec_annotation2 -PRINTED BY pr_rec_annotation2 - [ "{" "struct" ident(id) "}"] -> [ Struct id ] -| [ "{" "wf" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Wf(r,id,l) ] -| [ "{" "measure" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Mes(r,id,l) ] -END - -let pr_binder2 (idl,c) = - str "(" ++ Util.prlist_with_sep spc Nameops.pr_id idl ++ spc () ++ - str ": " ++ Ppconstr.pr_lconstr_expr c ++ str ")" +module Gram = Pcoq.Gram +module Vernac = Pcoq.Vernac_ +module Tactic = Pcoq.Tactic -VERNAC ARGUMENT EXTEND binder2 -PRINTED BY pr_binder2 - [ "(" ne_ident_list(idl) ":" lconstr(c) ")"] -> [ (idl,c) ] -END +module FunctionGram = +struct + let gec s = Gram.entry_create ("Function."^s) + (* types *) + let function_rec_definition_loc : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) located Gram.entry = gec "function_rec_definition_loc" +end +open FunctionGram -let make_binder2 (idl,c) = - LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,Topconstr.default_binder_kind,c) - -let pr_rec_definition2 (id,bl,annot,type_,def) = - Nameops.pr_id id ++ spc () ++ Util.prlist_with_sep spc pr_binder2 bl ++ - Util.pr_opt pr_rec_annotation2 annot ++ spc () ++ str ":" ++ spc () ++ - Ppconstr.pr_lconstr_expr type_ ++ str " :=" ++ spc () ++ - Ppconstr.pr_lconstr_expr def - -VERNAC ARGUMENT EXTEND rec_definition2 -PRINTED BY pr_rec_definition2 - [ ident(id) binder2_list(bl) - rec_annotation2_opt(annot) ":" lconstr(type_) - ":=" lconstr(def)] -> - [ (id,bl,annot,type_,def) ] -END +GEXTEND Gram + GLOBAL: function_rec_definition_loc ; -let make_rec_definitions2 (id,bl,annot,type_,def) = - let bl = List.map make_binder2 bl in - let names = List.map snd (Topconstr.names_of_local_assums bl) in - let check_one_name () = - if List.length names > 1 then - Util.user_err_loc - (Util.dummy_loc,"Function", - Pp.str "the recursive argument needs to be specified"); - 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 - (try ignore(Util.list_index0 (Name id) names); annot - with Not_found -> Util.user_err_loc - (Util.dummy_loc,"Function", - Pp.str "No argument named " ++ Nameops.pr_id id) - ) - with Failure "check_exists_args" -> check_one_name ();annot - in - let ni = - match annot with - | None -> - annot - | Some an -> - check_exists_args an - in - ((Util.dummy_loc,id), ni, bl, type_, def) + function_rec_definition_loc: + [ [ g = Vernac.rec_definition -> loc, g ]] + ; + END +type 'a function_rec_definition_loc_argtype = ((Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) located, 'a) Genarg.abstract_argument_type +let (wit_function_rec_definition_loc : Genarg.tlevel function_rec_definition_loc_argtype), + (globwit_function_rec_definition_loc : Genarg.glevel function_rec_definition_loc_argtype), + (rawwit_function_rec_definition_loc : Genarg.rlevel function_rec_definition_loc_argtype) = + Genarg.create_arg "function_rec_definition_loc" VERNAC COMMAND EXTEND Function - ["Function" ne_rec_definition2_list_sep(recsl,"with")] -> + ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] -> [ - do_generate_principle false (List.map make_rec_definitions2 recsl); + do_generate_principle false (List.map snd recsl); ] END @@ -215,7 +166,7 @@ END let pr_fun_scheme_arg (princ_name,fun_name,s) = Nameops.pr_id princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++ - Ppconstr.pr_rawsort s + Ppconstr.pr_glob_sort s VERNAC ARGUMENT EXTEND fun_scheme_arg PRINTED BY pr_fun_scheme_arg @@ -224,17 +175,18 @@ END let warning_error names e = + let e = Cerrors.process_vernac_interp_error e in match e with | Building_graph e -> Pp.msg_warning (str "Cannot define graph(s) for " ++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++ - if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()) + if do_observe () then (spc () ++ Errors.print e) else mt ()) | Defining_principle e -> Pp.msg_warning (str "Cannot define principle(s) for "++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++ - if do_observe () then Cerrors.explain_exn e else mt ()) + if do_observe () then Errors.print e else mt ()) | _ -> raise e @@ -480,7 +432,7 @@ TACTIC EXTEND fauto [ "fauto" tactic(tac)] -> [ let heuristic = chose_heuristic None in - finduction None heuristic (snd tac) + finduction None heuristic (Tacinterp.eval_tactic tac) ] | [ "fauto" ] -> diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index b74422a3..c88c6669 100644 --- a/plugins/funind/rawterm_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -2,11 +2,11 @@ open Printer open Pp open Names open Term -open Rawterm +open Glob_term open Libnames open Indfun_common open Util -open Rawtermops +open Glob_termops let observe strm = if do_observe () @@ -23,31 +23,31 @@ type binder_type = | Prod of name | LetIn of name -type raw_context = (binder_type*rawconstr) list +type glob_context = (binder_type*glob_constr) list (* - compose_raw_context [(bt_1,n_1,t_1);......] rt returns + compose_glob_context [(bt_1,n_1,t_1);......] rt returns b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the binders corresponding to the bt_i's *) -let compose_raw_context = +let compose_glob_context = let compose_binder (bt,t) acc = match bt with - | Lambda n -> mkRLambda(n,t,acc) - | Prod n -> mkRProd(n,t,acc) - | LetIn n -> mkRLetIn(n,t,acc) + | Lambda n -> mkGLambda(n,t,acc) + | Prod n -> mkGProd(n,t,acc) + | LetIn n -> mkGLetIn(n,t,acc) in List.fold_right compose_binder (* - The main part deals with building a list of raw constructor expressions + The main part deals with building a list of globalized constructor expressions from the rhs of a fixpoint equation. *) type 'a build_entry_pre_return = { - context : raw_context; (* the binding context of the result *) + context : glob_context; (* the binding context of the result *) value : 'a; (* The value *) } @@ -159,8 +159,8 @@ let apply_args ctxt body args = | _,[] -> (* No more args *) (ctxt,body) | [],_ -> (* no more fun *) - let f,args' = raw_decompose_app body in - (ctxt,mkRApp(f,args'@args)) + let f,args' = glob_decompose_app body in + (ctxt,mkGApp(f,args'@args)) | (Lambda Anonymous,t)::ctxt',arg::args' -> do_apply avoid ctxt' body args' | (Lambda (Name id),t)::ctxt',arg::args' -> @@ -215,8 +215,8 @@ let combine_app f args = let combine_lam n t b = { context = []; - value = mkRLambda(n, compose_raw_context t.context t.value, - compose_raw_context b.context b.value ) + value = mkGLambda(n, compose_glob_context t.context t.value, + compose_glob_context b.context b.value ) } @@ -269,8 +269,8 @@ let make_discr_match_brl i = list_map_i (fun j (_,idl,patl,_) -> if j=i - then (dummy_loc,idl,patl, mkRRef (Lazy.force coq_True_ref)) - else (dummy_loc,idl,patl, mkRRef (Lazy.force coq_False_ref)) + then (dummy_loc,idl,patl, mkGRef (Lazy.force coq_True_ref)) + else (dummy_loc,idl,patl, mkGRef (Lazy.force coq_False_ref)) ) 0 (* @@ -281,7 +281,7 @@ let make_discr_match_brl i = *) let make_discr_match brl = fun el i -> - mkRCases(None, + mkGCases(None, make_discr_match_el el, make_discr_match_brl i brl) @@ -312,22 +312,22 @@ let build_constructors_of_type ind' argl = if argl = [] then Array.to_list - (Array.init (cst_narg - npar) (fun _ -> mkRHole ()) + (Array.init (cst_narg - npar) (fun _ -> mkGHole ()) ) else argl in let pat_as_term = - mkRApp(mkRRef (ConstructRef(ind',i+1)),argl) + mkGApp(mkGRef (ConstructRef(ind',i+1)),argl) in - cases_pattern_of_rawconstr Anonymous pat_as_term + cases_pattern_of_glob_constr Anonymous pat_as_term ) ind.Declarations.mind_consnames (* [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 + let f,_ = glob_decompose_app b in match f with - | RRef(_,ref) -> + | GRef(_,ref) -> begin let ind_type = match ref with @@ -350,8 +350,8 @@ let rec find_type_of nb b = then raise (Invalid_argument "find_type_of : not a valid inductive"); ind_type end - | RCast(_,b,_) -> find_type_of nb b - | RApp _ -> assert false (* we have decomposed any application via raw_decompose_app *) + | GCast(_,b,_) -> find_type_of nb b + | GApp _ -> assert false (* we have decomposed any application via glob_decompose_app *) | _ -> raise (Invalid_argument "not a ref") @@ -419,7 +419,7 @@ let add_pat_variables pat typ env : Environ.env = let rec pattern_to_term_and_type env typ = function | PatVar(loc,Anonymous) -> assert false | PatVar(loc,Name id) -> - mkRVar id + mkGVar id | PatCstr(loc,constr,patternl,_) -> let cst_narg = Inductiveops.mis_constructor_nargs_env @@ -445,7 +445,7 @@ let rec pattern_to_term_and_type env typ = function let patl_as_term = List.map2 (pattern_to_term_and_type env) (List.rev cs_args_types) patternl in - mkRApp(mkRRef(ConstructRef constr), + mkGApp(mkGRef(ConstructRef constr), implicit_args@patl_as_term ) @@ -472,7 +472,7 @@ let rec pattern_to_term_and_type env typ = function 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. + WARNING: The terms constructed here are only USING the glob_constr 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. @@ -481,15 +481,15 @@ let rec pattern_to_term_and_type env typ = function *) -let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = - observe (str " Entering : " ++ Printer.pr_rawconstr rt); +let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = + observe (str " Entering : " ++ Printer.pr_glob_constr rt); match rt with - | RRef _ | RVar _ | REvar _ | RPatVar _ | RSort _ | RHole _ -> + | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> (* 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 = + | GApp(_,_,_) -> + let f,args = glob_decompose_app rt in + let args_res : (glob_constr list) build_entry_return = List.fold_right (* create the arguments lists of constructors and combine them *) (fun arg ctxt_argsl -> let arg_res = build_entry_lc env funnames ctxt_argsl.to_avoid arg in @@ -500,19 +500,19 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = in begin match f with - | RLambda _ -> + | GLambda _ -> let rec aux t l = match l with | [] -> t | u::l -> match t with - | RLambda(loc,na,_,nat,b) -> - RLetIn(dummy_loc,na,u,aux b l) + | GLambda(loc,na,_,nat,b) -> + GLetIn(dummy_loc,na,u,aux b l) | _ -> - RApp(dummy_loc,t,l) + GApp(dummy_loc,t,l) in build_entry_lc env funnames avoid (aux f args) - | RVar(_,id) when Idset.mem id funnames -> + | GVar(_,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 @@ -525,20 +525,20 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = 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 + let res_rt = mkGVar res in let new_result = List.map (fun arg_res -> let new_hyps = [Prod (Name res),res_raw_type; - Prod Anonymous,mkRApp(res_rt,(mkRVar id)::arg_res.value)] + Prod Anonymous,mkGApp(res_rt,(mkGVar id)::arg_res.value)] in {context = arg_res.context@new_hyps; value = res_rt } ) args_res.result in { result = new_result; to_avoid = new_avoid } - | RVar _ | REvar _ | RPatVar _ | RHole _ | RSort _ | RRef _ -> + | GVar _ | GEvar _ | GPatVar _ | GHole _ | GSort _ | GRef _ -> (* if have [g t1 ... tn] with [g] not appearing in [funnames] then foreach [ctxt,v1 ... vn] in [args_res] we return @@ -549,11 +549,11 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = result = List.map (fun args_res -> - {args_res with value = mkRApp(f,args_res.value)}) + {args_res with value = mkGApp(f,args_res.value)}) args_res.result } - | RApp _ -> assert false (* we have collected all the app in [raw_decompose_app] *) - | RLetIn(_,n,t,b) -> + | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *) + | GLetIn(_,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 @@ -567,7 +567,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = let new_b = replace_var_by_term id - (RVar(dummy_loc,id)) + (GVar(dummy_loc,id)) b in (Name new_id,new_b,new_avoid) @@ -577,27 +577,26 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = env funnames avoid - (mkRLetIn(new_n,t,mkRApp(new_b,args))) - | RCases _ | RIf _ | RLetTuple _ -> + (mkGLetIn(new_n,t,mkGApp(new_b,args))) + | GCases _ | GIf _ | GLetTuple _ -> (* 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" - | RCast(_,b,_) -> + | GCast(_,b,_) -> (* 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" + build_entry_lc env funnames avoid (mkGApp(b,args)) + | GRec _ -> error "Not handled GRec" + | GProd _ -> error "Cannot apply a type" end (* end of the application treatement *) - | RLambda(_,n,_,t,b) -> + | GLambda(_,n,_,t,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the type @@ -612,7 +611,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = 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) -> + | GProd(_,n,_,t,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the type @@ -622,7 +621,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = 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,v,b) -> + | GLetIn(_,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] @@ -638,21 +637,21 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = 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) -> + | GCases(_,_,_,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 env funnames make_discr el brl avoid - | RIf(_,b,(na,e_option),lhs,rhs) -> + | GIf(_,b,(na,e_option),lhs,rhs) -> 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") + Printer.pr_glob_constr b ++ str " in " ++ + Printer.pr_glob_constr rt ++ str ". try again with a cast") in let case_pats = build_constructors_of_type ind [] in assert (Array.length case_pats = 2); @@ -663,17 +662,17 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = [lhs;rhs] in let match_expr = - mkRCases(None,[(b,(Anonymous,None))],brl) + mkGCases(None,[(b,(Anonymous,None))],brl) in - (* Pp.msgnl (str "new case := " ++ Printer.pr_rawconstr match_expr); *) + (* Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *) build_entry_lc env funnames avoid match_expr - | RLetTuple(_,nal,_,b,e) -> + | GLetTuple(_,nal,_,b,e) -> begin - let nal_as_rawconstr = + let nal_as_glob_constr = List.map (function - Name id -> mkRVar id - | Anonymous -> mkRHole () + Name id -> mkGVar id + | Anonymous -> mkGHole () ) nal in @@ -683,26 +682,25 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = 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") + Printer.pr_glob_constr b ++ str " in " ++ + Printer.pr_glob_constr rt ++ str ". try again with a cast") in - let case_pats = build_constructors_of_type ind nal_as_rawconstr in + let case_pats = build_constructors_of_type ind nal_as_glob_constr 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 + let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in build_entry_lc env funnames avoid match_expr end - | RRec _ -> error "Not handled RRec" - | RCast(_,b,_) -> + | GRec _ -> error "Not handled GRec" + | GCast(_,b,_) -> build_entry_lc env funnames avoid b - | RDynamic _ -> error "Not handled RDynamic" and build_entry_lc_from_case env funname make_discr (el:tomatch_tuples) - (brl:Rawterm.cases_clauses) avoid : - rawconstr build_entry_return = + (brl:Glob_term.cases_clauses) avoid : + glob_constr build_entry_return = match el with | [] -> assert false (* this case correspond to match <nothing> with .... !*) | el -> @@ -762,7 +760,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve (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 = + let not_those_patterns : (identifier list -> glob_constr -> glob_constr) list = List.map2 (fun pat typ -> fun avoid pat'_as_term -> @@ -778,9 +776,9 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve Detyping.detype false [] (Termops.names_of_rel_context env_with_pat_ids) typ_of_id in - mkRProd (Name id,raw_typ_of_id,acc)) + mkGProd (Name id,raw_typ_of_id,acc)) pat_ids - (raw_make_neq pat'_as_term (pattern_to_term renamed_pat)) + (glob_make_neq pat'_as_term (pattern_to_term renamed_pat)) ) patl types @@ -835,7 +833,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve else acc ) idl - [(Prod Anonymous,raw_make_eq ~typ pat_as_term e)] + [(Prod Anonymous,glob_make_eq ~typ pat_as_term e)] ) patl matched_expr.value @@ -879,16 +877,16 @@ let is_res id = let same_raw_term rt1 rt2 = match rt1,rt2 with - | RRef(_,r1), RRef (_,r2) -> r1=r2 - | RHole _, RHole _ -> true + | GRef(_,r1), GRef (_,r2) -> r1=r2 + | GHole _, GHole _ -> true | _ -> false let decompose_raw_eq lhs rhs = let rec decompose_raw_eq lhs rhs acc = - observe (str "decomposing eq for " ++ pr_rawconstr lhs ++ str " " ++ pr_rawconstr rhs); - let (rhd,lrhs) = raw_decompose_app rhs in - let (lhd,llhs) = raw_decompose_app lhs in - observe (str "lhd := " ++ pr_rawconstr lhd); - observe (str "rhd := " ++ pr_rawconstr rhd); + observe (str "decomposing eq for " ++ pr_glob_constr lhs ++ str " " ++ pr_glob_constr rhs); + let (rhd,lrhs) = glob_decompose_app rhs in + let (lhd,llhs) = glob_decompose_app lhs in + observe (str "lhd := " ++ pr_glob_constr lhd); + observe (str "rhd := " ++ pr_glob_constr rhd); observe (str "llhs := " ++ int (List.length llhs)); observe (str "lrhs := " ++ int (List.length lrhs)); let sllhs = List.length llhs in @@ -905,29 +903,29 @@ let decompose_raw_eq lhs rhs = exception Continue (* The second phase which reconstruct the real type of the constructor. - rebuild the raw constructors expression. + rebuild the globalized constructors expression. eliminates some meaningless equalities, applies some rewrites...... *) let rec rebuild_cons env nb_args relname args crossed_types depth rt = - observe (str "rebuilding : " ++ pr_rawconstr rt); + observe (str "rebuilding : " ++ pr_glob_constr rt); match rt with - | RProd(_,n,k,t,b) -> + | GProd(_,n,k,t,b) -> let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t::crossed_types in begin match t with - | RApp(_,(RVar(_,res_id) as res_rt),args') when is_res res_id -> + | GApp(_,(GVar(_,res_id) as res_rt),args') when is_res res_id -> begin match args' with - | (RVar(_,this_relname))::args' -> + | (GVar(_,this_relname))::args' -> (*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]) + mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt]) in let t' = Pretyping.Default.understand Evd.empty env new_t in let new_env = Environ.push_rel (n,None,t') env in @@ -937,17 +935,17 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = args new_crossed_types (depth + 1) b in - mkRProd(n,new_t,new_b), + mkGProd(n,new_t,new_b), Idset.filter not_free_in_t id_to_exclude | _ -> (* the first args is the name of the function! *) assert false end - | RApp(loc1,RRef(loc2,eq_as_ref),[ty;RVar(loc3,id);rt]) + | GApp(loc1,GRef(loc2,eq_as_ref),[ty;GVar(loc3,id);rt]) when eq_as_ref = Lazy.force Coqlib.coq_eq_ref && n = Anonymous -> begin try - observe (str "computing new type for eq : " ++ pr_rawconstr rt); + observe (str "computing new type for eq : " ++ pr_glob_constr rt); let t' = try Pretyping.Default.understand Evd.empty env t with _ -> raise Continue in @@ -968,7 +966,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = new_args new_crossed_types (depth + 1) subst_b in - mkRProd(n,t,new_b),id_to_exclude + mkGProd(n,t,new_b),id_to_exclude with Continue -> let jmeq = Libnames.IndRef (destInd (jmeq ())) in let ty' = Pretyping.Default.understand Evd.empty env ty in @@ -979,20 +977,20 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = ((Util.list_chop nparam args')) in let rt_typ = - RApp(Util.dummy_loc, - RRef (Util.dummy_loc,Libnames.IndRef ind), + GApp(Util.dummy_loc, + GRef (Util.dummy_loc,Libnames.IndRef ind), (List.map (fun p -> Detyping.detype false [] (Termops.names_of_rel_context env) p) params)@(Array.to_list (Array.make (List.length args' - nparam) - (mkRHole ())))) + (mkGHole ())))) in let eq' = - RApp(loc1,RRef(loc2,jmeq),[ty;RVar(loc3,id);rt_typ;rt]) + GApp(loc1,GRef(loc2,jmeq),[ty;GVar(loc3,id);rt_typ;rt]) in - observe (str "computing new type for jmeq : " ++ pr_rawconstr eq'); + observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); let eq'_as_constr = Pretyping.Default.understand Evd.empty env eq' in observe (str " computing new type for jmeq : done") ; let new_args = @@ -1051,14 +1049,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = new_args new_crossed_types (depth + 1) subst_b in - mkRProd(n,eq',new_b),id_to_exclude + mkGProd(n,eq',new_b),id_to_exclude end (* 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 + mkGProd(n,t,new_b),id_to_exclude else new_b, Idset.add id id_to_exclude *) - | RApp(loc1,RRef(loc2,eq_as_ref),[ty;rt1;rt2]) + | GApp(loc1,GRef(loc2,eq_as_ref),[ty;rt1;rt2]) when eq_as_ref = Lazy.force Coqlib.coq_eq_ref && n = Anonymous -> begin @@ -1069,8 +1067,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let new_rt = List.fold_left (fun acc (lhs,rhs) -> - mkRProd(Anonymous, - mkRApp(mkRRef(eq_as_ref),[mkRHole ();lhs;rhs]),acc) + mkGProd(Anonymous, + mkGApp(mkGRef(eq_as_ref),[mkGHole ();lhs;rhs]),acc) ) b l @@ -1078,7 +1076,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = rebuild_cons env nb_args relname args crossed_types depth new_rt else raise Continue with Continue -> - observe (str "computing new type for prod : " ++ pr_rawconstr rt); + observe (str "computing new type for prod : " ++ pr_glob_constr rt); let t' = Pretyping.Default.understand Evd.empty env t in let new_env = Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = @@ -1091,10 +1089,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | Name id when Idset.mem id id_to_exclude && depth >= nb_args -> new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) - | _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude + | _ -> mkGProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude end | _ -> - observe (str "computing new type for prod : " ++ pr_rawconstr rt); + observe (str "computing new type for prod : " ++ pr_glob_constr rt); let t' = Pretyping.Default.understand Evd.empty env t in let new_env = Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = @@ -1107,13 +1105,13 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | Name id when Idset.mem id id_to_exclude && depth >= nb_args -> new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) - | _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude + | _ -> mkGProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude end - | RLambda(_,n,k,t,b) -> + | GLambda(_,n,k,t,b) -> begin let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t :: crossed_types in - observe (str "computing new type for lambda : " ++ pr_rawconstr rt); + observe (str "computing new type for lambda : " ++ pr_glob_constr rt); let t' = Pretyping.Default.understand Evd.empty env t in match n with | Name id -> @@ -1121,19 +1119,19 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let new_b,id_to_exclude = rebuild_cons new_env nb_args relname - (args@[mkRVar id])new_crossed_types + (args@[mkGVar id])new_crossed_types (depth + 1 ) b in if Idset.mem id id_to_exclude && depth >= nb_args then new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude) else - RProd(dummy_loc,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude + GProd(dummy_loc,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude | _ -> anomaly "Should not have an anonymous function here" (* We have renamed all the anonymous functions during alpha_renaming phase *) end - | RLetIn(_,n,t,b) -> + | GLetIn(_,n,t,b) -> begin let not_free_in_t id = not (is_free_in id t) in let t' = Pretyping.Default.understand Evd.empty env t in @@ -1147,10 +1145,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match n with | Name id when Idset.mem id id_to_exclude && depth >= nb_args -> new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) - | _ -> RLetIn(dummy_loc,n,t,new_b), + | _ -> GLetIn(dummy_loc,n,t,new_b), Idset.filter not_free_in_t id_to_exclude end - | RLetTuple(_,nal,(na,rto),t,b) -> + | GLetTuple(_,nal,(na,rto),t,b) -> assert (rto=None); begin let not_free_in_t id = not (is_free_in id t) in @@ -1173,22 +1171,22 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (* | Name id when Idset.mem id id_to_exclude -> *) (* new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *) (* | _ -> *) - RLetTuple(dummy_loc,nal,(na,None),t,new_b), + GLetTuple(dummy_loc,nal,(na,None),t,new_b), Idset.filter not_free_in_t (Idset.union id_to_exclude id_to_exclude') end - | _ -> mkRApp(mkRVar relname,args@[rt]),Idset.empty + | _ -> mkGApp(mkGVar relname,args@[rt]),Idset.empty (* debuging wrapper *) let rebuild_cons env nb_args relname args crossed_types rt = - observe (str "rebuild_cons : rt := "++ pr_rawconstr rt ++ - str "nb_args := " ++ str (string_of_int nb_args)); +(* observennl (str "rebuild_cons : rt := "++ pr_glob_constr rt ++ *) +(* str "nb_args := " ++ str (string_of_int nb_args)); *) let res = rebuild_cons env nb_args relname args crossed_types 0 rt in - observe (str " leads to "++ pr_rawconstr (fst res)); +(* observe (str " leads to "++ pr_glob_constr (fst res)); *) res @@ -1200,30 +1198,30 @@ let rebuild_cons env nb_args relname args crossed_types rt = 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 -> + | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params + | GApp(_,GVar(_,relname'),rtl) when Idset.mem relname' relnames -> compute_cst_params_from_app [] (params,rtl) - | RApp(_,f,args) -> + | GApp(_,f,args) -> List.fold_left (compute_cst_params relnames) params (f::args) - | RLambda(_,_,_,t,b) | RProd(_,_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) -> + | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetIn(_,_,t,b) | GLetTuple(_,_,_,t,b) -> let t_params = compute_cst_params relnames params t in compute_cst_params relnames t_params b - | RCases _ -> + | GCases _ -> params (* If there is still cases at this point they can only be discriminitation ones *) - | RSort _ -> params - | RHole _ -> params - | RIf _ | RRec _ | RCast _ | RDynamic _ -> + | GSort _ -> params + | GHole _ -> params + | GIf _ | GRec _ | GCast _ -> raise (UserError("compute_cst_params", str "Not handled case")) and compute_cst_params_from_app acc (params,rtl) = match params,rtl with | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) - | ((Name id,_,is_defined) as param)::params',(RVar(_,id'))::rtl' + | ((Name id,_,is_defined) as param)::params',(GVar(_,id'))::rtl' when id_ord id id' == 0 && not is_defined -> compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc -let compute_params_name relnames (args : (Names.name * Rawterm.rawconstr * bool) list array) csts = +let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * bool) list array) csts = let rels_params = Array.mapi (fun i args -> @@ -1242,7 +1240,7 @@ let compute_params_name relnames (args : (Names.name * Rawterm.rawconstr * bool) if array_for_all (fun l -> let (n',nt',is_defined') = List.nth l i in - n = n' && Topconstr.eq_rawconstr nt nt' && is_defined = is_defined') + n = n' && Topconstr.eq_glob_constr nt nt' && is_defined = is_defined') rels_params then l := param::!l @@ -1261,15 +1259,15 @@ 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,RType None)) + | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc,GType None)) let do_build_inductive - funnames (funsargs: (Names.name * rawconstr * bool) list list) + funnames (funsargs: (Names.name * glob_constr * bool) list list) returned_types - (rtl:rawconstr list) = + (rtl:glob_constr list) = let _time1 = System.get_time () in -(* Pp.msgnl (prlist_with_sep fnl Printer.pr_rawconstr rtl); *) +(* Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr 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 @@ -1286,7 +1284,7 @@ let do_build_inductive 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 + Environ.push_named (id,None,Typing.type_of env Evd.empty (Constrintern.global_reference id)) env ) funnames (Global.env ()) @@ -1294,19 +1292,19 @@ let do_build_inductive let resa = Array.map (build_entry_lc env funnames_as_set []) rta in let env_with_graphs = let rel_arity i funargs = (* Reduilding arities (with parameters) *) - let rel_first_args :(Names.name * Rawterm.rawconstr * bool ) list = + let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list = funargs in List.fold_right (fun (n,t,is_defined) acc -> if is_defined then - Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_rawconstr Idset.empty t, + Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, acc) else Topconstr.CProdN (dummy_loc, - [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_rawconstr Idset.empty t], + [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], acc ) ) @@ -1325,9 +1323,9 @@ let do_build_inductive let constr i res = List.map (function result (* (args',concl') *) -> - let rt = compose_raw_context result.context result.value in + let rt = compose_glob_context result.context result.value in let nb_args = List.length funsargs.(i) in - (* with_full_print (fun rt -> Pp.msgnl (str "raw constr " ++ pr_rawconstr rt)) rt; *) + (* with_full_print (fun rt -> Pp.msgnl (str "glob constr " ++ pr_glob_constr rt)) rt; *) fst ( rebuild_cons env_with_graphs nb_args relnames.(i) [] @@ -1346,7 +1344,7 @@ let do_build_inductive 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 = + let rel_constructors i rt : (identifier*glob_constr) list = next_constructor_id := (-1); List.map (fun constr -> (mk_constructor_id i),constr) (constr i rt) in @@ -1360,19 +1358,19 @@ let do_build_inductive rel_constructors in let rel_arity i funargs = (* Reduilding arities (with parameters) *) - let rel_first_args :(Names.name * Rawterm.rawconstr * bool ) list = + let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list = (snd (list_chop nrel_params funargs)) in List.fold_right (fun (n,t,is_defined) acc -> if is_defined then - Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_rawconstr Idset.empty t, + Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, acc) else Topconstr.CProdN (dummy_loc, - [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_rawconstr Idset.empty t], + [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], acc ) ) @@ -1389,10 +1387,10 @@ let do_build_inductive (fun (n,t,is_defined) -> if is_defined then - Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_rawconstr Idset.empty t) + Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_glob_constr Idset.empty t) else Topconstr.LocalRawAssum - ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_rawconstr Idset.empty t) + ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t) ) rels_params in @@ -1402,7 +1400,7 @@ let do_build_inductive false,((dummy_loc,id), Flags.with_option Flags.raw_print - (Constrextern.extern_rawtype Idset.empty) ((* zeta_normalize *) t) + (Constrextern.extern_glob_type Idset.empty) ((* zeta_normalize *) t) ) )) (rel_constructors) @@ -1465,7 +1463,7 @@ let do_build_inductive str "while trying to define"++ spc () ++ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds)) ++ fnl () ++ - Cerrors.explain_exn e + Errors.print e in observe msg; raise e diff --git a/plugins/funind/rawterm_to_relation.mli b/plugins/funind/glob_term_to_relation.mli index a314050f..5c91292b 100644 --- a/plugins/funind/rawterm_to_relation.mli +++ b/plugins/funind/glob_term_to_relation.mli @@ -9,8 +9,8 @@ val build_inductive : Names.identifier list -> (* The list of function name *) - (Names.name*Rawterm.rawconstr*bool) list list -> (* The list of function args *) + (Names.name*Glob_term.glob_constr*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 *) + Glob_term.glob_constr list -> (* the list of body *) unit diff --git a/plugins/funind/rawtermops.ml b/plugins/funind/glob_termops.ml index e31f1452..cdd0eaf7 100644 --- a/plugins/funind/rawtermops.ml +++ b/plugins/funind/glob_termops.ml @@ -1,89 +1,89 @@ open Pp -open Rawterm +open Glob_term open Util open Names (* Ocaml 3.06 Map.S does not handle is_empty *) let idmap_is_empty m = m = Idmap.empty (* - Some basic functions to rebuild rawconstr + Some basic functions to rebuild glob_constr In each of them the location is Util.dummy_loc *) -let mkRRef ref = RRef(dummy_loc,ref) -let mkRVar id = RVar(dummy_loc,id) -let mkRApp(rt,rtl) = RApp(dummy_loc,rt,rtl) -let mkRLambda(n,t,b) = RLambda(dummy_loc,n,Explicit,t,b) -let mkRProd(n,t,b) = RProd(dummy_loc,n,Explicit,t,b) -let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b) -let mkRCases(rto,l,brl) = RCases(dummy_loc,Term.RegularStyle,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,CastConv (Term.DEFAULTcast,t)) +let mkGRef ref = GRef(dummy_loc,ref) +let mkGVar id = GVar(dummy_loc,id) +let mkGApp(rt,rtl) = GApp(dummy_loc,rt,rtl) +let mkGLambda(n,t,b) = GLambda(dummy_loc,n,Explicit,t,b) +let mkGProd(n,t,b) = GProd(dummy_loc,n,Explicit,t,b) +let mkGLetIn(n,t,b) = GLetIn(dummy_loc,n,t,b) +let mkGCases(rto,l,brl) = GCases(dummy_loc,Term.RegularStyle,rto,l,brl) +let mkGSort s = GSort(dummy_loc,s) +let mkGHole () = GHole(dummy_loc,Evd.BinderType Anonymous) +let mkGCast(b,t) = GCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t)) (* - Some basic functions to decompose rawconstrs + Some basic functions to decompose glob_constrs These are analogous to the ones constrs *) -let raw_decompose_prod = - let rec raw_decompose_prod args = function - | RProd(_,n,k,t,b) -> - raw_decompose_prod ((n,t)::args) b +let glob_decompose_prod = + let rec glob_decompose_prod args = function + | GProd(_,n,k,t,b) -> + glob_decompose_prod ((n,t)::args) b | rt -> args,rt in - raw_decompose_prod [] - -let raw_decompose_prod_or_letin = - let rec raw_decompose_prod args = function - | RProd(_,n,k,t,b) -> - raw_decompose_prod ((n,None,Some t)::args) b - | RLetIn(_,n,t,b) -> - raw_decompose_prod ((n,Some t,None)::args) b + glob_decompose_prod [] + +let glob_decompose_prod_or_letin = + let rec glob_decompose_prod args = function + | GProd(_,n,k,t,b) -> + glob_decompose_prod ((n,None,Some t)::args) b + | GLetIn(_,n,t,b) -> + glob_decompose_prod ((n,Some t,None)::args) b | rt -> args,rt in - raw_decompose_prod [] + glob_decompose_prod [] -let raw_compose_prod = - List.fold_left (fun b (n,t) -> mkRProd(n,t,b)) +let glob_compose_prod = + List.fold_left (fun b (n,t) -> mkGProd(n,t,b)) -let raw_compose_prod_or_letin = +let glob_compose_prod_or_letin = List.fold_left ( fun concl decl -> match decl with - | (n,None,Some t) -> mkRProd(n,t,concl) - | (n,Some bdy,None) -> mkRLetIn(n,bdy,concl) + | (n,None,Some t) -> mkGProd(n,t,concl) + | (n,Some bdy,None) -> mkGLetIn(n,bdy,concl) | _ -> assert false) -let raw_decompose_prod_n n = - let rec raw_decompose_prod i args c = +let glob_decompose_prod_n n = + let rec glob_decompose_prod i args c = if i<=0 then args,c else match c with - | RProd(_,n,_,t,b) -> - raw_decompose_prod (i-1) ((n,t)::args) b + | GProd(_,n,_,t,b) -> + glob_decompose_prod (i-1) ((n,t)::args) b | rt -> args,rt in - raw_decompose_prod n [] + glob_decompose_prod n [] -let raw_decompose_prod_or_letin_n n = - let rec raw_decompose_prod i args c = +let glob_decompose_prod_or_letin_n n = + let rec glob_decompose_prod i args c = if i<=0 then args,c else match c with - | RProd(_,n,_,t,b) -> - raw_decompose_prod (i-1) ((n,None,Some t)::args) b - | RLetIn(_,n,t,b) -> - raw_decompose_prod (i-1) ((n,Some t,None)::args) b + | GProd(_,n,_,t,b) -> + glob_decompose_prod (i-1) ((n,None,Some t)::args) b + | GLetIn(_,n,t,b) -> + glob_decompose_prod (i-1) ((n,Some t,None)::args) b | rt -> args,rt in - raw_decompose_prod n [] + glob_decompose_prod n [] -let raw_decompose_app = +let glob_decompose_app = let rec decompose_rapp acc rt = -(* msgnl (str "raw_decompose_app on : "++ Printer.pr_rawconstr rt); *) +(* msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *) match rt with - | RApp(_,rt,rtl) -> + | GApp(_,rt,rtl) -> decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt | rt -> rt,List.rev acc in @@ -92,24 +92,24 @@ let raw_decompose_app = -(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *) -let raw_make_eq ?(typ= mkRHole ()) t1 t2 = - mkRApp(mkRRef (Lazy.force Coqlib.coq_eq_ref),[typ;t2;t1]) +(* [glob_make_eq t1 t2] build the glob_constr corresponding to [t2 = t1] *) +let glob_make_eq ?(typ= mkGHole ()) t1 t2 = + mkGApp(mkGRef (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 = - mkRApp(mkRRef (Lazy.force Coqlib.coq_not_ref),[raw_make_eq t1 t2]) +(* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *) +let glob_make_neq t1 t2 = + mkGApp(mkGRef (Lazy.force Coqlib.coq_not_ref),[glob_make_eq t1 t2]) -(* [raw_make_or P1 P2] build the rawconstr corresponding to [P1 \/ P2] *) -let raw_make_or t1 t2 = mkRApp (mkRRef(Lazy.force Coqlib.coq_or_ref),[t1;t2]) +(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *) +let glob_make_or t1 t2 = mkGApp (mkGRef(Lazy.force Coqlib.coq_or_ref),[t1;t2]) -(* [raw_make_or_list [P1;...;Pn]] build the rawconstr corresponding +(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding to [P1 \/ ( .... \/ Pn)] *) -let rec raw_make_or_list = function +let rec glob_make_or_list = function | [] -> raise (Invalid_argument "mk_or") | [e] -> e - | e::l -> raw_make_or e (raw_make_or_list l) + | e::l -> glob_make_or e (glob_make_or_list l) let remove_name_from_mapping mapping na = @@ -120,70 +120,69 @@ let remove_name_from_mapping mapping na = let change_vars = let rec change_vars mapping rt = match rt with - | RRef _ -> rt - | RVar(loc,id) -> + | GRef _ -> rt + | GVar(loc,id) -> let new_id = try Idmap.find id mapping with Not_found -> id in - RVar(loc,new_id) - | REvar _ -> rt - | RPatVar _ -> rt - | RApp(loc,rt',rtl) -> - RApp(loc, + GVar(loc,new_id) + | GEvar _ -> rt + | GPatVar _ -> rt + | GApp(loc,rt',rtl) -> + GApp(loc, change_vars mapping rt', List.map (change_vars mapping) rtl ) - | RLambda(loc,name,k,t,b) -> - RLambda(loc, + | GLambda(loc,name,k,t,b) -> + GLambda(loc, name, k, change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) - | RProd(loc,name,k,t,b) -> - RProd(loc, + | GProd(loc,name,k,t,b) -> + GProd(loc, name, k, change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) - | RLetIn(loc,name,def,b) -> - RLetIn(loc, + | GLetIn(loc,name,def,b) -> + GLetIn(loc, name, change_vars mapping def, change_vars (remove_name_from_mapping mapping name) b ) - | RLetTuple(loc,nal,(na,rto),b,e) -> + | GLetTuple(loc,nal,(na,rto),b,e) -> let new_mapping = List.fold_left remove_name_from_mapping mapping nal in - RLetTuple(loc, + GLetTuple(loc, nal, (na, Option.map (change_vars mapping) rto), change_vars mapping b, change_vars new_mapping e ) - | RCases(loc,sty,infos,el,brl) -> - RCases(loc,sty, + | GCases(loc,sty,infos,el,brl) -> + GCases(loc,sty, infos, List.map (fun (e,x) -> (change_vars mapping e,x)) el, List.map (change_vars_br mapping) brl ) - | RIf(loc,b,(na,e_option),lhs,rhs) -> - RIf(loc, + | GIf(loc,b,(na,e_option),lhs,rhs) -> + GIf(loc, change_vars mapping b, (na,Option.map (change_vars mapping) e_option), change_vars mapping lhs, change_vars mapping rhs ) - | RRec _ -> error "Local (co)fixes are not supported" - | RSort _ -> rt - | RHole _ -> rt - | RCast(loc,b,CastConv (k,t)) -> - RCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t)) - | RCast(loc,b,CastCoerce) -> - RCast(loc,change_vars mapping b,CastCoerce) - | RDynamic _ -> error "Not handled RDynamic" + | GRec _ -> error "Local (co)fixes are not supported" + | GSort _ -> rt + | GHole _ -> rt + | GCast(loc,b,CastConv (k,t)) -> + GCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t)) + | GCast(loc,b,CastCoerce) -> + GCast(loc,change_vars mapping b,CastCoerce) and change_vars_br mapping ((loc,idl,patl,res) as br) = let new_mapping = List.fold_right Idmap.remove idl mapping in if idmap_is_empty new_mapping @@ -262,22 +261,22 @@ let get_pattern_id pat = raw_get_pattern_id pat [] let rec alpha_rt excluded rt = let new_rt = match rt with - | RRef _ | RVar _ | REvar _ | RPatVar _ -> rt - | RLambda(loc,Anonymous,k,t,b) -> + | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt + | GLambda(loc,Anonymous,k,t,b) -> let new_id = Namegen.next_ident_away (id_of_string "_x") excluded in let new_excluded = new_id :: excluded in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in - RLambda(loc,Name new_id,k,new_t,new_b) - | RProd(loc,Anonymous,k,t,b) -> + GLambda(loc,Name new_id,k,new_t,new_b) + | GProd(loc,Anonymous,k,t,b) -> let new_t = alpha_rt excluded t in let new_b = alpha_rt excluded b in - RProd(loc,Anonymous,k,new_t,new_b) - | RLetIn(loc,Anonymous,t,b) -> + GProd(loc,Anonymous,k,new_t,new_b) + | GLetIn(loc,Anonymous,t,b) -> let new_t = alpha_rt excluded t in let new_b = alpha_rt excluded b in - RLetIn(loc,Anonymous,new_t,new_b) - | RLambda(loc,Name id,k,t,b) -> + GLetIn(loc,Anonymous,new_t,new_b) + | GLambda(loc,Name id,k,t,b) -> let new_id = Namegen.next_ident_away id excluded in let t,b = if new_id = id @@ -289,8 +288,8 @@ let rec alpha_rt excluded rt = let new_excluded = new_id::excluded in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in - RLambda(loc,Name new_id,k,new_t,new_b) - | RProd(loc,Name id,k,t,b) -> + GLambda(loc,Name new_id,k,new_t,new_b) + | GProd(loc,Name id,k,t,b) -> let new_id = Namegen.next_ident_away id excluded in let new_excluded = new_id::excluded in let t,b = @@ -302,8 +301,8 @@ let rec alpha_rt excluded rt = in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in - RProd(loc,Name new_id,k,new_t,new_b) - | RLetIn(loc,Name id,t,b) -> + GProd(loc,Name new_id,k,new_t,new_b) + | GLetIn(loc,Name id,t,b) -> let new_id = Namegen.next_ident_away id excluded in let t,b = if new_id = id @@ -315,10 +314,10 @@ let rec alpha_rt excluded rt = let new_excluded = new_id::excluded in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in - RLetIn(loc,Name new_id,new_t,new_b) + GLetIn(loc,Name new_id,new_t,new_b) - | RLetTuple(loc,nal,(na,rto),t,b) -> + | GLetTuple(loc,nal,(na,rto),t,b) -> let rev_new_nal,new_excluded,mapping = List.fold_left (fun (nal,excluded,mapping) na -> @@ -345,28 +344,27 @@ let rec alpha_rt excluded rt = let new_t = alpha_rt new_excluded new_t in let new_b = alpha_rt new_excluded new_b in let new_rto = Option.map (alpha_rt new_excluded) new_rto in - RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b) - | RCases(loc,sty,infos,el,brl) -> + GLetTuple(loc,new_nal,(na,new_rto),new_t,new_b) + | GCases(loc,sty,infos,el,brl) -> let new_el = List.map (function (rt,i) -> alpha_rt excluded rt, i) el in - RCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl) - | RIf(loc,b,(na,e_o),lhs,rhs) -> - RIf(loc,alpha_rt excluded b, + GCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl) + | GIf(loc,b,(na,e_o),lhs,rhs) -> + GIf(loc,alpha_rt excluded b, (na,Option.map (alpha_rt excluded) e_o), alpha_rt excluded lhs, alpha_rt excluded rhs ) - | RRec _ -> error "Not handled RRec" - | RSort _ -> rt - | RHole _ -> rt - | RCast (loc,b,CastConv (k,t)) -> - RCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t)) - | RCast (loc,b,CastCoerce) -> - RCast(loc,alpha_rt excluded b,CastCoerce) - | RDynamic _ -> error "Not handled RDynamic" - | RApp(loc,f,args) -> - RApp(loc, + | GRec _ -> error "Not handled GRec" + | GSort _ -> rt + | GHole _ -> rt + | GCast (loc,b,CastConv (k,t)) -> + GCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t)) + | GCast (loc,b,CastCoerce) -> + GCast(loc,alpha_rt excluded b,CastCoerce) + | GApp(loc,f,args) -> + GApp(loc, alpha_rt excluded f, List.map (alpha_rt excluded) args ) @@ -386,35 +384,34 @@ and alpha_br excluded (loc,ids,patl,res) = *) let is_free_in id = let rec is_free_in = function - | RRef _ -> false - | RVar(_,id') -> id_ord id' id == 0 - | REvar _ -> false - | RPatVar _ -> false - | RApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl) - | RLambda(_,n,_,t,b) | RProd(_,n,_,t,b) | RLetIn(_,n,t,b) -> + | GRef _ -> false + | GVar(_,id') -> id_ord id' id == 0 + | GEvar _ -> false + | GPatVar _ -> false + | GApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl) + | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) | GLetIn(_,n,t,b) -> let check_in_b = match n with | Name id' -> id_ord id' id <> 0 | _ -> true in is_free_in t || (check_in_b && is_free_in b) - | RCases(_,_,_,el,brl) -> + | GCases(_,_,_,el,brl) -> (List.exists (fun (e,_) -> is_free_in e) el) || List.exists is_free_in_br brl - | RLetTuple(_,nal,_,b,t) -> + | GLetTuple(_,nal,_,b,t) -> let check_in_nal = not (List.exists (function Name id' -> id'= id | _ -> false) nal) in is_free_in t || (check_in_nal && is_free_in b) - | RIf(_,cond,_,br1,br2) -> + | GIf(_,cond,_,br1,br2) -> is_free_in cond || is_free_in br1 || is_free_in br2 - | RRec _ -> raise (UserError("",str "Not handled RRec")) - | RSort _ -> false - | RHole _ -> false - | RCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t - | RCast (_,b,CastCoerce) -> is_free_in b - | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) + | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GSort _ -> false + | GHole _ -> false + | GCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t + | GCast (_,b,CastCoerce) -> is_free_in b and is_free_in_br (_,ids,_,rt) = (not (List.mem id ids)) && is_free_in rt in @@ -425,7 +422,7 @@ let is_free_in id = let rec pattern_to_term = function | PatVar(loc,Anonymous) -> assert false | PatVar(loc,Name id) -> - mkRVar id + mkGVar id | PatCstr(loc,constr,patternl,_) -> let cst_narg = Inductiveops.mis_constructor_nargs_env @@ -436,13 +433,13 @@ let rec pattern_to_term = function Array.to_list (Array.init (cst_narg - List.length patternl) - (fun _ -> mkRHole ()) + (fun _ -> mkGHole ()) ) in let patl_as_term = List.map pattern_to_term patternl in - mkRApp(mkRRef(Libnames.ConstructRef constr), + mkGApp(mkGRef(Libnames.ConstructRef constr), implicit_args@patl_as_term ) @@ -451,69 +448,68 @@ let rec pattern_to_term = function let replace_var_by_term x_id term = let rec replace_var_by_pattern rt = match rt with - | RRef _ -> rt - | RVar(_,id) when id_ord id x_id == 0 -> term - | RVar _ -> rt - | REvar _ -> rt - | RPatVar _ -> rt - | RApp(loc,rt',rtl) -> - RApp(loc, + | GRef _ -> rt + | GVar(_,id) when id_ord id x_id == 0 -> term + | GVar _ -> rt + | GEvar _ -> rt + | GPatVar _ -> rt + | GApp(loc,rt',rtl) -> + GApp(loc, replace_var_by_pattern rt', List.map replace_var_by_pattern rtl ) - | RLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt - | RLambda(loc,name,k,t,b) -> - RLambda(loc, + | GLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt + | GLambda(loc,name,k,t,b) -> + GLambda(loc, name, k, replace_var_by_pattern t, replace_var_by_pattern b ) - | RProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt - | RProd(loc,name,k,t,b) -> - RProd(loc, + | GProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt + | GProd(loc,name,k,t,b) -> + GProd(loc, name, k, replace_var_by_pattern t, replace_var_by_pattern b ) - | RLetIn(_,Name id,_,_) when id_ord id x_id == 0 -> rt - | RLetIn(loc,name,def,b) -> - RLetIn(loc, + | GLetIn(_,Name id,_,_) when id_ord id x_id == 0 -> rt + | GLetIn(loc,name,def,b) -> + GLetIn(loc, name, replace_var_by_pattern def, replace_var_by_pattern b ) - | RLetTuple(_,nal,_,_,_) + | GLetTuple(_,nal,_,_,_) when List.exists (function Name id -> id = x_id | _ -> false) nal -> rt - | RLetTuple(loc,nal,(na,rto),def,b) -> - RLetTuple(loc, + | GLetTuple(loc,nal,(na,rto),def,b) -> + GLetTuple(loc, nal, (na,Option.map replace_var_by_pattern rto), replace_var_by_pattern def, replace_var_by_pattern b ) - | RCases(loc,sty,infos,el,brl) -> - RCases(loc,sty, + | GCases(loc,sty,infos,el,brl) -> + GCases(loc,sty, infos, List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el, List.map replace_var_by_pattern_br brl ) - | RIf(loc,b,(na,e_option),lhs,rhs) -> - RIf(loc, replace_var_by_pattern b, + | GIf(loc,b,(na,e_option),lhs,rhs) -> + GIf(loc, replace_var_by_pattern b, (na,Option.map replace_var_by_pattern e_option), replace_var_by_pattern lhs, replace_var_by_pattern rhs ) - | RRec _ -> raise (UserError("",str "Not handled RRec")) - | RSort _ -> rt - | RHole _ -> rt - | RCast(loc,b,CastConv(k,t)) -> - RCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t)) - | RCast(loc,b,CastCoerce) -> - RCast(loc,replace_var_by_pattern b,CastCoerce) - | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) + | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GSort _ -> rt + | GHole _ -> rt + | GCast(loc,b,CastConv(k,t)) -> + GCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t)) + | GCast(loc,b,CastCoerce) -> + GCast(loc,replace_var_by_pattern b,CastCoerce) and replace_var_by_pattern_br ((loc,idl,patl,res) as br) = if List.exists (fun id -> id_ord id x_id == 0) idl then br @@ -586,28 +582,28 @@ let id_of_name = function | Names.Name x -> x (* TODO: finish Rec caes *) -let ids_of_rawterm c = - let rec ids_of_rawterm acc c = +let ids_of_glob_constr c = + let rec ids_of_glob_constr acc c = let idof = id_of_name in match c with - | RVar (_,id) -> id::acc - | RApp (loc,g,args) -> - ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc - | RLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc - | RProd (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc - | RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc - | RCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc - | RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc - | RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc - | RLetTuple (_,nal,(na,po),b,c) -> - List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc - | RCases (loc,sty,rtntypopt,tml,brchl) -> - List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl) - | RRec _ -> failwith "Fix inside a constructor branch" - | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> [] + | GVar (_,id) -> id::acc + | GApp (loc,g,args) -> + ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc + | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc + | GProd (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc + | GLetIn (loc,na,b,c) -> idof na :: ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc + | GCast (loc,c,CastConv(k,t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc + | GCast (loc,c,CastCoerce) -> ids_of_glob_constr [] c @ acc + | GIf (loc,c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc + | GLetTuple (_,nal,(na,po),b,c) -> + List.map idof nal @ ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc + | GCases (loc,sty,rtntypopt,tml,brchl) -> + List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_glob_constr [] c) brchl) + | GRec _ -> failwith "Fix inside a constructor branch" + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> [] in (* build the set *) - List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_rawterm [] c) + List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_glob_constr [] c) @@ -616,59 +612,58 @@ let ids_of_rawterm c = 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, + | GRef _ -> rt + | GVar _ -> rt + | GEvar _ -> rt + | GPatVar _ -> rt + | GApp(loc,rt',rtl) -> + GApp(loc, zeta_normalize_term rt', List.map zeta_normalize_term rtl ) - | RLambda(loc,name,k,t,b) -> - RLambda(loc, + | GLambda(loc,name,k,t,b) -> + GLambda(loc, name, k, zeta_normalize_term t, zeta_normalize_term b ) - | RProd(loc,name,k,t,b) -> - RProd(loc, + | GProd(loc,name,k,t,b) -> + GProd(loc, name, k, zeta_normalize_term t, zeta_normalize_term b ) - | RLetIn(_,Name id,def,b) -> + | GLetIn(_,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, + | GLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b + | GLetTuple(loc,nal,(na,rto),def,b) -> + GLetTuple(loc, nal, (na,Option.map zeta_normalize_term rto), zeta_normalize_term def, zeta_normalize_term b ) - | RCases(loc,sty,infos,el,brl) -> - RCases(loc,sty, + | GCases(loc,sty,infos,el,brl) -> + GCases(loc,sty, 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, + | GIf(loc,b,(na,e_option),lhs,rhs) -> + GIf(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,CastConv(k,t)) -> - RCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t)) - | RCast(loc,b,CastCoerce) -> - RCast(loc,zeta_normalize_term b,CastCoerce) - | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) + | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GSort _ -> rt + | GHole _ -> rt + | GCast(loc,b,CastConv(k,t)) -> + GCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t)) + | GCast(loc,b,CastCoerce) -> + GCast(loc,zeta_normalize_term b,CastCoerce) and zeta_normalize_br (loc,idl,patl,res) = (loc,idl,patl,zeta_normalize_term res) in @@ -688,29 +683,28 @@ let expand_as = in let rec expand_as map rt = match rt with - | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ -> rt - | RVar(_,id) -> + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> rt + | GVar(_,id) -> begin try Idmap.find id map with Not_found -> rt end - | RApp(loc,f,args) -> RApp(loc,expand_as map f,List.map (expand_as map) args) - | RLambda(loc,na,k,t,b) -> RLambda(loc,na,k,expand_as map t, expand_as map b) - | RProd(loc,na,k,t,b) -> RProd(loc,na,k,expand_as map t, expand_as map b) - | RLetIn(loc,na,v,b) -> RLetIn(loc,na, expand_as map v,expand_as map b) - | RLetTuple(loc,nal,(na,po),v,b) -> - RLetTuple(loc,nal,(na,Option.map (expand_as map) po), + | GApp(loc,f,args) -> GApp(loc,expand_as map f,List.map (expand_as map) args) + | GLambda(loc,na,k,t,b) -> GLambda(loc,na,k,expand_as map t, expand_as map b) + | GProd(loc,na,k,t,b) -> GProd(loc,na,k,expand_as map t, expand_as map b) + | GLetIn(loc,na,v,b) -> GLetIn(loc,na, expand_as map v,expand_as map b) + | GLetTuple(loc,nal,(na,po),v,b) -> + GLetTuple(loc,nal,(na,Option.map (expand_as map) po), expand_as map v, expand_as map b) - | RIf(loc,e,(na,po),br1,br2) -> - RIf(loc,expand_as map e,(na,Option.map (expand_as map) po), + | GIf(loc,e,(na,po),br1,br2) -> + GIf(loc,expand_as map e,(na,Option.map (expand_as map) po), expand_as map br1, expand_as map br2) - | RRec _ -> error "Not handled RRec" - | RDynamic _ -> error "Not handled RDynamic" - | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t)) - | RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce) - | RCases(loc,sty,po,el,brl) -> - RCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, + | GRec _ -> error "Not handled GRec" + | GCast(loc,b,CastConv(kind,t)) -> GCast(loc,expand_as map b,CastConv(kind,expand_as map t)) + | GCast(loc,b,CastCoerce) -> GCast(loc,expand_as map b,CastCoerce) + | GCases(loc,sty,po,el,brl) -> + GCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) and expand_as_br map (loc,idl,cpl,rt) = (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt) diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli new file mode 100644 index 00000000..bfd15357 --- /dev/null +++ b/plugins/funind/glob_termops.mli @@ -0,0 +1,126 @@ +open Glob_term + +(* Ocaml 3.06 Map.S does not handle is_empty *) +val idmap_is_empty : 'a Names.Idmap.t -> bool + + +(* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *) +val get_pattern_id : cases_pattern -> Names.identifier list + +(* [pattern_to_term pat] returns a glob_constr corresponding to [pat]. + [pat] must not contain occurences of anonymous pattern +*) +val pattern_to_term : cases_pattern -> glob_constr + +(* + Some basic functions to rebuild glob_constr + In each of them the location is Util.dummy_loc +*) +val mkGRef : Libnames.global_reference -> glob_constr +val mkGVar : Names.identifier -> glob_constr +val mkGApp : glob_constr*(glob_constr list) -> glob_constr +val mkGLambda : Names.name * glob_constr * glob_constr -> glob_constr +val mkGProd : Names.name * glob_constr * glob_constr -> glob_constr +val mkGLetIn : Names.name * glob_constr * glob_constr -> glob_constr +val mkGCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr +val mkGSort : glob_sort -> glob_constr +val mkGHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *) +val mkGCast : glob_constr* glob_constr -> glob_constr +(* + Some basic functions to decompose glob_constrs + These are analogous to the ones constrs +*) +val glob_decompose_prod : glob_constr -> (Names.name*glob_constr) list * glob_constr +val glob_decompose_prod_or_letin : + glob_constr -> (Names.name*glob_constr option*glob_constr option) list * glob_constr +val glob_decompose_prod_n : int -> glob_constr -> (Names.name*glob_constr) list * glob_constr +val glob_decompose_prod_or_letin_n : int -> glob_constr -> + (Names.name*glob_constr option*glob_constr option) list * glob_constr +val glob_compose_prod : glob_constr -> (Names.name*glob_constr) list -> glob_constr +val glob_compose_prod_or_letin: glob_constr -> + (Names.name*glob_constr option*glob_constr option) list -> glob_constr +val glob_decompose_app : glob_constr -> glob_constr*(glob_constr list) + + +(* [glob_make_eq t1 t2] build the glob_constr corresponding to [t2 = t1] *) +val glob_make_eq : ?typ:glob_constr -> glob_constr -> glob_constr -> glob_constr +(* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *) +val glob_make_neq : glob_constr -> glob_constr -> glob_constr +(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *) +val glob_make_or : glob_constr -> glob_constr -> glob_constr + +(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding + to [P1 \/ ( .... \/ Pn)] +*) +val glob_make_or_list : glob_constr list -> glob_constr + + +(* alpha_conversion functions *) + + + +(* Replace the var mapped in the glob_constr/context *) +val change_vars : Names.identifier Names.Idmap.t -> glob_constr -> glob_constr + + + +(* [alpha_pat avoid pat] rename all the variables present in [pat] s.t. + the result does not share variables with [avoid]. This function create + a fresh variable for each occurence of the anonymous pattern. + + Also returns a mapping from old variables to new ones and the concatenation of + [avoid] with the variables appearing in the result. +*) + val alpha_pat : + Names.Idmap.key list -> + Glob_term.cases_pattern -> + Glob_term.cases_pattern * Names.Idmap.key list * + Names.identifier Names.Idmap.t + +(* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt + conventions and does not share bound variables with avoid +*) +val alpha_rt : Names.identifier list -> glob_constr -> glob_constr + +(* same as alpha_rt but for case branches *) +val alpha_br : Names.identifier list -> + Util.loc * Names.identifier list * Glob_term.cases_pattern list * + Glob_term.glob_constr -> + Util.loc * Names.identifier list * Glob_term.cases_pattern list * + Glob_term.glob_constr + + +(* Reduction function *) +val replace_var_by_term : + Names.identifier -> + Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr + + + +(* + [is_free_in id rt] checks if [id] is a free variable in [rt] +*) +val is_free_in : Names.identifier -> glob_constr -> bool + + +val are_unifiable : cases_pattern -> cases_pattern -> bool +val eq_cases_pattern : cases_pattern -> cases_pattern -> bool + + + +(* + ids_of_pat : cases_pattern -> Idset.t + returns the set of variables appearing in a pattern +*) +val ids_of_pat : cases_pattern -> Names.Idset.t + +(* TODO: finish this function (Fix not treated) *) +val ids_of_glob_constr: glob_constr -> Names.Idset.t + +(* + removing let_in construction in a glob_constr +*) +val zeta_normalize : Glob_term.glob_constr -> Glob_term.glob_constr + + +val expand_as : glob_constr -> glob_constr diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index a61671f8..8caeca57 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -4,7 +4,7 @@ open Term open Pp open Indfun_common open Libnames -open Rawterm +open Glob_term open Declarations let is_rec_info scheme_info = @@ -19,13 +19,11 @@ let is_rec_info scheme_info = 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 false else Tactics.new_destruct false - let functional_induction with_clean c princl pat = Dumpglob.pause (); let res = let f,args = decompose_app c in @@ -65,9 +63,8 @@ let functional_induction with_clean c princl pat = errorlabstrm "" (str "Cannot find induction principle for " ++Printer.pr_lconstr (mkConst c') ) in - (princ,Rawterm.NoBindings, Tacmach.pf_type_of g princ) + (princ,Glob_term.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 @@ -78,7 +75,7 @@ let functional_induction with_clean c princl pat = if princ_infos.Tactics.farg_in_concl then [c] else [] in - List.map (fun c -> Tacexpr.ElimOnConstr (c,NoBindings)) (args@c_list) + List.map (fun c -> Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))) (args@c_list) in let princ' = Some (princ,bindings) in let princ_vars = @@ -104,9 +101,9 @@ let functional_induction with_clean c princl pat = (Tacmach.pf_ids_of_hyps g) in let flag = - Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; + Glob_term.Cbv + {Glob_term.all_flags + with Glob_term.rDelta = false; } in Tacticals.tclTHEN @@ -114,7 +111,6 @@ let functional_induction with_clean c princl pat = (Hiddentac.h_reduce flag Tacticals.allHypsAndConcl) g else Tacticals.tclIDTAC g - in Tacticals.tclTHEN (choose_dest_or_ind @@ -129,56 +125,43 @@ let functional_induction with_clean c princl pat = Dumpglob.continue (); res - - - -type annot = - Struct of identifier - | Wf of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list - | Mes of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list - - -type newfixpoint_expr = - identifier * annot * Topconstr.local_binder list * Topconstr.constr_expr * Topconstr.constr_expr - -let rec abstract_rawconstr c = function +let rec abstract_glob_constr c = function | [] -> c - | Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_rawconstr c bl) + | Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_glob_constr c bl) | Topconstr.LocalRawAssum (idl,k,t)::bl -> List.fold_right (fun x b -> Topconstr.mkLambdaC([x],k,t,b)) idl - (abstract_rawconstr c bl) + (abstract_glob_constr c bl) let interp_casted_constr_with_implicits sigma env impls c = -(* Constrintern.interp_rawconstr_with_implicits sigma env [] impls c *) Constrintern.intern_gen false sigma env ~impls ~allow_patvar:false ~ltacvars:([],[]) c - (* - Construct a fixpoint as a Rawterm + Construct a fixpoint as a Glob_term and not as a constr *) + let build_newrecursive -(lnameargsardef) = + lnameargsardef = let env0 = Global.env() and sigma = Evd.empty in let (rec_sign,rec_impls) = List.fold_left - (fun (env,impls) ((_,recname),_,bl,arityc,_) -> + (fun (env,impls) ((_,recname),bl,arityc,_) -> let arityc = Topconstr.prod_constr_expr arityc bl in let arity = Constrintern.interp_type sigma env0 arityc in let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in - (Environ.push_named (recname,None,arity) env, (recname, impl) :: impls)) - (env0,[]) lnameargsardef in + (Environ.push_named (recname,None,arity) env, Idmap.add recname impl impls)) + (env0,Constrintern.empty_internalization_env) lnameargsardef in let recdef = (* Declare local notations *) let fs = States.freeze() in let def = try List.map - (fun (_,_,bl,_,def) -> - let def = abstract_rawconstr def bl in + (fun (_,bl,_,def) -> + let def = abstract_glob_constr def bl in interp_casted_constr_with_implicits sigma rec_sign rec_impls def ) @@ -189,34 +172,31 @@ let build_newrecursive in recdef,rec_impls - -let compute_annot (name,annot,args,types,body) = - let names = List.map snd (Topconstr.names_of_local_assums args) in - match annot with - | None -> - if List.length names > 1 then - user_err_loc - (dummy_loc,"Function", - Pp.str "the recursive argument needs to be specified"); - let new_annot = (id_of_name (List.hd names)) in - (name,Struct new_annot,args,types,body) - | Some r -> (name,r,args,types,body) - +let build_newrecursive l = + let l' = List.map + (fun ((fixna,_,bll,ar,body_opt),lnot) -> + match body_opt with + | Some body -> + (fixna,bll,ar,body) + | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") + ) l + in + build_newrecursive l' (* Checks whether or not the mutual bloc is recursive *) let rec is_rec names = let names = List.fold_right Idset.add names Idset.empty in let check_id id names = Idset.mem id names in let rec lookup names = function - | RVar(_,id) -> check_id id names - | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false - | RCast(_,b,_) -> lookup names b - | RRec _ -> error "RRec not handled" - | RIf(_,b,_,lhs,rhs) -> + | GVar(_,id) -> check_id id names + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false + | GCast(_,b,_) -> lookup names b + | GRec _ -> error "GRec not handled" + | GIf(_,b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) - | RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b) -> + | GLetIn(_,na,t,b) | GLambda(_,na,_,t,b) | GProd(_,na,_,t,b) -> lookup names t || lookup (Nameops.name_fold Idset.remove na names) b - | RLetTuple(_,nal,_,t,b) -> lookup names t || + | GLetTuple(_,nal,_,t,b) -> lookup names t || lookup (List.fold_left (fun acc na -> Nameops.name_fold Idset.remove na acc) @@ -224,8 +204,8 @@ let rec is_rec names = nal ) b - | RApp(_,f,args) -> List.exists (lookup names) (f::args) - | RCases(_,_,_,el,brl) -> + | GApp(_,f,args) -> List.exists (lookup names) (f::args) + | GCases(_,_,_,el,brl) -> List.exists (fun (e,_) -> lookup names e) el || List.exists (lookup_br names) brl and lookup_br names (_,idl,_,rt) = @@ -240,9 +220,9 @@ let rec local_binders_length = function | Topconstr.LocalRawDef _::bl -> 1 + local_binders_length bl | Topconstr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl -let prepare_body (name,annot,args,types,body) rt = +let prepare_body ((name,_,args,types,_),_) rt = let n = local_binders_length args in -(* Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_rawconstr rt); *) +(* Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_glob_constr rt); *) let fun_args,rt' = chop_rlambda_n n rt in (fun_args,rt') @@ -251,7 +231,7 @@ let derive_inversion fix_names = try (* we first transform the fix_names identifier into their corresponding constant *) let fix_names_as_constant = - List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names + List.map (fun id -> destConst (Constrintern.global_reference id)) fix_names in (* Then we check that the graphs have been defined @@ -268,20 +248,22 @@ let derive_inversion fix_names = Ensures by : register_built i*) (List.map - (fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id))) + (fun id -> destInd (Constrintern.global_reference (mk_rel_id id))) fix_names ) with e -> + let e' = Cerrors.process_vernac_interp_error e in msg_warning - (str "Cannot built inversion information" ++ - if do_observe () then Cerrors.explain_exn e else mt ()) + (str "Cannot build inversion information" ++ + if do_observe () then (fnl() ++ Errors.print e') else mt ()) with _ -> () let warning_error names e = + let e = Cerrors.process_vernac_interp_error e in let e_explain e = match e with - | ToShow e -> spc () ++ Cerrors.explain_exn e - | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt () + | ToShow e -> spc () ++ Errors.print e + | _ -> if do_observe () then (spc () ++ Errors.print e) else mt () in match e with | Building_graph e -> @@ -297,10 +279,11 @@ let warning_error names e = | _ -> raise e let error_error names e = + let e = Cerrors.process_vernac_interp_error e in let e_explain e = match e with - | ToShow e -> spc () ++ Cerrors.explain_exn e - | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt () + | ToShow e -> spc () ++ Errors.print e + | _ -> if do_observe () then (spc () ++ Errors.print e) else mt () in match e with | Building_graph e -> @@ -311,16 +294,16 @@ let error_error names e = | _ -> raise e let generate_principle on_error - is_general do_built fix_rec_l recdefs interactive_proof + is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof (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 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 - let funs_types = List.map (function (_,_,_,types,_) -> types) fix_rec_l in + let funs_types = List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in try (* We then register the Inductive graphs of the functions *) - Rawterm_to_relation.build_inductive names funs_args funs_types recdefs; + Glob_term_to_relation.build_inductive names funs_args funs_types recdefs; if do_built then begin @@ -334,7 +317,7 @@ let generate_principle on_error locate_ind f_R_mut) in - let fname_kn (fname,_,_,_,_) = + let fname_kn ((fname,_,_,_,_),_) = let f_ref = Ident fname in locate_with_msg (pr_reference f_ref++str ": Not an inductive type!") @@ -366,21 +349,18 @@ let generate_principle on_error with e -> on_error names e -let register_struct is_rec fixpoint_exprl = +let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = match fixpoint_exprl with | [((_,fname),_,bl,ret_type,body),_] when not is_rec -> + let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in let ce,imps = - Command.interp_definition - (Flags.boxed_definitions ()) bl None body (Some ret_type) + Command.interp_definition bl None body (Some ret_type) in Command.declare_definition fname (Decl_kinds.Global,Decl_kinds.Definition) ce imps (fun _ _ -> ()) | _ -> - let fixpoint_exprl = - List.map (fun ((name,annot,bl,types,body),ntn) -> - ((name,annot,bl,types,Some body),ntn)) fixpoint_exprl in - Command.do_fixpoint fixpoint_exprl (Flags.boxed_definitions()) + Command.do_fixpoint fixpoint_exprl let generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation @@ -402,8 +382,8 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas in match wf_arg with | None -> - if List.length names = 1 then 1 - else error "Recursive argument must be specified" + if List.length names = 1 then 1 + else error "Recursive argument must be specified" | Some wf_arg -> list_index (Name wf_arg) names in @@ -447,7 +427,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas using_lemmas -let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type body = +let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas args ret_type body = let wf_arg_type,wf_arg = match wf_arg with | None -> @@ -473,28 +453,186 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b | _ -> assert false with Not_found -> assert false in - let ltof = - let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in - Libnames.Qualid (dummy_loc,Libnames.qualid_of_path - (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (id_of_string "ltof"))) - in - let fun_from_mes = - let applied_mes = - Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg]) in - Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],Topconstr.default_binder_kind,wf_arg_type,applied_mes) - in - let wf_rel_from_mes = - Topconstr.mkAppC(Topconstr.mkRefC ltof,[wf_arg_type;fun_from_mes]) - in - register_wf ~is_mes:true fname rec_impls wf_rel_from_mes (Some wf_arg) + let wf_rel_from_mes,is_mes = + match wf_rel_expr_opt with + | None -> + let ltof = + let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in + Libnames.Qualid (dummy_loc,Libnames.qualid_of_path + (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (id_of_string "ltof"))) + in + let fun_from_mes = + let applied_mes = + Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg]) in + Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],Topconstr.default_binder_kind,wf_arg_type,applied_mes) + in + let wf_rel_from_mes = + Topconstr.mkAppC(Topconstr.mkRefC ltof,[wf_arg_type;fun_from_mes]) + in + wf_rel_from_mes,true + | Some wf_rel_expr -> + let wf_rel_with_mes = + let a = Names.id_of_string "___a" in + let b = Names.id_of_string "___b" in + Topconstr.mkLambdaC( + [dummy_loc,Name a;dummy_loc,Name b], + Topconstr.Default Lib.Explicit, + wf_arg_type, + Topconstr.mkAppC(wf_rel_expr, + [ + Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC a]); + Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC b]) + ]) + ) + in + wf_rel_with_mes,false + in + register_wf ~is_mes:is_mes fname rec_impls wf_rel_from_mes (Some wf_arg) using_lemmas args ret_type body +let map_option f = function + | None -> None + | Some v -> Some (f v) + +let decompose_lambda_n_assum_constr_expr = + let rec decompose_lambda_n_assum_constr_expr acc n e = + if n = 0 then (List.rev acc,e) + else + match e with + | Topconstr.CLambdaN(_, [],e') -> decompose_lambda_n_assum_constr_expr acc n e' + | Topconstr.CLambdaN(lambda_loc,(nal,bk,nal_type)::bl,e') -> + let nal_length = List.length nal in + if nal_length <= n + then + decompose_lambda_n_assum_constr_expr + (Topconstr.LocalRawAssum(nal,bk,nal_type)::acc) + (n - nal_length) + (Topconstr.CLambdaN(lambda_loc,bl,e')) + else + let nal_keep,nal_expr = list_chop n nal in + (List.rev (Topconstr.LocalRawAssum(nal_keep,bk,nal_type)::acc), + Topconstr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e') + ) + | Topconstr.CLetIn(_, na,nav,e') -> + decompose_lambda_n_assum_constr_expr + (Topconstr.LocalRawDef(na,nav)::acc) (pred n) e' + | _ -> error "Not enough product or assumption" + in + decompose_lambda_n_assum_constr_expr [] + +let decompose_prod_n_assum_constr_expr = + let rec decompose_prod_n_assum_constr_expr acc n e = + (* Pp.msgnl (str "n := " ++ int n ++ fnl ()++ *) + (* str "e := " ++ Ppconstr.pr_lconstr_expr e); *) + if n = 0 then + (* let _ = Pp.msgnl (str "return_type := " ++ Ppconstr.pr_lconstr_expr e) in *) + (List.rev acc,e) + else + match e with + | Topconstr.CProdN(_, [],e') -> decompose_prod_n_assum_constr_expr acc n e' + | Topconstr.CProdN(lambda_loc,(nal,bk,nal_type)::bl,e') -> + let nal_length = List.length nal in + if nal_length <= n + then + (* let _ = Pp.msgnl (str "first case") in *) + decompose_prod_n_assum_constr_expr + (Topconstr.LocalRawAssum(nal,bk,nal_type)::acc) + (n - nal_length) + (if bl = [] then e' else (Topconstr.CLambdaN(lambda_loc,bl,e'))) + else + (* let _ = Pp.msgnl (str "second case") in *) + let nal_keep,nal_expr = list_chop n nal in + (List.rev (Topconstr.LocalRawAssum(nal_keep,bk,nal_type)::acc), + Topconstr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e') + ) + | Topconstr.CArrow(_,premisse,concl) -> + (* let _ = Pp.msgnl (str "arrow case") in *) + decompose_prod_n_assum_constr_expr + (Topconstr.LocalRawAssum([dummy_loc,Names.Anonymous], + Topconstr.Default Lib.Explicit,premisse) + ::acc) + (pred n) + concl + | Topconstr.CLetIn(_, na,nav,e') -> + decompose_prod_n_assum_constr_expr + (Topconstr.LocalRawDef(na,nav)::acc) (pred n) e' + | _ -> error "Not enough product or assumption" + in + decompose_prod_n_assum_constr_expr [] -let do_generate_principle on_error register_built interactive_proof fixpoint_exprl = - let recdefs,rec_impls = build_newrecursive fixpoint_exprl in +open Topconstr + +let id_of_name = function + | Name id -> id + | _ -> assert false + + let rec rebuild_bl (aux,assoc) bl typ = + match bl,typ with + | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc) + | (Topconstr.LocalRawAssum(nal,bk,_))::bl',typ -> + rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ + | (Topconstr.LocalRawDef(na,_))::bl',CLetIn(_,_,nat,typ') -> + rebuild_bl ((Topconstr.LocalRawDef(na,replace_vars_constr_expr assoc nat)::aux),assoc) + bl' typ' + | _ -> assert false + and rebuild_nal (aux,assoc) bk bl' nal lnal typ = + match nal,typ with + | [], _ -> rebuild_bl (aux,assoc) bl' typ + | na::nal,CArrow(_,nat,typ') -> + rebuild_nal + ((LocalRawAssum([na],bk,replace_vars_constr_expr assoc nat))::aux,assoc) + bk bl' nal (pred lnal) typ' + | _,CProdN(_,[],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ + | _,CProdN(_,(nal',bk',nal't)::rest,typ') -> + let lnal' = List.length nal' in + if lnal' >= lnal + then + let old_nal',new_nal' = list_chop lnal nal' in + rebuild_bl ((LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't)::aux),(List.rev_append (List.combine (List.map id_of_name (List.map snd old_nal')) (List.map id_of_name (List.map snd nal))) assoc)) bl' + (if new_nal' = [] && rest = [] + then typ' + else if new_nal' = [] + then CProdN(dummy_loc,rest,typ') + else CProdN(dummy_loc,((new_nal',bk',nal't)::rest),typ')) + else + let captured_nal,non_captured_nal = list_chop lnal' nal in + rebuild_nal ((LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't)::aux), (List.rev_append (List.combine (List.map id_of_name (List.map snd captured_nal)) ((List.map id_of_name (List.map snd nal)))) assoc)) + bk bl' non_captured_nal (lnal - lnal') (CProdN(dummy_loc,rest,typ')) + | _ -> assert false + +let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ + +let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = + let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in + let ((_,_,typel),_) = Command.interp_fixpoint fixl ntns in + let constr_expr_typel = + with_full_print (List.map (Constrextern.extern_constr false (Global.env ()))) typel in + let fixpoint_exprl_with_new_bl = + List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> + + let new_bl',new_ret_type,_ = rebuild_bl ([],[]) bl fix_typ in + (((lna,(rec_arg_opt,rec_order),new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) + ) + fixpoint_exprl constr_expr_typel + in + fixpoint_exprl_with_new_bl + + +let do_generate_principle on_error register_built interactive_proof + (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) :unit = + List.iter (fun (_,l) -> if l <> [] then error "Function does not support notations for now") fixpoint_exprl; let _is_struct = match fixpoint_exprl with - | [(((_,name),Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] -> + | [((_,(wf_x,Topconstr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] -> + let ((((_,name),_,args,types,body)),_) as fixpoint_expr = + match recompute_binder_list [fixpoint_expr] with + | [e] -> e + | _ -> assert false + in + let fixpoint_exprl = [fixpoint_expr] in + let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let using_lemmas = [] in let pre_hook = generate_principle on_error @@ -505,9 +643,18 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp true in if register_built - then register_wf name rec_impls wf_rel wf_x using_lemmas args types body pre_hook; + then register_wf name rec_impls wf_rel (map_option snd wf_x) using_lemmas args types body pre_hook; false - | [(((_,name),Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] -> + |[((_,(wf_x,Topconstr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] -> + let ((((_,name),_,args,types,body)),_) as fixpoint_expr = + match recompute_binder_list [fixpoint_expr] with + | [e] -> e + | _ -> assert false + in + let fixpoint_exprl = [fixpoint_expr] in + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let using_lemmas = [] in + let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in let pre_hook = generate_principle on_error @@ -518,56 +665,35 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp true in if register_built - then register_mes name rec_impls wf_mes wf_x using_lemmas args types body pre_hook; + then register_mes name rec_impls wf_mes wf_rel_opt (map_option snd wf_x) using_lemmas args types body pre_hook; true | _ -> - let fix_names = - List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl - in - let is_one_rec = is_rec fix_names in - let old_fixpoint_exprl = - List.map - (function - | (name,Some (Struct id),args,types,body),_ -> - let annot = - try Some (dummy_loc, id), Topconstr.CStructRec - with Not_found -> - raise (UserError("",str "Cannot find argument " ++ - Ppconstr.pr_id id)) - in - (name,annot,args,types,body),([]:Vernacexpr.decl_notation list) - | (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 - user_err_loc - (dummy_loc,"Function", - Pp.str "the recursive argument needs to be specified in Function") - else - let loc, na = List.hd names in - (name,(Some (loc, Nameops.out_name na), Topconstr.CStructRec),args,types,body), - ([]:Vernacexpr.decl_notation list) - | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> - error - ("Cannot use mutual definition with well-founded recursion or measure") - ) - (List.combine fixpoint_exprl recdefs) - in + List.iter (function ((_na,(_,ord),_args,_body,_type),_not) -> + match ord with + | Topconstr.CMeasureRec _ | Topconstr.CWfRec _ -> + error + ("Cannot use mutual definition with well-founded recursion or measure") + | _ -> () + ) + fixpoint_exprl; + let fixpoint_exprl = recompute_binder_list fixpoint_exprl in + let fix_names = + List.map (function (((_,name),_,_,_,_),_) -> name) fixpoint_exprl + in (* ok all the expressions are structural *) - let fix_names = - List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl - in - let is_rec = List.exists (is_rec fix_names) recdefs in - if register_built then register_struct is_rec old_fixpoint_exprl; - generate_principle - on_error - false - register_built - fixpoint_exprl - recdefs - interactive_proof - (Functional_principles_proofs.prove_princ_for_struct interactive_proof); - if register_built then derive_inversion fix_names; - true; + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let is_rec = List.exists (is_rec fix_names) recdefs in + if register_built then register_struct is_rec fixpoint_exprl; + generate_principle + on_error + false + register_built + fixpoint_exprl + recdefs + interactive_proof + (Functional_principles_proofs.prove_princ_for_struct interactive_proof); + if register_built then derive_inversion fix_names; + true; in () @@ -638,7 +764,6 @@ let rec add_args id new_args b = | CGeneralization _ -> anomaly "add_args : CGeneralization" | CPrim _ -> b | CDelimiters _ -> anomaly "add_args : CDelimiters" - | CDynamic _ -> anomaly "add_args : CDynamic" exception Stop of Topconstr.constr_expr @@ -701,75 +826,71 @@ let rec get_args b t : Topconstr.local_binder list * 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") ) - + 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 - Dumpglob.pause (); - (match c_body.const_body with - | None -> error "Cannot build a graph over an axiom !" - | Some b -> - let env = Global.env () in - let body = (force b) in - let extern_body,extern_type = - with_full_print - (fun () -> - (Constrextern.extern_constr false env body, - Constrextern.extern_type false env - (Typeops.type_of_constant_type env c_body.const_type) - ) - ) - () - in - let (nal_tas,b,t) = get_args extern_body extern_type in - let expr_list = - match b with - | Topconstr.CFix(loc,l_id,fixexprl) -> - let l = - List.map - (fun (id,(n,recexp),bl,t,b) -> - let loc, rec_id = Option.get n in - let new_args = - List.flatten - (List.map - (function - | Topconstr.LocalRawDef (na,_)-> [] - | Topconstr.LocalRawAssum (nal,_,_) -> - List.map - (fun (loc,n) -> - CRef(Libnames.Ident(loc, Nameops.out_name n))) - nal - ) - nal_tas - ) - in - let b' = add_args (snd id) new_args b in - (id, Some (Struct rec_id),nal_tas@bl,t,b') - ) - fixexprl - in - l - | _ -> - let id = id_of_label (con_label c) in - [((dummy_loc,id),None,nal_tas,t,b)] - in - do_generate_principle error_error false false expr_list; - (* We register the infos *) - let mp,dp,_ = repr_con c in - List.iter - (fun ((_,id),_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id))) - expr_list); + Dumpglob.pause (); + (match body_of_constant c_body with + | None -> error "Cannot build a graph over an axiom !" + | Some b -> + let env = Global.env () in + let body = (force b) in + let extern_body,extern_type = + with_full_print + (fun () -> + (Constrextern.extern_constr false env body, + Constrextern.extern_type false env + (Typeops.type_of_constant_type env c_body.const_type) + ) + ) + () + in + let (nal_tas,b,t) = get_args extern_body extern_type in + let expr_list = + match b with + | Topconstr.CFix(loc,l_id,fixexprl) -> + let l = + List.map + (fun (id,(n,recexp),bl,t,b) -> + let loc, rec_id = Option.get n in + let new_args = + List.flatten + (List.map + (function + | Topconstr.LocalRawDef (na,_)-> [] + | Topconstr.LocalRawAssum (nal,_,_) -> + List.map + (fun (loc,n) -> + CRef(Libnames.Ident(loc, Nameops.out_name n))) + nal + ) + nal_tas + ) + in + let b' = add_args (snd id) new_args b in + (((id, ( Some (dummy_loc,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) + ) + fixexprl + in + l + | _ -> + let id = id_of_label (con_label c) in + [((dummy_loc,id),(None,Topconstr.CStructRec),nal_tas,t,Some b),[]] + in + do_generate_principle error_error false false expr_list; + (* We register the infos *) + let mp,dp,_ = repr_con c in + List.iter + (fun (((_,id),_,_,_,_),_) -> add_Function false (make_con mp dp (label_of_id id))) + expr_list); Dumpglob.continue () - -(* let make_graph _ = assert false *) - let do_generate_principle = do_generate_principle warning_error true diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli new file mode 100644 index 00000000..e65b5808 --- /dev/null +++ b/plugins/funind/indfun.mli @@ -0,0 +1,24 @@ +open Util +open Names +open Term +open Pp +open Indfun_common +open Libnames +open Glob_term +open Declarations + +val do_generate_principle : + bool -> + (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> + unit + + +val functional_induction : + bool -> + Term.constr -> + (Term.constr * Term.constr Glob_term.bindings) option -> + Genarg.intro_pattern_expr Util.located option -> + Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma + + +val make_graph : Libnames.global_reference -> unit diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 0f048f59..dd475315 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -76,8 +76,8 @@ let chop_rlambda_n = then List.rev acc,rt else match rt with - | Rawterm.RLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b - | Rawterm.RLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b + | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b + | Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b | _ -> raise (Util.UserError("chop_rlambda_n", str "chop_rlambda_n: Not enough Lambdas")) @@ -90,7 +90,7 @@ let chop_rprod_n = then List.rev acc,rt else match rt with - | Rawterm.RProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b + | Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b | _ -> raise (Util.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products")) in chop_prod_n [] @@ -120,9 +120,9 @@ let const_of_id id = let def_of_const t = match (Term.kind_of_term t) with Term.Const sp -> - (try (match (Global.lookup_constant sp) with - {Declarations.const_body=Some c} -> Declarations.force c - |_ -> assert false) + (try (match Declarations.body_of_constant (Global.lookup_constant sp) with + | Some c -> Declarations.force c + | _ -> assert false) with _ -> assert false) |_ -> assert false @@ -158,6 +158,7 @@ let definition_message id = let save with_clean id const (locality,kind) hook = let {const_entry_body = pft; + const_entry_secctx = _; const_entry_type = tpo; const_entry_opaque = opacity } = const in let l,r = match locality with @@ -180,48 +181,9 @@ let save with_clean id const (locality,kind) hook = - -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 cook_proof _ = + let (id,(entry,_,strength,hook)) = Pfedit.cook_proof (fun _ -> ()) in + (id,(entry,strength,hook)) let new_save_named opacity = let id,(const,persistence,hook) = cook_proof true in @@ -401,7 +363,7 @@ let pr_table tb = let l = Cmap.fold (fun k v acc -> v::acc) tb [] in Util.prlist_with_sep fnl pr_info l -let in_Function,out_Function = +let in_Function : function_info -> Libobject.obj = Libobject.declare_object {(Libobject.default_object "FUNCTIONS_DB") with Libobject.cache_function = cache_Function; @@ -490,6 +452,7 @@ open Goptions let functional_induction_rewrite_dependent_proofs_sig = { optsync = false; + optdepr = false; optname = "Functional Induction Rewrite Dependent"; optkey = ["Functional";"Induction";"Rewrite";"Dependent"]; optread = (fun () -> !functional_induction_rewrite_dependent_proofs); @@ -502,6 +465,7 @@ let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = t let function_debug_sig = { optsync = false; + optdepr = false; optname = "Function debug"; optkey = ["Function_debug"]; optread = (fun () -> !function_debug); @@ -521,6 +485,7 @@ let is_strict_tcc () = !strict_tcc let strict_tcc_sig = { optsync = false; + optdepr = false; optname = "Raw Function Tcc"; optkey = ["Function_raw_tcc"]; optread = (fun () -> !strict_tcc); diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 6f6607fc..e0076735 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -35,11 +35,11 @@ val list_union_eq : val list_add_set_eq : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list -val chop_rlambda_n : int -> Rawterm.rawconstr -> - (name*Rawterm.rawconstr*bool) list * Rawterm.rawconstr +val chop_rlambda_n : int -> Glob_term.glob_constr -> + (name*Glob_term.glob_constr*bool) list * Glob_term.glob_constr -val chop_rprod_n : int -> Rawterm.rawconstr -> - (name*Rawterm.rawconstr) list * Rawterm.rawconstr +val chop_rprod_n : int -> Glob_term.glob_constr -> + (name*Glob_term.glob_constr) list * Glob_term.glob_constr val def_of_const : Term.constr -> Term.constr val eq : Term.constr Lazy.t @@ -50,15 +50,8 @@ val jmeq_refl : unit -> Term.constr (* [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 -> diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index aa42f6cd..0b04a572 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,7 +16,6 @@ open Tacticals open Tactics open Indfun_common open Tacmach -open Termops open Sign open Hiddentac @@ -24,17 +23,17 @@ open Hiddentac 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) + | loc, Glob_term.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) + | loc, Glob_term.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) let pr_bindings prc prlc = function - | Rawterm.ImplicitBindings l -> + | Glob_term.ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ Util.prlist_with_sep spc prc l - | Rawterm.ExplicitBindings l -> + | Glob_term.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 () + | Glob_term.NoBindings -> mt () let pr_with_bindings prc prlc (c,bl) = @@ -60,12 +59,13 @@ let observennl strm = let do_observe_tac s tac g = - let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in + let goal = begin try (Printer.pr_goal g) with _ -> assert false end in try let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v with e -> + let e' = Cerrors.process_vernac_interp_error e in msgnl (str "observation "++ s++str " raised exception " ++ - Cerrors.explain_exn e ++ str " on goal " ++ goal ); + Errors.print e' ++ str " on goal " ++ goal ); raise e;; @@ -84,7 +84,7 @@ let nf_zeta = (* [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 + Constrintern.global_reference id with Not_found -> raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id)) @@ -248,7 +248,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem | [] | [_] | [_;_] -> anomaly "bad context" | hres::res::(x,_,t)::ctxt -> Termops.it_mkLambda_or_LetIn - ~init:(Termops.it_mkProd_or_LetIn ~init:concl [hres;res]) + (Termops.it_mkProd_or_LetIn concl [hres;res]) ((x,None,t)::ctxt) ) lemmas_types_infos @@ -313,7 +313,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem | None -> (id::pre_args,pre_tac) | Some b -> (pre_args, - tclTHEN (h_reduce (Rawterm.Unfold([Rawterm.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac + tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac ) else (pre_args,pre_tac) @@ -395,10 +395,10 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem observe_tac "unfolding" pre_tac; (* $zeta$ normalizing of the conclusion *) h_reduce - (Rawterm.Cbv - { Rawterm.all_flags with - Rawterm.rDelta = false ; - Rawterm.rConst = [] + (Glob_term.Cbv + { Glob_term.all_flags with + Glob_term.rDelta = false ; + Glob_term.rConst = [] } ) onConcl; @@ -424,7 +424,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Namegen.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid + (dummy_loc,Glob_term.NamedHyp id,p)::bindings,id::avoid ) ([],pf_ids_of_hyps g) princ_infos.params @@ -434,12 +434,12 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.rev (fst (List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Namegen.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Rawterm.NamedHyp id,(nf_zeta p))::bindings,id::avoid) + (dummy_loc,Glob_term.NamedHyp id,(nf_zeta p))::bindings,id::avoid) ([],avoid) princ_infos.predicates (lemmas))) in - Rawterm.ExplicitBindings (params_bindings@lemmas_bindings) + Glob_term.ExplicitBindings (params_bindings@lemmas_bindings) in tclTHENSEQ [ observe_tac "intro args_names" (tclMAP h_intro args_names); @@ -526,15 +526,15 @@ and intros_with_rewrite_aux : tactic = Tauto.tauto g | Case(_,_,v,_) -> tclTHENSEQ[ - h_case false (v,Rawterm.NoBindings); + h_case false (v,Glob_term.NoBindings); intros_with_rewrite ] g | LetIn _ -> tclTHENSEQ[ h_reduce - (Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; + (Glob_term.Cbv + {Glob_term.all_flags + with Glob_term.rDelta = false; }) onConcl ; @@ -547,9 +547,9 @@ and intros_with_rewrite_aux : tactic = | LetIn _ -> tclTHENSEQ[ h_reduce - (Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; + (Glob_term.Cbv + {Glob_term.all_flags + with Glob_term.rDelta = false; }) onConcl ; @@ -563,7 +563,7 @@ let rec reflexivity_with_destruct_cases g = match kind_of_term (snd (destApp (pf_concl g))).(2) with | Case(_,_,v,_) -> tclTHENSEQ[ - h_case false (v,Rawterm.NoBindings); + h_case false (v,Glob_term.NoBindings); intros; observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases ] @@ -636,7 +636,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = *) let lemmas = Array.map - (fun (_,(ctxt,concl)) -> nf_zeta (Termops.it_mkLambda_or_LetIn ~init:concl ctxt)) + (fun (_,(ctxt,concl)) -> nf_zeta (Termops.it_mkLambda_or_LetIn concl ctxt)) lemmas_types_infos in (* We get the constant and the principle corresponding to this lemma *) @@ -686,16 +686,16 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = 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; + (Glob_term.Cbv + {Glob_term.all_flags + with Glob_term.rDelta = false; }) onConcl ; h_generalize (List.map mkVar ids); thin ids ] - else unfold_in_concl [(all_occurrences,Names.EvalConstRef (destConst f))] + else unfold_in_concl [(Termops.all_occurrences, Names.EvalConstRef (destConst f))] in (* The proof of each branche itself *) let ind_number = ref 0 in @@ -733,7 +733,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = (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 false (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings))))) + (observe_tac "elim" ((elim false (mkVar hres,Glob_term.NoBindings) (Some (mkVar graph_principle_id,Glob_term.NoBindings))))) (fun i g -> observe_tac "prove_branche" (prove_branche i) g )) ] g @@ -763,7 +763,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g 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 = Termops.it_mkProd_or_LetIn 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 @@ -784,7 +784,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g (fun entry -> (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type ) ) - (make_scheme (array_map_to_list (fun const -> const,Rawterm.RType None) funs)) + (make_scheme (array_map_to_list (fun const -> const,Glob_term.GType None) funs)) ) in let proving_tac = @@ -806,7 +806,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g 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))) + correctness_lemma = Some (destConst (Constrintern.global_reference (mk_correct_id f_id))) } ) @@ -818,7 +818,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g 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 = Termops.it_mkProd_or_LetIn 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 @@ -858,7 +858,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g 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))) + completeness_lemma = Some (destConst (Constrintern.global_reference (mk_complete_id f_id))) } ) funs; @@ -955,7 +955,7 @@ let functional_inversion kn hid fconst f_correct : tactic = h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]; thin [hid]; h_intro hid; - Inv.inv FullInversion None (Rawterm.NamedHyp hid); + Inv.inv FullInversion None (Glob_term.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 diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 40ee116d..4eedf8dc 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,6 @@ (* Merging of induction principles. *) -(*i $Id: i*) open Libnames open Tactics open Indfun_common @@ -21,12 +20,12 @@ open Term open Termops open Declarations open Environ -open Rawterm -open Rawtermops +open Glob_term +open Glob_termops (** {1 Utilities} *) -(** {2 Useful operations on constr and rawconstr} *) +(** {2 Useful operations on constr and glob_constr} *) let rec popn i c = if i<=0 then c else pop (popn (i-1) c) @@ -61,7 +60,7 @@ let string_of_name nme = string_of_id (id_of_name nme) (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *) let isVarf f x = match x with - | RVar (_,x) -> Pervasives.compare x f = 0 + | GVar (_,x) -> Pervasives.compare x f = 0 | _ -> false (** [ident_global_exist id] returns true if identifier [id] is linked @@ -98,7 +97,7 @@ let prNamedConstr s c = let prNamedRConstr s c = begin msg(str ""); - msg(str(s^" {§ ") ++ Printer.pr_rawconstr c ++ str " §} "); + msg(str(s^" {§ ") ++ Printer.pr_glob_constr c ++ str " §} "); msg(str ""); end let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc @@ -130,7 +129,7 @@ let prNamedRLDecl s lc = end let showind (id:identifier) = - let cstrid = Tacinterp.constr_of_id (Global.env()) id in + let cstrid = Constrintern.global_reference id in let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in List.iter (fun (nm, optcstr, tp) -> @@ -378,15 +377,15 @@ let verify_inds mib1 mib2 = let build_raw_params prms_decl avoid = let dummy_constr = compose_prod (List.map (fun (x,_,z) -> x,z) prms_decl) (mkRel 1) in let _ = prNamedConstr "DUMMY" dummy_constr in - let dummy_rawconstr = Detyping.detype false avoid [] dummy_constr in - let _ = prNamedRConstr "RAWDUMMY" dummy_rawconstr in - let res,_ = raw_decompose_prod dummy_rawconstr in + let dummy_glob_constr = Detyping.detype false avoid [] dummy_constr in + let _ = prNamedRConstr "RAWDUMMY" dummy_glob_constr in + let res,_ = glob_decompose_prod dummy_glob_constr in let comblist = List.combine prms_decl res in - comblist, res , (avoid @ (Idset.elements (ids_of_rawterm dummy_rawconstr))) + comblist, res , (avoid @ (Idset.elements (ids_of_glob_constr dummy_glob_constr))) *) let ids_of_rawlist avoid rawl = - List.fold_left Idset.union avoid (List.map ids_of_rawterm rawl) + List.fold_left Idset.union avoid (List.map ids_of_glob_constr rawl) @@ -464,7 +463,7 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array ([],[],[],[]) arity_ctxt in (* let arity_ctxt2 = build_raw_params oib2.mind_arity_ctxt - (Idset.elements (ids_of_rawterm oib1.mind_arity_ctxt)) in*) + (Idset.elements (ids_of_glob_constr oib1.mind_arity_ctxt)) in*) let recprms1,otherprms1,args1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in let _ = prstr "\n\n\n" in let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in @@ -512,37 +511,37 @@ exception NoMerge let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in match c1 , c2 with - | RApp(_,f1, arr1), RApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> + | GApp(_,f1, arr1), GApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> let _ = prstr "\nICI1!\n";Pp.flush_all() in let args = filter_shift_stable lnk (arr1 @ arr2) in - RApp (dummy_loc,RVar (dummy_loc,shift.ident) , args) - | RApp(_,f1, arr1), RApp(_,f2,arr2) -> raise NoMerge - | RLetIn(_,nme,bdy,trm) , _ -> + GApp (dummy_loc,GVar (dummy_loc,shift.ident) , args) + | GApp(_,f1, arr1), GApp(_,f2,arr2) -> raise NoMerge + | GLetIn(_,nme,bdy,trm) , _ -> let _ = prstr "\nICI2!\n";Pp.flush_all() in let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in - RLetIn(dummy_loc,nme,bdy,newtrm) - | _, RLetIn(_,nme,bdy,trm) -> + GLetIn(dummy_loc,nme,bdy,newtrm) + | _, GLetIn(_,nme,bdy,trm) -> let _ = prstr "\nICI3!\n";Pp.flush_all() in let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in - RLetIn(dummy_loc,nme,bdy,newtrm) + GLetIn(dummy_loc,nme,bdy,newtrm) | _ -> let _ = prstr "\nICI4!\n";Pp.flush_all() in raise NoMerge let rec merge_app_unsafe c1 c2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in match c1 , c2 with - | RApp(_,f1, arr1), RApp(_,f2,arr2) -> + | GApp(_,f1, arr1), GApp(_,f2,arr2) -> let args = filter_shift_stable lnk (arr1 @ arr2) in - RApp (dummy_loc,RVar(dummy_loc,shift.ident) , args) + GApp (dummy_loc,GVar(dummy_loc,shift.ident) , args) (* FIXME: what if the function appears in the body of the let? *) - | RLetIn(_,nme,bdy,trm) , _ -> + | GLetIn(_,nme,bdy,trm) , _ -> let _ = prstr "\nICI2 '!\n";Pp.flush_all() in let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in - RLetIn(dummy_loc,nme,bdy,newtrm) - | _, RLetIn(_,nme,bdy,trm) -> + GLetIn(dummy_loc,nme,bdy,newtrm) + | _, GLetIn(_,nme,bdy,trm) -> let _ = prstr "\nICI3 '!\n";Pp.flush_all() in let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in - RLetIn(dummy_loc,nme,bdy,newtrm) + GLetIn(dummy_loc,nme,bdy,newtrm) | _ -> let _ = prstr "\nICI4 '!\n";Pp.flush_all() in raise NoMerge @@ -551,24 +550,24 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable = calls of branch 1 with all rec calls of branch 2. *) (* TODO: reecrire cette heuristique (jusqu'a merge_types) *) let rec merge_rec_hyps shift accrec - (ltyp:(Names.name * rawconstr option * rawconstr option) list) - filter_shift_stable : (Names.name * rawconstr option * rawconstr option) list = + (ltyp:(Names.name * glob_constr option * glob_constr option) list) + filter_shift_stable : (Names.name * glob_constr option * glob_constr option) list = let mergeonehyp t reldecl = match reldecl with - | (nme,x,Some (RApp(_,i,args) as ind)) + | (nme,x,Some (GApp(_,i,args) as ind)) -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable) | (nme,Some _,None) -> error "letins with recursive calls not treated yet" | (nme,None,Some _) -> assert false | (nme,None,None) | (nme,Some _,Some _) -> assert false in match ltyp with | [] -> [] - | (nme,None,Some (RApp(_,f, largs) as t)) :: lt when isVarf ind2name f -> + | (nme,None,Some (GApp(_,f, largs) as t)) :: lt when isVarf ind2name f -> let rechyps = List.map (mergeonehyp t) accrec in rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable -let rec build_suppl_reccall (accrec:(name * rawconstr) list) concl2 shift = +let rec build_suppl_reccall (accrec:(name * glob_constr) list) concl2 shift = List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec @@ -578,7 +577,7 @@ let find_app (nme:identifier) ltyp = (List.map (fun x -> match x with - | _,None,Some (RApp(_,f,_)) when isVarf nme f -> raise (Found 0) + | _,None,Some (GApp(_,f,_)) when isVarf nme f -> raise (Found 0) | _ -> ()) ltyp); false @@ -592,9 +591,9 @@ let prnt_prod_or_letin nm letbdy typ = let rec merge_types shift accrec1 - (ltyp1:(name * rawconstr option * rawconstr option) list) - (concl1:rawconstr) (ltyp2:(name * rawconstr option * rawconstr option) list) concl2 - : (name * rawconstr option * rawconstr option) list * rawconstr = + (ltyp1:(name * glob_constr option * glob_constr option) list) + (concl1:glob_constr) (ltyp2:(name * glob_constr option * glob_constr option) list) concl2 + : (name * glob_constr option * glob_constr option) list * glob_constr = let _ = prstr "MERGE_TYPES\n" in let _ = prstr "ltyp 1 : " in let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp1 in @@ -638,7 +637,7 @@ let rec merge_types shift accrec1 rechyps , concl | (nme,None, Some t1)as e ::lt1 -> (match t1 with - | RApp(_,f,carr) when isVarf ind1name f -> + | GApp(_,f,carr) when isVarf ind1name f -> merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2 | _ -> let recres, recconcl2 = @@ -705,8 +704,8 @@ let build_link_map allargs1 allargs2 lnk = Precond: vars sets of [typcstr1] and [typcstr2] must be disjoint. TODO: return nothing if equalities (after linking) are contradictory. *) -let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr) - (typcstr2:rawconstr) : rawconstr = +let merge_one_constructor (shift:merge_infos) (typcstr1:glob_constr) + (typcstr2:glob_constr) : glob_constr = (* FIXME: les noms des parametres corerspondent en principe au parametres du niveau mib, mais il faudrait s'en assurer *) (* shift.nfunresprmsx last args are functional result *) @@ -714,17 +713,17 @@ let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr) shift.mib1.mind_nparams + shift.oib1.mind_nrealargs - shift.nfunresprms1 in let nargs2 = shift.mib2.mind_nparams + shift.oib2.mind_nrealargs - shift.nfunresprms2 in - let allargs1,rest1 = raw_decompose_prod_or_letin_n nargs1 typcstr1 in - let allargs2,rest2 = raw_decompose_prod_or_letin_n nargs2 typcstr2 in + let allargs1,rest1 = glob_decompose_prod_or_letin_n nargs1 typcstr1 in + let allargs2,rest2 = glob_decompose_prod_or_letin_n nargs2 typcstr2 in (* Build map of linked args of [typcstr2], and apply it to [typcstr2]. *) let linked_map = build_link_map allargs1 allargs2 shift.lnk2 in let rest2 = change_vars linked_map rest2 in - let hyps1,concl1 = raw_decompose_prod_or_letin rest1 in - let hyps2,concl2' = raw_decompose_prod_or_letin rest2 in + let hyps1,concl1 = glob_decompose_prod_or_letin rest1 in + let hyps2,concl2' = glob_decompose_prod_or_letin rest2 in let ltyp,concl2 = merge_types shift [] (List.rev hyps1) concl1 (List.rev hyps2) concl2' in let _ = prNamedRLDecl "ltyp result:" ltyp in - let typ = raw_compose_prod_or_letin concl2 (List.rev ltyp) in + let typ = glob_compose_prod_or_letin concl2 (List.rev ltyp) in let revargs1 = list_filteri (fun i _ -> isArg_stable shift.lnk1.(i)) (List.rev allargs1) in let _ = prNamedRLDecl "ltyp allargs1" allargs1 in @@ -734,7 +733,7 @@ let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr) let _ = prNamedRLDecl "ltyp allargs2" allargs2 in let _ = prNamedRLDecl "ltyp revargs2" revargs2 in let typwithprms = - raw_compose_prod_or_letin typ (List.rev revargs2 @ List.rev revargs1) in + glob_compose_prod_or_letin typ (List.rev revargs2 @ List.rev revargs1) in typwithprms @@ -757,11 +756,11 @@ let merge_constructor_id id1 id2 shift:identifier = (** [merge_constructors lnk shift avoid] merges the two list of - constructor [(name*type)]. These are translated to rawterms + constructor [(name*type)]. These are translated to glob_constr first, each of them having distinct var names. *) let rec merge_constructors (shift:merge_infos) (avoid:Idset.t) - (typcstr1:(identifier * rawconstr) list) - (typcstr2:(identifier * rawconstr) list) : (identifier * rawconstr) list = + (typcstr1:(identifier * glob_constr) list) + (typcstr2:(identifier * glob_constr) list) : (identifier * glob_constr) list = List.flatten (List.map (fun (id1,rawtyp1) -> @@ -779,12 +778,12 @@ let rec merge_constructors (shift:merge_infos) (avoid:Idset.t) info in [shift], avoiding identifiers in [avoid]. *) let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) (oib2:one_inductive_body) = - (* building rawconstr type of constructors *) + (* building glob_constr type of constructors *) let mkrawcor nme avoid typ = (* first replace rel 1 by a varname *) let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in Detyping.detype false (Idset.elements avoid) [] substindtyp in - let lcstr1: rawconstr list = + let lcstr1: glob_constr list = Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in (* add to avoid all indentifiers of lcstr1 *) let avoid2 = Idset.union avoid (ids_of_rawlist avoid lcstr1) in @@ -793,10 +792,10 @@ let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) let avoid3 = Idset.union avoid (ids_of_rawlist avoid lcstr2) in let params1 = - try fst (raw_decompose_prod_n shift.nrecprms1 (List.hd lcstr1)) + try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1)) with _ -> [] in let params2 = - try fst (raw_decompose_prod_n shift.nrecprms2 (List.hd lcstr2)) + try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2)) with _ -> [] in let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in @@ -817,8 +816,8 @@ let rec merge_mutual_inductive_body merge_inductive_body shift Idset.empty mib1.mind_packets.(0) mib2.mind_packets.(0) -let rawterm_to_constr_expr x = (* build a constr_expr from a rawconstr *) - Flags.with_option Flags.raw_print (Constrextern.extern_rawtype Idset.empty) x +let glob_constr_to_constr_expr x = (* build a constr_expr from a glob_constr *) + Flags.with_option Flags.raw_print (Constrextern.extern_glob_type Idset.empty) x let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let params = prms2 @ prms1 in @@ -828,7 +827,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let _ = prstr "param :" in let _ = prNamedRConstr (string_of_name nme) tp in let _ = prstr " ; " in - let typ = rawterm_to_constr_expr tp in + let typ = glob_constr_to_constr_expr tp in LocalRawAssum ([(dummy_loc,nme)], Topconstr.default_binder_kind, typ) :: acc) [] params in let concl = Constrextern.extern_constr false (Global.env()) concl in @@ -845,38 +844,38 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = -(** [rawterm_list_to_inductive_expr ident rawlist] returns the +(** [glob_constr_list_to_inductive_expr ident rawlist] returns the induct_expr corresponding to the the list of constructor types [rawlist], named ident. FIXME: params et cstr_expr (arity) *) -let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift - (rawlist:(identifier * rawconstr) list) = +let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift + (rawlist:(identifier * glob_constr) list) = let lident = dummy_loc, shift.ident in let bindlist , cstr_expr = (* params , arities *) merge_rec_params_and_arity prms1 prms2 shift mkSet in let lcstor_expr : (bool * (lident * constr_expr)) list = List.map (* zeta_normalize t ? *) - (fun (id,t) -> false, ((dummy_loc,id),rawterm_to_constr_expr t)) + (fun (id,t) -> false, ((dummy_loc,id),glob_constr_to_constr_expr t)) rawlist in lident , bindlist , Some cstr_expr , lcstor_expr -let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) = +let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) = match rdecl with | (nme,None,t) -> let traw = Detyping.detype false [] [] t in - RProd (dummy_loc,nme,Explicit,traw,t2) + GProd (dummy_loc,nme,Explicit,traw,t2) | (_,Some _,_) -> assert false -let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) = +let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) = match rdecl with | (nme,None,t) -> let traw = Detyping.detype false [] [] t in - RProd (dummy_loc,nme,Explicit,traw,t2) + GProd (dummy_loc,nme,Explicit,traw,t2) | (_,Some _,_) -> assert false @@ -902,7 +901,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) recprms1=prms1; recprms1=prms1; } in *) - let indexpr = rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in + let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in @@ -1024,9 +1023,3 @@ let relprinctype_to_funprinctype relprinctype nfuns = url = "citeseer.ist.psu.edu/bundy93rippling.html" } *) -(* -*** Local Variables: *** -*** compile-command: "make -C ../.. plugins/funind/merge.cmo" *** -*** indent-tabs-mode: nil *** -*** End: *** -*) diff --git a/plugins/funind/rawtermops.mli b/plugins/funind/rawtermops.mli deleted file mode 100644 index 455e7c89..00000000 --- a/plugins/funind/rawtermops.mli +++ /dev/null @@ -1,126 +0,0 @@ -open Rawterm - -(* Ocaml 3.06 Map.S does not handle is_empty *) -val idmap_is_empty : 'a Names.Idmap.t -> bool - - -(* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *) -val get_pattern_id : cases_pattern -> Names.identifier list - -(* [pattern_to_term pat] returns a rawconstr corresponding to [pat]. - [pat] must not contain occurences of anonymous pattern -*) -val pattern_to_term : cases_pattern -> rawconstr - -(* - Some basic functions to rebuild rawconstr - In each of them the location is Util.dummy_loc -*) -val mkRRef : Libnames.global_reference -> rawconstr -val mkRVar : Names.identifier -> rawconstr -val mkRApp : rawconstr*(rawconstr list) -> rawconstr -val mkRLambda : Names.name*rawconstr*rawconstr -> rawconstr -val mkRProd : Names.name*rawconstr*rawconstr -> rawconstr -val mkRLetIn : Names.name*rawconstr*rawconstr -> rawconstr -val mkRCases : rawconstr option * tomatch_tuples * 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 -*) -val raw_decompose_prod : rawconstr -> (Names.name*rawconstr) list * rawconstr -val raw_decompose_prod_or_letin : - rawconstr -> (Names.name*rawconstr option*rawconstr option) list * rawconstr -val raw_decompose_prod_n : int -> rawconstr -> (Names.name*rawconstr) list * rawconstr -val raw_decompose_prod_or_letin_n : int -> rawconstr -> - (Names.name*rawconstr option*rawconstr option) list * rawconstr -val raw_compose_prod : rawconstr -> (Names.name*rawconstr) list -> rawconstr -val raw_compose_prod_or_letin: rawconstr -> - (Names.name*rawconstr option*rawconstr option) list -> rawconstr -val raw_decompose_app : rawconstr -> rawconstr*(rawconstr list) - - -(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *) -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] *) -val raw_make_or : rawconstr -> rawconstr -> rawconstr - -(* [raw_make_or_list [P1;...;Pn]] build the rawconstr corresponding - to [P1 \/ ( .... \/ Pn)] -*) -val raw_make_or_list : rawconstr list -> rawconstr - - -(* alpha_conversion functions *) - - - -(* Replace the var mapped in the rawconstr/context *) -val change_vars : Names.identifier Names.Idmap.t -> rawconstr -> rawconstr - - - -(* [alpha_pat avoid pat] rename all the variables present in [pat] s.t. - the result does not share variables with [avoid]. This function create - a fresh variable for each occurence of the anonymous pattern. - - Also returns a mapping from old variables to new ones and the concatenation of - [avoid] with the variables appearing in the result. -*) - val alpha_pat : - Names.Idmap.key list -> - Rawterm.cases_pattern -> - Rawterm.cases_pattern * Names.Idmap.key list * - Names.identifier Names.Idmap.t - -(* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt - conventions and does not share bound variables with avoid -*) -val alpha_rt : Names.identifier list -> rawconstr -> rawconstr - -(* same as alpha_rt but for case branches *) -val alpha_br : Names.identifier list -> - Util.loc * Names.identifier list * Rawterm.cases_pattern list * - Rawterm.rawconstr -> - Util.loc * Names.identifier list * Rawterm.cases_pattern list * - Rawterm.rawconstr - - -(* Reduction function *) -val replace_var_by_term : - Names.identifier -> - Rawterm.rawconstr -> Rawterm.rawconstr -> Rawterm.rawconstr - - - -(* - [is_free_in id rt] checks if [id] is a free variable in [rt] -*) -val is_free_in : Names.identifier -> rawconstr -> bool - - -val are_unifiable : cases_pattern -> cases_pattern -> bool -val eq_cases_pattern : cases_pattern -> cases_pattern -> bool - - - -(* - ids_of_pat : cases_pattern -> Idset.t - returns the set of variables appearing in a pattern -*) -val ids_of_pat : cases_pattern -> Names.Idset.t - -(* TODO: finish this function (Fix not treated) *) -val ids_of_rawterm: rawconstr -> Names.Idset.t - -(* - removing let_in construction in a rawterm -*) -val zeta_normalize : Rawterm.rawconstr -> Rawterm.rawconstr - - -val expand_as : rawconstr -> rawconstr diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 83868da9..55ebd31b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,10 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: recdef.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Term -open Termops open Namegen open Environ open Declarations @@ -36,7 +33,7 @@ open Proof_type open Vernacinterp open Pfedit open Topconstr -open Rawterm +open Glob_term open Pretyping open Pretyping.Default open Safe_typing @@ -69,45 +66,39 @@ let pf_get_new_id id g = let h_intros l = tclMAP h_intro l -let debug_queue = Queue.create () +let debug_queue = Stack.create () -let rec print_debug_queue e = - let lmsg,goal = Queue.pop debug_queue in - if Queue.is_empty debug_queue - then - msgnl (lmsg ++ (str " raised exception " ++ Cerrors.explain_exn e) ++ str " on goal " ++ goal) - else +let rec print_debug_queue b e = + if not (Stack.is_empty debug_queue) + then begin - print_debug_queue e; - msgnl (str " from " ++ lmsg ++ str " on goal " ++ goal); + let lmsg,goal = Stack.pop debug_queue in + if b then + msgnl (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal) + else + begin + msgnl (str " from " ++ lmsg ++ str " on goal " ++ goal); + end; + print_debug_queue false e; end + let do_observe_tac s tac g = - let goal = Printer.pr_goal (sig_it g) in - let lmsg = (str "recdef ") ++ (str s) in - Queue.add (lmsg,goal) debug_queue; + let goal = Printer.pr_goal g in + let lmsg = (str "recdef : ") ++ (str s) in + Stack.push (lmsg,goal) debug_queue; try let v = tac g in - ignore(Queue.pop debug_queue); + ignore(Stack.pop debug_queue); v with e -> - if not (Queue.is_empty debug_queue) + if not (Stack.is_empty debug_queue) then - print_debug_queue e; + print_debug_queue true e; raise e -(*let do_observe_tac s tac g = - let goal = begin (Printer.pr_goal (sig_it g)) end in - try let v = tac g in msgnl (goal ++ fnl () ++ (str "recdef ") ++ - (str s)++(str " ")++(str "finished")); v - with e -> - msgnl (str "observation "++str s++str " raised exception " ++ - Cerrors.explain_exn e ++ str " on goal " ++ goal ); - raise e;; -*) - let observe_tac s tac g = if Tacinterp.get_debug () <> Tactic_debug.DebugOff then do_observe_tac s tac g @@ -145,9 +136,9 @@ let message s = if Flags.is_verbose () then msgnl(str s);; let def_of_const t = match (kind_of_term t) with Const sp -> - (try (match (Global.lookup_constant sp) with - {const_body=Some c} -> Declarations.force c - |_ -> assert false) + (try (match body_of_constant (Global.lookup_constant sp) with + | Some c -> Declarations.force c + | _ -> assert false) with _ -> anomaly ("Cannot find definition of constant "^ (string_of_id (id_of_label (con_label sp)))) @@ -180,11 +171,23 @@ let rank_for_arg_list h = | x::tl -> if predicate h x then Some i else rank_aux (i+1) tl in rank_aux 0;; -let rec (find_call_occs : int -> constr -> constr -> +let rec check_not_nested f t = + match kind_of_term t with + | App(g, _) when eq_constr f g -> + errorlabstrm "recdef" (str "Nested recursive function are not allowed with Function") + | Var(_) when eq_constr t f -> errorlabstrm "recdef" (str "Nested recursive function are not allowed with Function") + | _ -> iter_constr (check_not_nested f) t + + + + +let rec (find_call_occs : int -> int -> constr -> constr -> (constr list -> constr) * constr list list) = - fun nb_lam f expr -> + fun nb_arg nb_lam f expr -> match (kind_of_term expr) with - App (g, args) when g = f -> + App (g, args) when eq_constr g f -> + if Array.length args <> nb_arg then errorlabstrm "recdef" (str "Partial application of function " ++ Printer.pr_lconstr expr ++ str " in its body is not allowed while using Function"); + Array.iter (check_not_nested f) args; (fun l -> List.hd l), [Array.to_list args] | App (g, args) -> let (largs: constr list) = Array.to_list args in @@ -193,7 +196,7 @@ let rec (find_call_occs : int -> constr -> constr -> | a::upper_tl -> (match find_aux upper_tl with (cf, ((arg1::args) as args_for_upper_tl)) -> - (match find_call_occs nb_lam f a with + (match find_call_occs nb_arg nb_lam f a with cf2, (_ :: _ as other_args) -> let rec avoid_duplicates args = match args with @@ -217,7 +220,7 @@ let rec (find_call_occs : int -> constr -> constr -> other_args'@args_for_upper_tl | _, [] -> (fun x -> a::cf x), args_for_upper_tl) | _, [] -> - (match find_call_occs nb_lam f a with + (match find_call_occs nb_arg nb_lam f a with cf, (arg1::args) -> (fun l -> cf l::upper_tl), (arg1::args) | _, [] -> (fun x -> a::upper_tl), [])) in begin @@ -227,15 +230,16 @@ let rec (find_call_occs : int -> constr -> constr -> (fun l -> mkApp (g, Array.of_list (cf l))), args end | Rel(v) -> if v > nb_lam then error "find_call_occs : Rel" else ((fun l -> expr),[]) + | Var(_) when eq_constr expr f -> errorlabstrm "recdef" (str "Partial application of function " ++ Printer.pr_lconstr expr ++ str " in its body is not allowed while using Function") | Var(id) -> (fun l -> expr), [] | Meta(_) -> error "find_call_occs : Meta" | Evar(_) -> error "find_call_occs : Evar" | Sort(_) -> (fun l -> expr), [] - | Cast(b,_,_) -> find_call_occs nb_lam f b + | Cast(b,_,_) -> find_call_occs nb_arg nb_lam f b | Prod(_,_,_) -> error "find_call_occs : Prod" | Lambda(na,t,b) -> begin - match find_call_occs (succ nb_lam) f b with + match find_call_occs nb_arg (succ nb_lam) f b with | _, [] -> (* Lambda are authorized as long as they do not contain recursives calls *) (fun l -> expr),[] @@ -243,7 +247,7 @@ let rec (find_call_occs : int -> constr -> constr -> end | LetIn(na,v,t,b) -> begin - match find_call_occs nb_lam f v, find_call_occs (succ nb_lam) f b with + match find_call_occs nb_arg nb_lam f v, find_call_occs nb_arg (succ nb_lam) f b with | (_,[]),(_,[]) -> ((fun l -> expr), []) | (_,[]),(cf,(_::_ as l)) -> @@ -256,7 +260,7 @@ let rec (find_call_occs : int -> constr -> constr -> | Ind(_) -> (fun l -> expr), [] | Construct (_, _) -> (fun l -> expr), [] | Case(i,t,a,r) -> - (match find_call_occs nb_lam f a with + (match find_call_occs nb_arg nb_lam f a with cf, (arg1::args) -> (fun l -> mkCase(i, t, (cf l), r)),(arg1::args) | _ -> (fun l -> expr),[]) | Fix(_) -> error "find_call_occs : Fix" @@ -369,15 +373,15 @@ let rec mk_intros_and_continue thin_intros (extra_eqn:bool) h_intros thin_intros; tclMAP - (fun eq -> tclTRY (Equality.general_rewrite_in true all_occurrences (* deps proofs also: *) true teq eq false)) + (fun eq -> tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true (* deps proofs also: *) true teq eq false)) (List.rev eqs); (fun g1 -> let ty_teq = pf_type_of g1 (mkVar teq) in let teq_lhs,teq_rhs = - let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal (sig_it g1) ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in + let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal g1 ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in args.(1),args.(2) in - cont_function (mkVar teq::eqs) (replace_term teq_lhs teq_rhs expr) g1 + cont_function (mkVar teq::eqs) (Termops.replace_term teq_lhs teq_rhs expr) g1 ) ] @@ -430,7 +434,7 @@ let tclUSER tac is_mes l g = clear_tac; if is_mes then tclTHEN - (unfold_in_concl [(all_occurrences, evaluable_of_global_reference + (unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))]) tac else tac @@ -529,8 +533,8 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs = Nameops.out_name k_na,Nameops.out_name def_na in tclTHENS - (general_rewrite_bindings false all_occurrences - (* dep proofs also: *) true + (general_rewrite_bindings false Termops.all_occurrences + (* dep proofs also: *) true true (mkVar eq, ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k; dummy_loc, NamedHyp def_id, mkVar def]) false) @@ -572,7 +576,7 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs observe_tac "refl equal" (apply (delayed_force refl_equal))] g | spec1::specs -> fun g -> - let ids = ids_of_named_context (pf_hyps g) in + let ids = Termops.ids_of_named_context (pf_hyps g) in let p = next_ident_away_in_goal p_id ids in let ids = p::ids in let pmax = next_ident_away_in_goal pmax_id ids in @@ -618,7 +622,7 @@ let rec introduce_all_values concl_tac is_mes acc_inv func context_fn (List.rev values) (List.rev specs) (delayed_force coq_O) [] [])] | arg::args -> (fun g -> - let ids = ids_of_named_context (pf_hyps g) in + let ids = Termops.ids_of_named_context (pf_hyps g) in let rec_res = next_ident_away_in_goal rec_res_id ids in let ids = rec_res::ids in let hspec = next_ident_away_in_goal hspec_id ids in @@ -657,13 +661,13 @@ let rec introduce_all_values concl_tac is_mes acc_inv func context_fn ) -let rec_leaf_terminate f_constr concl_tac is_mes acc_inv hrec (func:global_reference) eqs expr = - match find_call_occs 0 f_constr expr with +let rec_leaf_terminate nb_arg f_constr concl_tac is_mes acc_inv hrec (func:global_reference) eqs expr = + match find_call_occs nb_arg 0 f_constr expr with | context_fn, args -> observe_tac "introduce_all_values" (introduce_all_values concl_tac is_mes acc_inv func context_fn eqs hrec args [] []) -let proveterminate rec_arg_id is_mes acc_inv (hrec:identifier) +let proveterminate nb_arg rec_arg_id is_mes acc_inv (hrec:identifier) (f_constr:constr) (func:global_reference) base_leaf rec_leaf = let rec proveterminate (eqs:constr list) (expr:constr) = try @@ -671,7 +675,7 @@ let proveterminate rec_arg_id is_mes acc_inv (hrec:identifier) let v = match (kind_of_term expr) with Case (ci, t, a, l) -> - (match find_call_occs 0 f_constr a with + (match find_call_occs nb_arg 0 f_constr a with _,[] -> (fun g -> let destruct_tac, rev_to_thin_intro = @@ -683,16 +687,16 @@ let proveterminate rec_arg_id is_mes acc_inv (hrec:identifier) true proveterminate eqs - ci.ci_cstr_nargs.(i)) + ci.ci_cstr_ndecls.(i)) 0 (Array.to_list l)) g) | _, _::_ -> - (match find_call_occs 0 f_constr expr with + (match find_call_occs nb_arg 0 f_constr expr with _,[] -> observe_tac "base_leaf" (base_leaf func eqs expr) | _, _:: _ -> observe_tac "rec_leaf" (rec_leaf is_mes acc_inv hrec func eqs expr))) | _ -> - (match find_call_occs 0 f_constr expr with + (match find_call_occs nb_arg 0 f_constr expr with _,[] -> (try observe_tac "base_leaf" (base_leaf func eqs expr) with e -> (msgerrnl (str "failure in base case");raise e )) @@ -831,7 +835,7 @@ let rec instantiate_lambda t l = let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_arg_num : tactic = begin fun g -> - let ids = ids_of_named_context (pf_hyps g) in + let ids = Termops.ids_of_named_context (pf_hyps g) in let func_body = (def_of_const (constr_of_global func)) in let (f_name, _, body1) = destLambda func_body in let f_id = @@ -864,6 +868,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a rec_arg_id (fun rec_arg_id hrec acc_inv g -> (proveterminate + nb_args [rec_arg_id] is_mes acc_inv @@ -871,7 +876,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a (mkVar f_id) func base_leaf_terminate - (rec_leaf_terminate (mkVar f_id) concl_tac) + (rec_leaf_terminate nb_args (mkVar f_id) concl_tac) [] expr ) @@ -882,9 +887,9 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a end let get_current_subgoals_types () = - let pts = get_pftreestate () in - let _,subs = extract_open_pftreestate pts in - List.map snd ((* List.sort (fun (x,_) (y,_) -> x -y ) *)subs ) + let p = Proof_global.give_me_the_proof () in + let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in + List.map (Goal.V82.abstract_type sigma) sgs let build_and_l l = let and_constr = Coqlib.build_coq_and () in @@ -918,7 +923,7 @@ let clear_goals = | Prod(Name id as na,t',b) -> let b' = clear_goal b in if noccurn 1 b' && (is_rec_res id) - then pop b' + then Termops.pop b' else if b' == b then t else mkProd(na,t',b') | _ -> map_constr clear_goal t @@ -934,6 +939,13 @@ let build_new_goal_type () = let res = build_and_l sub_gls_types in res +let is_opaque_constant c = + let cb = Global.lookup_constant c in + match cb.Declarations.const_body with + | Declarations.OpaqueDef _ -> true + | Declarations.Undef _ -> true + | Declarations.Def _ -> false + let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) let current_proof_name = get_current_proof_name () in @@ -943,20 +955,16 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ try (add_suffix current_proof_name "_subproof") with _ -> anomaly "open_new_goal with an unamed theorem" in - let sign = Global.named_context () in - let sign = clear_proofs sign in + let sign = initialize_named_context_for_proof () in let na = next_global_ident_away name [] in - if occur_existential gls_type then + if Termops.occur_existential gls_type then Util.error "\"abstract\" cannot handle existentials"; let hook _ _ = let opacity = let na_ref = Libnames.Ident (dummy_loc,na) in let na_global = Nametab.global na_ref in match na_global with - ConstRef c -> - let cb = Global.lookup_constant c in - if cb.Declarations.const_opaque then true - else begin match cb.const_body with None -> true | _ -> false end + ConstRef c -> is_opaque_constant c | _ -> anomaly "equation_lemma: not a constant" in let lemma = mkConst (Lib.make_con na) in @@ -1000,7 +1008,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ Eauto.eauto_with_bases false (true,5) - [delayed_force refl_equal] + [Evd.empty,delayed_force refl_equal] [Auto.Hint_db.empty empty_transparent_state false] ] ) @@ -1101,38 +1109,31 @@ let (value_f:constr list -> global_reference -> constr) = al ) in - let fun_body = - RCases + let context = List.map + (fun (x, c) -> Name x, None, c) (List.combine rev_x_id_l (List.rev al)) + in + let env = Environ.push_rel_context context (Global.env ()) in + let glob_body = + GCases (d0,RegularStyle,None, - [RApp(d0, RRef(d0,fterm), List.rev_map (fun x_id -> RVar(d0, x_id)) rev_x_id_l), + [GApp(d0, GRef(d0,fterm), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l), (Anonymous,None)], [d0, [v_id], [PatCstr(d0,(ind_of_ref (delayed_force coq_sig_ref),1), [PatVar(d0, Name v_id); PatVar(d0, Anonymous)], Anonymous)], - RVar(d0,v_id)]) - in - let value = - List.fold_left2 - (fun acc x_id a -> - RLambda - (d0, Name x_id, Explicit, RDynamic(d0, constr_in a), - acc - ) - ) - fun_body - rev_x_id_l - (List.rev al) + GVar(d0,v_id)]) in - understand Evd.empty (Global.env()) value;; + let body = understand Evd.empty env glob_body in + it_mkLambda_or_LetIn body context let (declare_fun : identifier -> logical_kind -> constr -> global_reference) = fun f_id kind value -> let ce = {const_entry_body = value; + const_entry_secctx = None; const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = true} in + const_entry_opaque = false } in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; let (declare_f : identifier -> logical_kind -> constr list -> global_reference -> global_reference) = @@ -1152,7 +1153,7 @@ let start_equation (f:global_reference) (term_f:global_reference) let x = n_x_id ids nargs in tclTHENLIST [ h_intros x; - unfold_in_concl [(all_occurrences, evaluable_of_global_reference f)]; + unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference f)]; observe_tac "simplest_case" (simplest_case (mkApp (terminate_constr, Array.of_list (List.map mkVar x)))); @@ -1194,7 +1195,7 @@ let rec introduce_all_values_eq cont_tac functional termine simpl_iter (onHyp heq2); unfold_in_hyp [((true,[1]), evaluable_of_global_reference (global_of_constr functional))] - (heq2, InHyp); + (heq2, Termops.InHyp); tclTHENS (fun gls -> let t_eq = compute_renamed_type gls (mkVar heq2) in @@ -1202,8 +1203,8 @@ let rec introduce_all_values_eq cont_tac functional termine let _,_,t = destProd t_eq in let def_na,_,_ = destProd t in Nameops.out_name def_na in - observe_tac "rewrite heq" (general_rewrite_bindings false all_occurrences - (* dep proofs also: *) true (mkVar heq2, + observe_tac "rewrite heq" (general_rewrite_bindings false Termops.all_occurrences + true (* dep proofs also: *) true (mkVar heq2, ExplicitBindings[dummy_loc,NamedHyp def_id, f]) false) gls) [tclTHENLIST @@ -1258,7 +1259,7 @@ let rec introduce_all_values_eq cont_tac functional termine f_S(mkVar pmax'); dummy_loc, NamedHyp def_id, f]) in - observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false all_occurrences (* dep proofs also: *) true + observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false Termops.all_occurrences true (* dep proofs also: *) true c_b false)) g ) @@ -1293,12 +1294,12 @@ let rec_leaf_eq termine f ids functional eqs expr fn args = functional termine f p heq1 p [] [] eqs ids args); observe_tac "failing here" (apply (delayed_force refl_equal))] -let rec prove_eq (termine:constr) (f:constr)(functional:global_reference) +let rec prove_eq nb_arg (termine:constr) (f:constr)(functional:global_reference) (eqs:constr list) (expr:constr) = (* tclTRY *) observe_tac "prove_eq" (match kind_of_term expr with Case(ci,t,a,l) -> - (match find_call_occs 0 f a with + (match find_call_occs nb_arg 0 f a with _,[] -> (fun g -> let destruct_tac,rev_to_thin_intro = mkDestructEq [] a g in @@ -1307,38 +1308,35 @@ let rec prove_eq (termine:constr) (f:constr)(functional:global_reference) (list_map_i (fun i -> mk_intros_and_continue (List.rev rev_to_thin_intro) true - (prove_eq termine f functional) - eqs ci.ci_cstr_nargs.(i)) + (prove_eq nb_arg termine f functional) + eqs ci.ci_cstr_ndecls.(i)) 0 (Array.to_list l)) g) | _,_::_ -> - (match find_call_occs 0 f expr with + (match find_call_occs nb_arg 0 f expr with _,[] -> observe_tac "base_leaf_eq(1)" (base_leaf_eq functional eqs f) | fn,args -> fun g -> - let ids = ids_of_named_context (pf_hyps g) in + let ids = Termops.ids_of_named_context (pf_hyps g) in observe_tac "rec_leaf_eq" (rec_leaf_eq termine f ids (constr_of_global functional) eqs expr fn args) g)) | _ -> - (match find_call_occs 0 f expr with + (match find_call_occs nb_arg 0 f expr with _,[] -> observe_tac "base_leaf_eq(2)" ( base_leaf_eq functional eqs f) | fn,args -> fun g -> - let ids = ids_of_named_context (pf_hyps g) in + let ids = Termops.ids_of_named_context (pf_hyps g) in observe_tac "rec_leaf_eq" (rec_leaf_eq termine f ids (constr_of_global functional) eqs expr fn args) g));; -let (com_eqn : identifier -> +let (com_eqn : int -> identifier -> global_reference -> global_reference -> global_reference -> constr -> unit) = - fun eq_name functional_ref f_ref terminate_ref equation_lemma_type -> + fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type -> let opacity = match terminate_ref with - | ConstRef c -> - let cb = Global.lookup_constant c in - if cb.Declarations.const_opaque then true - else begin match cb.const_body with None -> true | _ -> false end + | ConstRef c -> is_opaque_constant c | _ -> anomaly "terminate_lemma: not a constant" in let (evmap, env) = Lemmas.get_current_context() in @@ -1349,7 +1347,7 @@ let (com_eqn : identifier -> by (start_equation f_ref terminate_ref (fun x -> - prove_eq + prove_eq nb_arg (constr_of_global terminate_ref) f_constr functional_ref @@ -1382,12 +1380,12 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num generate_induction_principle using_lemmas : unit = let function_type = interp_constr Evd.empty (Global.env()) type_of_f in let env = push_named (function_name,None,function_type) (Global.env()) in -(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) + (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) let equation_lemma_type = nf_betaiotazeta (interp_gen (OfType None) Evd.empty env ~impls:rec_impls eq) in -(* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *) + (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *) let res_vars,eq' = decompose_prod equation_lemma_type in let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in let eq' = nf_zeta env_eq' eq' in @@ -1406,7 +1404,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let equation_id = add_suffix function_name "_equation" in let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in - let functional_ref = declare_fun functional_id (IsDefinition Definition) res in + let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) res in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in let relation = interp_constr @@ -1420,14 +1418,15 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in + let _ = Table.extraction_inline true [Ident (dummy_loc,term_id)] in (* message "start second proof"; *) let stop = ref false in begin - try com_eqn equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type) + try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type) with e -> begin if Tacinterp.get_debug () <> Tactic_debug.DebugOff - then pperrnl (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e) + then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e) else anomaly "Cannot create equation Lemma" ; (* ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *) diff --git a/plugins/funind/recdef_plugin.mllib b/plugins/funind/recdef_plugin.mllib index 31818c39..ec1f5436 100644 --- a/plugins/funind/recdef_plugin.mllib +++ b/plugins/funind/recdef_plugin.mllib @@ -1,7 +1,7 @@ Indfun_common -Rawtermops +Glob_termops Recdef -Rawterm_to_relation +Glob_term_to_relation Functional_principles_proofs Functional_principles_types Invfun |