aboutsummaryrefslogtreecommitdiffhomepage
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.ml144
1 files changed, 82 insertions, 62 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 04d0f3de4..1a1a4dfe7 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -25,6 +25,8 @@ open Ind_tables
open Misctypes
open Proofview.Notations
+let out_punivs = Univ.out_punivs
+
(**********************************************************************)
(* Generic synthesis of boolean equality *)
@@ -55,6 +57,8 @@ exception NonSingletonProp of inductive
let dl = Loc.ghost
+let constr_of_global g = lazy (Universes.constr_of_global g)
+
(* Some pre declaration of constant we are going to use *)
let bb = constr_of_global Coqlib.glob_bool
@@ -93,7 +97,7 @@ let destruct_on c =
None (None,None) None
(* reconstruct the inductive with the correct deBruijn indexes *)
-let mkFullInd ind n =
+let mkFullInd (ind,u) n =
let mib = Global.lookup_mind (fst ind) in
let nparams = mib.mind_nparams in
let nparrec = mib.mind_nparams_rec in
@@ -101,12 +105,12 @@ let mkFullInd ind n =
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
if nparrec > 0
- then mkApp (mkInd ind,
+ then mkApp (mkIndU (ind,u),
Array.of_list(extended_rel_list (nparrec+n) lnamesparrec))
- else mkInd ind
+ else mkIndU (ind,u)
let check_bool_is_defined () =
- try let _ = Global.type_of_global Coqlib.glob_bool in ()
+ try let _ = Global.type_of_global_unsafe Coqlib.glob_bool in ()
with e when Errors.noncritical e -> raise (UndefinedCst "bool")
let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
@@ -142,7 +146,7 @@ let build_beq_scheme kn =
let eqs_typ = List.map (fun aa ->
let a = lift !lift_cnt aa in
incr lift_cnt;
- myArrow a (myArrow a bb)
+ myArrow a (myArrow a (Lazy.force bb))
) ext_rel_list in
let eq_input = List.fold_left2
@@ -159,11 +163,12 @@ let build_beq_scheme kn =
t a) eq_input lnamesparrec
in
let make_one_eq cur =
- let ind = kn,cur in
+ let u = Univ.Instance.empty in
+ let ind = (kn,cur),u (* FIXME *) in
(* current inductive we are working on *)
- let cur_packet = mib.mind_packets.(snd ind) in
+ let cur_packet = mib.mind_packets.(snd (fst ind)) in
(* Inductive toto : [rettyp] := *)
- let rettyp = Inductive.type_of_inductive env (mib,cur_packet) in
+ let rettyp = Inductive.type_of_inductive env ((mib,cur_packet),u) in
(* split rettyp in a list without the non rec params and the last ->
e.g. Inductive vec (A:Set) : nat -> Set := ... will do [nat] *)
let rettyp_l = quick_chop nparrec (deconstruct_type rettyp) in
@@ -182,7 +187,7 @@ let build_beq_scheme kn =
| Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Declareops.no_seff
| Cast (x,_,_) -> aux (applist (x,a))
| App _ -> assert false
- | Ind (kn',i as ind') ->
+ | Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Declareops.no_seff
else begin
try
@@ -200,16 +205,17 @@ let build_beq_scheme kn =
(Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in
if Int.equal (Array.length args) 0 then eq, eff
else mkApp (eq, args), eff
- with Not_found -> raise(EqNotFound (ind',ind))
+ with Not_found -> raise(EqNotFound (ind', fst ind))
end
| Sort _ -> raise InductiveWithSort
| Prod _ -> raise InductiveWithProduct
| Lambda _-> raise (EqUnknown "Lambda")
| LetIn _ -> raise (EqUnknown "LetIn")
| Const kn ->
- (match Environ.constant_opt_value env kn with
- | None -> raise (ParameterWithoutEquality kn)
+ (match Environ.constant_opt_value_in env kn with
+ | None -> raise (ParameterWithoutEquality (fst kn))
| Some c -> aux (applist (c,a)))
+ | Proj _ -> raise (EqUnknown "Proj")
| Construct _ -> raise (EqUnknown "Construct")
| Case _ -> raise (EqUnknown "Case")
| CoFix _ -> raise (EqUnknown "CoFix")
@@ -224,28 +230,28 @@ let build_beq_scheme kn =
List.fold_left (fun a b -> mkLambda(Anonymous,b,a))
(mkLambda (Anonymous,
mkFullInd ind (n+3+(List.length rettyp_l)+nb_ind-1),
- bb))
+ (Lazy.force bb)))
(List.rev rettyp_l) in
(* make_one_eq *)
(* do the [| C1 ... => match Y with ... end
...
Cn => match Y with ... end |] part *)
- let ci = make_case_info env ind MatchStyle in
+ let ci = make_case_info env (fst ind) MatchStyle in
let constrs n = get_constructors env (make_ind_family (ind,
extended_rel_list (n+nb_ind-1) mib.mind_params_ctxt)) in
let constrsi = constrs (3+nparrec) in
let n = Array.length constrsi in
- let ar = Array.make n ff in
- let eff = ref Declareops.no_seff in
+ let ar = Array.make n (Lazy.force ff) in
+ let eff = ref Declareops.no_seff in
for i=0 to n-1 do
let nb_cstr_args = List.length constrsi.(i).cs_args in
- let ar2 = Array.make n ff in
+ let ar2 = Array.make n (Lazy.force ff) in
let constrsj = constrs (3+nparrec+nb_cstr_args) in
for j=0 to n-1 do
if Int.equal i j then
ar2.(j) <- let cc = (match nb_cstr_args with
- | 0 -> tt
- | _ -> let eqs = Array.make nb_cstr_args tt in
+ | 0 -> Lazy.force tt
+ | _ -> let eqs = Array.make nb_cstr_args (Lazy.force tt) in
for ndx = 0 to nb_cstr_args-1 do
let _,_,cc = List.nth constrsi.(i).cs_args ndx in
let eqA, eff' = compute_A_equality rel_list
@@ -270,7 +276,7 @@ let build_beq_scheme kn =
(constrsj.(j).cs_args)
)
else ar2.(j) <- (List.fold_left (fun a (p,q,r) ->
- mkLambda (p,r,a)) ff (constrsj.(j).cs_args) )
+ mkLambda (p,r,a)) (Lazy.force ff) (constrsj.(j).cs_args) )
done;
ar.(i) <- (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a))
@@ -287,21 +293,23 @@ let build_beq_scheme kn =
types = Array.make nb_ind mkSet and
cores = Array.make nb_ind mkSet in
let eff = ref Declareops.no_seff in
+ let u = Univ.Instance.empty in
for i=0 to (nb_ind-1) do
names.(i) <- Name (Id.of_string (rec_name i));
- types.(i) <- mkArrow (mkFullInd (kn,i) 0)
- (mkArrow (mkFullInd (kn,i) 1) bb);
+ types.(i) <- mkArrow (mkFullInd ((kn,i),u) 0)
+ (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
done;
- Array.init nb_ind (fun i ->
+ (Array.init nb_ind (fun i ->
let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in
- if not (Sorts.List.mem InSet kelim) then
- raise (NonSingletonProp (kn,i));
- let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in
- create_input fix),
- !eff
+ if not (Sorts.List.mem InSet kelim) then
+ 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 *)),
+ !eff
let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme
@@ -343,8 +351,8 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
(* if this happen then the args have to be already declared as a
Parameter*)
(
- let mp,dir,lbl = repr_con (destConst v) in
- mkConst (make_con mp dir (Label.make (
+ let mp,dir,lbl = repr_con (fst (destConst v)) in
+ mkConst (make_con mp dir (mk_label (
if Int.equal offset 1 then ("eq_"^(Label.to_string lbl))
else ((Label.to_string lbl)^"_lb")
)))
@@ -355,7 +363,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
let u,v = destruct_ind type_of_pq
in let lb_type_of_p =
try
- let c, eff = find_scheme lb_scheme_key u in
+ let c, eff = find_scheme 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
@@ -383,7 +391,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 aavoid narg lft rgt =
+let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
let avoid = Array.of_list aavoid in
let do_arg v offset =
try
@@ -400,8 +408,8 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
(* if this happen then the args have to be already declared as a
Parameter*)
(
- let mp,dir,lbl = repr_con (destConst v) in
- mkConst (make_con mp dir (Label.make (
+ let mp,dir,lbl = repr_con (fst (destConst v)) in
+ mkConst (make_con mp dir (mk_label (
if Int.equal offset 1 then ("eq_"^(Label.to_string lbl))
else ((Label.to_string lbl)^"_bl")
)))
@@ -417,13 +425,13 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
else (
let u,v = try destruct_ind tt1
(* trick so that the good sequence is returned*)
- with e when Errors.noncritical e -> ind,[||]
- in if eq_ind u ind
+ with e when Errors.noncritical e -> indu,[||]
+ in if eq_ind (fst u) ind
then Tacticals.New.tclTHENLIST [Equality.replace t1 t2; Auto.default_auto ; aux q1 q2 ]
else (
let bl_t1, eff =
try
- let c, eff = find_scheme bl_scheme_key u in
+ let c, eff = find_scheme bl_scheme_key (out_punivs u) (*FIXME*) in
mkConst c, eff
with Not_found ->
(* spiwack: the format of this error message should probably
@@ -462,15 +470,15 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
begin try Proofview.tclUNIT (destApp rgt)
with DestKO -> Proofview.tclZERO (UserError ("" , str"replace failed."))
end >>= fun (ind2,ca2) ->
- begin try Proofview.tclUNIT (destInd ind1)
+ begin try Proofview.tclUNIT (out_punivs (destInd ind1))
with DestKO ->
- begin try Proofview.tclUNIT (fst (destConstruct ind1))
+ begin try Proofview.tclUNIT (fst (fst (destConstruct ind1)))
with DestKO -> Proofview.tclZERO (UserError ("" , str"The expected type is an inductive one."))
end
end >>= fun (sp1,i1) ->
- begin try Proofview.tclUNIT (destInd ind2)
+ begin try Proofview.tclUNIT (out_punivs (destInd ind2))
with DestKO ->
- begin try Proofview.tclUNIT (fst (destConstruct ind2))
+ begin try Proofview.tclUNIT (fst (fst (destConstruct ind2)))
with DestKO -> Proofview.tclZERO (UserError ("" , str"The expected type is an inductive one."))
end
end >>= fun (sp2,i2) ->
@@ -517,15 +525,15 @@ let compute_bl_goal ind lnamesparrec nparrec =
mkNamedProd x (mkVar s) (
mkNamedProd y (mkVar s) (
mkArrow
- ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|]))
- ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|]))
+ ( mkApp(Lazy.force eq,[|(Lazy.force bb);mkApp(mkVar seq,[|mkVar x;mkVar y|]);(Lazy.force tt)|]))
+ ( mkApp(Lazy.force eq,[|mkVar s;mkVar x;mkVar y|]))
))
) list_id in
let bl_input = List.fold_left2 ( fun a (s,_,sbl,_) b ->
mkNamedProd sbl b a
) c (List.rev list_id) (List.rev bl_typ) in
let eqs_typ = List.map (fun (s,_,_,_) ->
- mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,bb))
+ mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,(Lazy.force bb)))
) list_id in
let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
mkNamedProd seq b a
@@ -536,12 +544,13 @@ let compute_bl_goal ind lnamesparrec nparrec =
in
let n = Id.of_string "x" and
m = Id.of_string "y" in
+ let u = Univ.Instance.empty in
create_input (
- mkNamedProd n (mkFullInd ind nparrec) (
- mkNamedProd m (mkFullInd ind (nparrec+1)) (
+ mkNamedProd n (mkFullInd (ind,u) nparrec) (
+ mkNamedProd m (mkFullInd (ind,u) (nparrec+1)) (
mkArrow
- (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|]))
- (mkApp(eq,[|mkFullInd ind (nparrec+3);mkVar n;mkVar m|]))
+ (mkApp(Lazy.force eq,[|(Lazy.force bb);mkApp(eqI,[|mkVar n;mkVar m|]);(Lazy.force tt)|]))
+ (mkApp(Lazy.force eq,[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|]))
))), eff
let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec =
@@ -600,7 +609,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
match (kind_of_term gl) with
| App (c,ca) -> (
match (kind_of_term c) with
- | Ind indeq ->
+ | Ind (indeq, u) ->
if eq_gr (IndRef indeq) Coqlib.glob_eq
then
Tacticals.New.tclTHEN
@@ -629,12 +638,14 @@ let make_bl_scheme mind =
let ind = (mind,0) in
let nparams = mib.mind_nparams in
let nparrec = mib.mind_nparams_rec in
- let lnonparrec,lnamesparrec =
+ 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
- [|fst (Pfedit.build_by_tactic (Global.env()) bl_goal
- (compute_bl_tact (!bl_scheme_kind_aux()) ind lnamesparrec nparrec))|],
- eff
+ let ctx = Univ.ContextSet.empty (*FIXME univs *) in
+ let (ans, _, _) = Pfedit.build_by_tactic (Global.env()) (bl_goal, ctx)
+ (compute_bl_tact (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec)
+ in
+ ([|ans|], Evd.empty_evar_universe_context), eff
let bl_scheme_kind = declare_mutual_scheme_object "_dec_bl" make_bl_scheme
@@ -645,6 +656,7 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind
let compute_lb_goal ind lnamesparrec nparrec =
let list_id = list_id lnamesparrec in
+ let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
let eqI, eff = eqI ind lnamesparrec in
let create_input c =
let x = Id.of_string "x" and
@@ -672,11 +684,12 @@ let compute_lb_goal ind lnamesparrec nparrec =
in
let n = Id.of_string "x" and
m = Id.of_string "y" in
+ let u = Univ.Instance.empty in
create_input (
- mkNamedProd n (mkFullInd ind nparrec) (
- mkNamedProd m (mkFullInd ind (nparrec+1)) (
+ mkNamedProd n (mkFullInd (ind,u) nparrec) (
+ mkNamedProd m (mkFullInd (ind,u) (nparrec+1)) (
mkArrow
- (mkApp(eq,[|mkFullInd ind (nparrec+2);mkVar n;mkVar m|]))
+ (mkApp(eq,[|mkFullInd (ind,u) (nparrec+2);mkVar n;mkVar m|]))
(mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|]))
))), eff
@@ -750,9 +763,10 @@ 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
- [|fst (Pfedit.build_by_tactic (Global.env()) lb_goal
- (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec))|],
- eff
+ let (ans, _, _) = Pfedit.build_by_tactic (Global.env()) (lb_goal,Univ.ContextSet.empty)
+ (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
+ in
+ ([|ans|], Evd.empty_evar_universe_context (* FIXME *)), eff
let lb_scheme_kind = declare_mutual_scheme_object "_dec_lb" make_lb_scheme
@@ -768,6 +782,7 @@ let check_not_is_defined () =
(* {n=m}+{n<>m} part *)
let compute_dec_goal ind lnamesparrec nparrec =
check_not_is_defined ();
+ let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
let list_id = list_id lnamesparrec in
let create_input c =
let x = Id.of_string "x" and
@@ -818,6 +833,8 @@ let compute_dec_goal ind lnamesparrec nparrec =
)
let compute_dec_tact ind lnamesparrec nparrec =
+ let eq = Lazy.force eq and tt = Lazy.force tt
+ and ff = Lazy.force ff and bb = Lazy.force bb in
let list_id = list_id lnamesparrec in
let eqI, eff = eqI ind lnamesparrec in
let avoid = ref [] in
@@ -915,11 +932,14 @@ let make_eq_decidability mind =
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 lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
- [|fst (Pfedit.build_by_tactic (Global.env())
- (compute_dec_goal ind lnamesparrec nparrec)
- (compute_dec_tact ind lnamesparrec nparrec))|], Declareops.no_seff
+ let (ans, _, _) = Pfedit.build_by_tactic (Global.env())
+ (compute_dec_goal (ind,u) lnamesparrec nparrec, Univ.ContextSet.empty)
+ (compute_dec_tact ind lnamesparrec nparrec)
+ in
+ ([|ans|], Evd.empty_evar_universe_context (* FIXME *)), Declareops.no_seff
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-06-11 00:25:33 +0000