From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- plugins/funind/indfun_common.ml | 168 ++++++++++++++++++++++++++-------------- 1 file changed, 110 insertions(+), 58 deletions(-) (limited to 'plugins/funind/indfun_common.ml') diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index f56e9241..a0b9217c 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -1,8 +1,10 @@ open Names open Pp +open Constr open Libnames open Globnames open Refiner + let mk_prefix pre id = Id.of_string (pre^(Id.to_string id)) let mk_rel_id = mk_prefix "R_" let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct" @@ -12,7 +14,7 @@ let mk_equation_id id = Nameops.add_suffix id "_equation" let msgnl m = () -let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) avoid +let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) (Id.Set.of_list avoid) let fresh_name avoid s = Name (fresh_id avoid s) @@ -21,19 +23,16 @@ let get_name avoid ?(default="H") = function | Name n -> Name n let array_get_start a = - try - Array.init - (Array.length a - 1) - (fun i -> a.(i)) - with Invalid_argument "index out of bounds" -> - invalid_arg "array_get_start" + Array.init + (Array.length a - 1) + (fun i -> a.(i)) let id_of_name = function Name id -> id | _ -> raise Not_found let locate ref = - let (loc,qid) = qualid_of_reference ref in + let {CAst.v=qid} = qualid_of_reference ref in Nametab.locate qid let locate_ind ref = @@ -49,7 +48,7 @@ let locate_constant ref = let locate_with_msg msg f x = try f x - with Not_found -> raise (CErrors.UserError("", msg)) + with Not_found -> raise (CErrors.UserError(None, msg)) let filter_map filter f = @@ -69,11 +68,11 @@ let chop_rlambda_n = if n == 0 then List.rev acc,rt else - match rt with - | 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 + match DAst.get rt with + | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b + | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b | _ -> - raise (CErrors.UserError("chop_rlambda_n", + raise (CErrors.UserError(Some "chop_rlambda_n", str "chop_rlambda_n: Not enough Lambdas")) in chop_lambda_n [] @@ -83,9 +82,9 @@ let chop_rprod_n = if n == 0 then List.rev acc,rt else - match rt with - | Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b - | _ -> raise (CErrors.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products")) + match DAst.get rt with + | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b + | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products")) in chop_prod_n [] @@ -101,20 +100,15 @@ let list_union_eq eq_fun l1 l2 = let list_add_set_eq eq_fun x l = if List.exists (eq_fun x) l then l else x::l - - - let const_of_id id = - let _,princ_ref = - qualid_of_reference (Libnames.Ident (Loc.ghost,id)) - in + let princ_ref = qualid_of_ident id in try Constrintern.locate_reference princ_ref with Not_found -> - CErrors.errorlabstrm "IndFun.const_of_id" - (str "cannot find " ++ Nameops.pr_id id) + CErrors.user_err ~hdr:"IndFun.const_of_id" + (str "cannot find " ++ Id.print id) let def_of_const t = - match (Term.kind_of_term t) with + match Constr.kind t with Term.Const sp -> (try (match Environ.constant_opt_value_in (Global.env()) sp with | Some c -> c @@ -123,15 +117,16 @@ let def_of_const t = |_ -> assert false let coq_constant s = - Coqlib.gen_constant_in_modules "RecursiveDefinition" + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s;; let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in Nametab.locate (make_qualid dp (Id.of_string s)) -let eq = lazy(coq_constant "eq") -let refl_equal = lazy(coq_constant "eq_refl") +let eq = lazy(EConstr.of_constr (coq_constant "eq")) +let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl")) (*****************************************************************) (* Copy of the standart save mechanism but without the much too *) @@ -162,7 +157,7 @@ let save with_clean id const (locality,_,kind) hook = let kn = declare_constant id ~local (DefinitionEntry const, k) in (locality, ConstRef kn) in - if with_clean then Pfedit.delete_current_proof (); + if with_clean then Proof_global.discard_current (); CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); definition_message id @@ -174,7 +169,7 @@ let cook_proof _ = let get_proof_clean do_reduce = let result = cook_proof do_reduce in - Pfedit.delete_current_proof (); + Proof_global.discard_current (); result let with_full_print f a = @@ -183,12 +178,13 @@ let with_full_print f a = and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in let old_rawprint = !Flags.raw_print in let old_printuniverses = !Constrextern.print_universes in + let old_printallowmatchdefaultclause = !Detyping.print_allow_match_default_clause in Constrextern.print_universes := true; + Detyping.print_allow_match_default_clause := false; Flags.raw_print := true; Impargs.make_implicit_args false; Impargs.make_strict_implicit_args false; Impargs.make_contextual_implicit_args false; - Impargs.make_contextual_implicit_args false; Dumpglob.pause (); try let res = f a in @@ -197,6 +193,7 @@ let with_full_print f a = Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Constrextern.print_universes := old_printuniverses; + Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; Dumpglob.continue (); res with @@ -206,6 +203,7 @@ let with_full_print f a = Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Constrextern.print_universes := old_printuniverses; + Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; Dumpglob.continue (); raise reraise @@ -218,14 +216,14 @@ let with_full_print f a = type function_info = { - function_constant : constant; + function_constant : Constant.t; graph_ind : inductive; - equation_lemma : constant option; - correctness_lemma : constant option; - completeness_lemma : constant option; - rect_lemma : constant option; - rec_lemma : constant option; - prop_lemma : constant option; + equation_lemma : Constant.t option; + correctness_lemma : Constant.t option; + completeness_lemma : Constant.t option; + rect_lemma : Constant.t option; + rec_lemma : Constant.t option; + prop_lemma : Constant.t option; is_general : bool; (* Has this function been defined using general recursive definition *) } @@ -332,18 +330,18 @@ let discharge_Function (_,finfos) = is_general = finfos.is_general } -open Term - let pr_ocst c = - Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) c (mt ()) + let sigma, env = Pfedit.get_current_context () in + Option.fold_right (fun v acc -> Printer.pr_lconstr_env env sigma (mkConst v)) c (mt ()) let pr_info f_info = + let sigma, env = Pfedit.get_current_context () in str "function_constant := " ++ - Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++ + Printer.pr_lconstr_env env sigma (mkConst f_info.function_constant)++ fnl () ++ str "function_constant_type := " ++ (try - Printer.pr_lconstr - (Global.type_of_global_unsafe (ConstRef f_info.function_constant)) + Printer.pr_lconstr_env env sigma + (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant))) with e when CErrors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ @@ -351,7 +349,7 @@ let pr_info f_info = str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++ str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++ str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++ - str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () + str "graph_ind := " ++ Printer.pr_lconstr_env env sigma (mkInd f_info.graph_ind) ++ fnl () let pr_table tb = let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in @@ -371,7 +369,7 @@ let in_Function : function_info -> Libobject.obj = let find_or_none id = try Some - (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant") + (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.") ) with Not_found -> None @@ -390,7 +388,7 @@ let update_Function finfo = let add_Function is_general f = - let f_id = Label.to_id (con_label f) in + let f_id = Label.to_id (Constant.label f) in let equation_lemma = find_or_none (mk_equation_id f_id) and correctness_lemma = find_or_none (mk_correct_id f_id) and completeness_lemma = find_or_none (mk_complete_id f_id) @@ -399,7 +397,7 @@ let add_Function is_general f = and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind") and graph_ind = match Nametab.locate (qualid_of_ident (mk_rel_id f_id)) - with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive") + with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.") in let finfos = { function_constant = f; @@ -425,7 +423,6 @@ open Goptions let functional_induction_rewrite_dependent_proofs_sig = { - optsync = false; optdepr = false; optname = "Functional Induction Rewrite Dependent"; optkey = ["Functional";"Induction";"Rewrite";"Dependent"]; @@ -438,7 +435,6 @@ let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = t let function_debug_sig = { - optsync = false; optdepr = false; optname = "Function debug"; optkey = ["Function_debug"]; @@ -457,7 +453,6 @@ let strict_tcc = ref false let is_strict_tcc () = !strict_tcc let strict_tcc_sig = { - optsync = false; optdepr = false; optname = "Raw Function Tcc"; optkey = ["Function_raw_tcc"]; @@ -475,13 +470,17 @@ exception ToShow of exn let jmeq () = try Coqlib.check_required_library Coqlib.jmeq_module_name; - Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq" + EConstr.of_constr @@ + Universes.constr_of_global @@ + Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq" with e when CErrors.noncritical e -> raise (ToShow e) let jmeq_refl () = try Coqlib.check_required_library Coqlib.jmeq_module_name; - Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq_refl" + EConstr.of_constr @@ + Universes.constr_of_global @@ + Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl" with e when CErrors.noncritical e -> raise (ToShow e) let h_intros l = @@ -489,10 +488,13 @@ let h_intros l = let h_id = Id.of_string "h" let hrec_id = Id.of_string "hrec" -let well_founded = function () -> (coq_constant "well_founded") -let acc_rel = function () -> (coq_constant "Acc") -let acc_inv_id = function () -> (coq_constant "Acc_inv") -let well_founded_ltof = function () -> (Coqlib.coq_constant "" ["Arith";"Wf_nat"] "well_founded_ltof") +let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded") +let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc") +let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv") + +let well_founded_ltof () = EConstr.of_constr @@ Universes.constr_of_global @@ + Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof" + let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (Global.env ()) *) @@ -501,8 +503,58 @@ let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (G | VarRef id -> EvalVarRef id | _ -> assert false;; -let list_rewrite (rev:bool) (eqs: (constr*bool) list) = +let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) = tclREPEAT (List.fold_right (fun (eq,b) i -> tclORELSE (Proofview.V82.of_tactic ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) i) (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));; + +let decompose_lam_n sigma n = + if n < 0 then CErrors.user_err Pp.(str "decompose_lam_n: integer parameter must be positive"); + let rec lamdec_rec l n c = + if Int.equal n 0 then l,c + else match EConstr.kind sigma c with + | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c + | Cast (c,_,_) -> lamdec_rec l n c + | _ -> CErrors.user_err Pp.(str "decompose_lam_n: not enough abstractions") + in + lamdec_rec [] n + +let lamn n env b = + let open EConstr in + let rec lamrec = function + | (0, env, b) -> b + | (n, ((v,t)::l), b) -> lamrec (n-1, l, mkLambda (v,t,b)) + | _ -> assert false + in + lamrec (n,env,b) + +(* compose_lam [xn:Tn;..;x1:T1] b = [x1:T1]..[xn:Tn]b *) +let compose_lam l b = lamn (List.length l) l b + +(* prodn n [xn:Tn;..;x1:T1;Gamma] b = (x1:T1)..(xn:Tn)b *) +let prodn n env b = + let open EConstr in + let rec prodrec = function + | (0, env, b) -> b + | (n, ((v,t)::l), b) -> prodrec (n-1, l, mkProd (v,t,b)) + | _ -> assert false + in + prodrec (n,env,b) + +(* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *) +let compose_prod l b = prodn (List.length l) l b + +type tcc_lemma_value = + | Undefined + | Value of constr + | Not_needed + +(* We only "purify" on exceptions. XXX: What is this doing here? *) +let funind_purify f x = + let st = Vernacstate.freeze_interp_state `No in + try f x + with e -> + let e = CErrors.push e in + Vernacstate.unfreeze_interp_state st; + Exninfo.iraise e -- cgit v1.2.3