summaryrefslogtreecommitdiff
path: root/toplevel/auto_ind_decl.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/auto_ind_decl.ml')
-rw-r--r--toplevel/auto_ind_decl.ml123
1 files changed, 66 insertions, 57 deletions
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<n then find (i+1)
- else error ("Var "^(Id.to_string s)^" seems unknown.")
+ else errorlabstrm "AutoIndDecl.do_replace_lb"
+ (str "Var " ++ pr_id s ++ str " seems unknown.")
)
in mkVar (find 1)
with e when Errors.noncritical e ->
@@ -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<n then find (i+1)
- else error ("Var "^(Id.to_string s)^" seems unknown.")
+ else errorlabstrm "AutoIndDecl.do_replace_bl"
+ (str "Var " ++ pr_id s ++ str " seems unknown.")
)
in mkVar (find 1)
with e when Errors.noncritical e ->
@@ -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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 23:51:06 +0000