From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- toplevel/auto_ind_decl.ml | 123 +++++++++++++++++++++++++--------------------- 1 file changed, 66 insertions(+), 57 deletions(-) (limited to 'toplevel/auto_ind_decl.ml') diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 26b54a73..7a89b9f5 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -19,6 +19,7 @@ open Termops open Declarations open Names open Globnames +open Nameops open Inductiveops open Tactics open Ind_tables @@ -54,6 +55,7 @@ exception InductiveWithProduct exception InductiveWithSort exception ParameterWithoutEquality of constant exception NonSingletonProp of inductive +exception DecidabilityMutualNotSupported let dl = Loc.ghost @@ -109,7 +111,7 @@ let check_bool_is_defined () = let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined") -let build_beq_scheme kn = +let build_beq_scheme mode kn = check_bool_is_defined (); (* fetching global env *) let env = Global.env() in @@ -177,23 +179,22 @@ let build_beq_scheme kn = let rec aux c = let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in match kind_of_term c with - | Rel x -> mkRel (x-nlist+ndx), Declareops.no_seff - | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Declareops.no_seff + | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants + | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Safe_typing.empty_private_constants | Cast (x,_,_) -> aux (applist (x,a)) | App _ -> assert false | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> - if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Declareops.no_seff + if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants else begin try let eq, eff = - let c, eff = find_scheme (!beq_scheme_kind_aux()) (kn',i) in + let c, eff = find_scheme ~mode (!beq_scheme_kind_aux()) (kn',i) in mkConst c, eff in let eqa, eff = let eqa, effs = List.split (List.map aux a) in Array.of_list eqa, - Declareops.union_side_effects - (Declareops.flatten_side_effects (List.rev effs)) - eff in + List.fold_left Safe_typing.concat_private eff (List.rev effs) + in let args = Array.append (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in @@ -236,7 +237,7 @@ let build_beq_scheme kn = let constrsi = constrs (3+nparrec) in let n = Array.length constrsi in let ar = Array.make n (Lazy.force ff) in - let eff = ref Declareops.no_seff in + let eff = ref Safe_typing.empty_private_constants in for i=0 to n-1 do let nb_cstr_args = List.length constrsi.(i).cs_args in let ar2 = Array.make n (Lazy.force ff) in @@ -254,7 +255,7 @@ let build_beq_scheme kn = (nb_cstr_args+ndx+1) cc in - eff := Declareops.union_side_effects eff' !eff; + eff := Safe_typing.concat_private eff' !eff; Array.set eqs ndx (mkApp (eqA, [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|] @@ -286,7 +287,7 @@ let build_beq_scheme kn = let names = Array.make nb_ind Anonymous and types = Array.make nb_ind mkSet and cores = Array.make nb_ind mkSet in - let eff = ref Declareops.no_seff in + let eff = ref Safe_typing.empty_private_constants in let u = Univ.Instance.empty in for i=0 to (nb_ind-1) do names.(i) <- Name (Id.of_string (rec_name i)); @@ -294,7 +295,7 @@ let build_beq_scheme kn = (mkArrow (mkFullInd ((kn,i),u) 1) (Lazy.force bb)); let c, eff' = make_one_eq i in cores.(i) <- c; - eff := Declareops.union_side_effects eff' !eff + eff := Safe_typing.concat_private eff' !eff done; (Array.init nb_ind (fun i -> let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in @@ -302,7 +303,7 @@ let build_beq_scheme kn = raise (NonSingletonProp (kn,i)); let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in create_input fix), - Evd.empty_evar_universe_context (* FIXME *)), + Evd.make_evar_universe_context (Global.env ()) None), !eff let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme @@ -328,7 +329,7 @@ let destruct_ind c = so from Ai we can find the the correct eq_Ai bl_ai or lb_ai *) (* used in the leib -> bool side*) -let do_replace_lb lb_scheme_key aavoid narg p q = +let do_replace_lb mode lb_scheme_key aavoid narg p q = let avoid = Array.of_list aavoid in let do_arg v offset = try @@ -338,7 +339,8 @@ let do_replace_lb lb_scheme_key aavoid narg p q = let rec find i = if Id.equal avoid.(n-i) s then avoid.(n-i-x) else (if i @@ -353,11 +355,11 @@ let do_replace_lb lb_scheme_key aavoid narg p q = ) in Proofview.Goal.nf_enter begin fun gl -> - let type_of_pq = Tacmach.New.of_old (fun gl -> pf_type_of gl p) gl in + let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in let u,v = destruct_ind type_of_pq in let lb_type_of_p = try - let c, eff = find_scheme lb_scheme_key (out_punivs u) (*FIXME*) in + let c, eff = find_scheme ~mode lb_scheme_key (out_punivs u) (*FIXME*) in Proofview.tclUNIT (mkConst c, eff) with Not_found -> (* spiwack: the format of this error message should probably @@ -369,7 +371,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q = Printer.pr_constr type_of_pq ++ str " first.") in - Proofview.tclZERO (Errors.UserError("",err_msg)) + Tacticals.New.tclZEROMSG err_msg in lb_type_of_p >>= fun (lb_type_of_p,eff) -> let lb_args = Array.append (Array.append @@ -385,7 +387,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q = end (* used in the bool -> leib side *) -let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = +let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let avoid = Array.of_list aavoid in let do_arg v offset = try @@ -395,7 +397,8 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let rec find i = if Id.equal avoid.(n-i) s then avoid.(n-i-x) else (if i @@ -414,7 +417,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = match (l1,l2) with | (t1::q1,t2::q2) -> Proofview.Goal.enter begin fun gl -> - let tt1 = Tacmach.New.pf_type_of gl t1 in + let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in if eq_constr t1 t2 then aux q1 q2 else ( let u,v = try destruct_ind tt1 @@ -456,28 +459,28 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = ) end | ([],[]) -> Proofview.tclUNIT () - | _ -> Proofview.tclZERO (UserError ("" , str"Both side of the equality must have the same arity.")) + | _ -> Tacticals.New.tclZEROMSG (str "Both side of the equality must have the same arity.") in begin try Proofview.tclUNIT (destApp lft) - with DestKO -> Proofview.tclZERO (UserError ("" , str"replace failed.")) + with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.") end >>= fun (ind1,ca1) -> begin try Proofview.tclUNIT (destApp rgt) - with DestKO -> Proofview.tclZERO (UserError ("" , str"replace failed.")) + with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.") end >>= fun (ind2,ca2) -> begin try Proofview.tclUNIT (out_punivs (destInd ind1)) with DestKO -> begin try Proofview.tclUNIT (fst (fst (destConstruct ind1))) - with DestKO -> Proofview.tclZERO (UserError ("" , str"The expected type is an inductive one.")) + with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.") end end >>= fun (sp1,i1) -> begin try Proofview.tclUNIT (out_punivs (destInd ind2)) with DestKO -> begin try Proofview.tclUNIT (fst (fst (destConstruct ind2))) - with DestKO -> Proofview.tclZERO (UserError ("" , str"The expected type is an inductive one.")) + with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.") end end >>= fun (sp2,i2) -> if not (eq_mind sp1 sp2) || not (Int.equal i1 i2) - then Proofview.tclZERO (UserError ("" , str"Eq should be on the same type")) + then Tacticals.New.tclZEROMSG (str "Eq should be on the same type") else aux (Array.to_list ca1) (Array.to_list ca2) (* @@ -502,8 +505,8 @@ let eqI ind l = (List.map (fun (_,seq,_,_)-> mkVar seq) list_id )) and e, eff = try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff - with Not_found -> error - ("The boolean equality on "^(string_of_mind (fst ind))^" is needed."); + with Not_found -> errorlabstrm "AutoIndDecl.eqI" + (str "The boolean equality on " ++ pr_mind (fst ind) ++ str " is needed."); in (if Array.equal eq_constr eA [||] then e else mkApp(e,eA)), eff (**********************************************************************) @@ -547,7 +550,7 @@ let compute_bl_goal ind lnamesparrec nparrec = (mkApp(Lazy.force eq,[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|])) ))), eff -let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec = +let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let avoid = ref [] in let first_intros = @@ -604,16 +607,16 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). if eq_gr (IndRef indeq) Coqlib.glob_eq then Tacticals.New.tclTHEN - (do_replace_bl bl_scheme_key ind + (do_replace_bl mode bl_scheme_key ind (!avoid) nparrec (ca.(2)) (ca.(1))) Auto.default_auto else - Proofview.tclZERO (UserError ("",str"Failure while solving Boolean->Leibniz.")) - | _ -> Proofview.tclZERO (UserError ("", str"Failure while solving Boolean->Leibniz.")) + Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.") + | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.") ) - | _ -> Proofview.tclZERO (UserError ("", str"Failure while solving Boolean->Leibniz.")) + | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.") end ] @@ -621,7 +624,12 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined") -let make_bl_scheme mind = +let side_effect_of_mode = function + | Declare.UserAutomaticRequest -> false + | Declare.InternalTacticRequest -> true + | Declare.UserIndividualRequest -> false + +let make_bl_scheme mode mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then errorlabstrm "" @@ -632,9 +640,10 @@ let make_bl_scheme mind = let lnonparrec,lnamesparrec = (* TODO subst *) context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in - let ctx = Evd.empty_evar_universe_context (*FIXME univs *) in - let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx bl_goal - (compute_bl_tact (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) + let ctx = Evd.make_evar_universe_context (Global.env ()) None in + let side_eff = side_effect_of_mode mode in + let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal + (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) in ([|ans|], ctx), eff @@ -684,7 +693,7 @@ let compute_lb_goal ind lnamesparrec nparrec = (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|])) ))), eff -let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec = +let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let avoid = ref [] in let first_intros = @@ -728,22 +737,22 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec = | App(c,ca) -> (match (kind_of_term ca.(1)) with | App(c',ca') -> let n = Array.length ca' in - do_replace_lb lb_scheme_key + do_replace_lb mode lb_scheme_key (!avoid) nparrec ca'.(n-2) ca'.(n-1) | _ -> - Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean.")) + Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.") ) | _ -> - Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean.")) + Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.") end ] end let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined") -let make_lb_scheme mind = +let make_lb_scheme mode mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then errorlabstrm "" @@ -754,11 +763,12 @@ let make_lb_scheme mind = let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in - let ctx = Evd.empty_evar_universe_context in - let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx lb_goal - (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) + let ctx = Evd.make_evar_universe_context (Global.env ()) None in + let side_eff = side_effect_of_mode mode in + let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal + (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) in - ([|ans|], ctx (* FIXME *)), eff + ([|ans|], ctx), eff let lb_scheme_kind = declare_mutual_scheme_object "_dec_lb" make_lb_scheme @@ -856,17 +866,15 @@ let compute_dec_tact ind lnamesparrec nparrec = let c, eff = find_scheme bl_scheme_kind ind in Proofview.tclUNIT (mkConst c,eff) with Not_found -> - Proofview.tclZERO (UserError ("",str"Error during the decidability part, boolean to leibniz"++ - str" equality is required.")) + Tacticals.New.tclZEROMSG (str "Error during the decidability part, boolean to leibniz equality is required.") end >>= fun (blI,eff') -> begin try let c, eff = find_scheme lb_scheme_kind ind in Proofview.tclUNIT (mkConst c,eff) with Not_found -> - Proofview.tclZERO (UserError ("",str"Error during the decidability part, leibniz to boolean"++ - str" equality is required.")) + Tacticals.New.tclZEROMSG (str "Error during the decidability part, leibniz to boolean equality is required.") end >>= fun (lbI,eff'') -> - let eff = (Declareops.union_side_effects eff'' (Declareops.union_side_effects eff' eff)) in + let eff = (Safe_typing.concat_private eff'' (Safe_typing.concat_private eff' eff)) in Tacticals.New.tclTHENLIST [ Proofview.tclEFFECTS eff; intros_using fresh_first_intros; @@ -917,22 +925,23 @@ let compute_dec_tact ind lnamesparrec nparrec = ] end -let make_eq_decidability mind = +let make_eq_decidability mode mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then - anomaly (Pp.str "Decidability lemma for mutual inductive types not supported"); + raise DecidabilityMutualNotSupported; let ind = (mind,0) in let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let u = Univ.Instance.empty in - let ctx = Evd.empty_evar_universe_context (* FIXME *)in + let ctx = Evd.make_evar_universe_context (Global.env ()) None in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in - let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx + let side_eff = side_effect_of_mode mode in + let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx (compute_dec_goal (ind,u) lnamesparrec nparrec) (compute_dec_tact ind lnamesparrec nparrec) in - ([|ans|], ctx), Declareops.no_seff + ([|ans|], ctx), Safe_typing.empty_private_constants let eq_dec_scheme_kind = declare_mutual_scheme_object "_eq_dec" make_eq_decidability -- cgit v1.2.3