aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/auto_ind_decl.ml144
-rw-r--r--toplevel/auto_ind_decl.mli9
-rw-r--r--toplevel/cerrors.ml16
-rw-r--r--toplevel/class.ml68
-rw-r--r--toplevel/class.mli21
-rw-r--r--toplevel/classes.ml107
-rw-r--r--toplevel/classes.mli5
-rw-r--r--toplevel/command.ml331
-rw-r--r--toplevel/command.mli42
-rw-r--r--toplevel/coqtop.ml1
-rw-r--r--toplevel/discharge.ml17
-rw-r--r--toplevel/discharge.mli2
-rw-r--r--toplevel/himsg.ml32
-rw-r--r--toplevel/ind_tables.ml40
-rw-r--r--toplevel/ind_tables.mli7
-rw-r--r--toplevel/indschemes.ml44
-rw-r--r--toplevel/metasyntax.ml4
-rw-r--r--toplevel/obligations.ml184
-rw-r--r--toplevel/obligations.mli4
-rw-r--r--toplevel/record.ml203
-rw-r--r--toplevel/record.mli7
-rw-r--r--toplevel/search.ml7
-rw-r--r--toplevel/usage.ml1
-rw-r--r--toplevel/vernacentries.ml162
-rw-r--r--toplevel/whelp.ml412
25 files changed, 941 insertions, 529 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
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index 6509a7d3b..21362c973 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.mli
@@ -26,17 +26,16 @@ exception ParameterWithoutEquality of constant
exception NonSingletonProp of inductive
val beq_scheme_kind : mutual scheme_kind
-val build_beq_scheme : mutual_inductive -> constr array * Declareops.side_effects
+val build_beq_scheme : mutual_scheme_object_function
(** {6 Build equivalence between boolean equality and Leibniz equality } *)
val lb_scheme_kind : mutual scheme_kind
-val make_lb_scheme : mutual_inductive -> constr array * Declareops.side_effects
-
+val make_lb_scheme : mutual_scheme_object_function
val bl_scheme_kind : mutual scheme_kind
-val make_bl_scheme : mutual_inductive -> constr array * Declareops.side_effects
+val make_bl_scheme : mutual_scheme_object_function
(** {6 Build decidability of equality } *)
val eq_dec_scheme_kind : mutual scheme_kind
-val make_eq_decidability : mutual_inductive -> constr array * Declareops.side_effects
+val make_eq_decidability : mutual_scheme_object_function
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 0186b08ac..f5cc2015b 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -58,22 +58,10 @@ let wrap_vernac_error exn strm =
Exninfo.copy exn e
let process_vernac_interp_error exn = match exn with
- | Univ.UniverseInconsistency (o,u,v,p) ->
- let pr_rel r =
- match r with
- Univ.Eq -> str"=" | Univ.Lt -> str"<" | Univ.Le -> str"<=" in
- let reason = match p with
- [] -> mt()
- | _::_ ->
- str " because" ++ spc() ++ Univ.pr_uni v ++
- prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ Univ.pr_uni v)
- p ++
- (if Univ.Universe.equal (snd (List.last p)) u then mt() else
- (spc() ++ str "= " ++ Univ.pr_uni u)) in
+ | Univ.UniverseInconsistency i ->
let msg =
if !Constrextern.print_universes then
- spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++
- pr_rel o ++ spc() ++ Univ.pr_uni v ++ reason ++ str")"
+ str "." ++ spc() ++ Univ.explain_universe_inconsistency i
else
mt() in
wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".")
diff --git a/toplevel/class.ml b/toplevel/class.ml
index a9cb6ca5e..d54efb632 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -66,7 +66,7 @@ let explain_coercion_error g = function
(* Verifications pour l'ajout d'une classe *)
let check_reference_arity ref =
- if not (Reductionops.is_arity (Global.env()) Evd.empty (Global.type_of_global ref)) then
+ if not (Reductionops.is_arity (Global.env()) Evd.empty (Global.type_of_global_unsafe ref)) then
raise (CoercionError (NotAClass ref))
let check_arity = function
@@ -118,19 +118,19 @@ l'indice de la classe source dans la liste lp
let get_source lp source =
match source with
| None ->
- let (cl1,lv1) =
+ let (cl1,u1,lv1) =
match lp with
| [] -> raise Not_found
| t1::_ -> find_class_type Evd.empty t1
in
- (cl1,lv1,1)
+ (cl1,u1,lv1,1)
| Some cl ->
let rec aux = function
| [] -> raise Not_found
| t1::lt ->
try
- let cl1,lv1 = find_class_type Evd.empty t1 in
- if cl_typ_eq cl cl1 then cl1,lv1,(List.length lt+1)
+ let cl1,u1,lv1 = find_class_type Evd.empty t1 in
+ if cl_typ_eq cl cl1 then cl1,u1,lv1,(List.length lt+1)
else raise Not_found
with Not_found -> aux lt
in aux (List.rev lp)
@@ -139,7 +139,7 @@ let get_target t ind =
if (ind > 1) then
CL_FUN
else
- fst (find_class_type Evd.empty t)
+ pi1 (find_class_type Evd.empty t)
let prods_of t =
let rec aux acc d = match kind_of_term d with
@@ -177,12 +177,12 @@ let error_not_transparent source =
errorlabstrm "build_id_coercion"
(pr_class source ++ str " must be a transparent constant.")
-let build_id_coercion idf_opt source =
+let build_id_coercion idf_opt source poly =
let env = Global.env () in
- let vs = match source with
- | CL_CONST sp -> mkConst sp
+ let vs, ctx = match source with
+ | CL_CONST sp -> Universes.fresh_global_instance env (ConstRef sp)
| _ -> error_not_transparent source in
- let c = match constant_opt_value env (destConst vs) with
+ let c = match constant_opt_value_in env (destConst vs) with
| Some c -> c
| None -> error_not_transparent source in
let lams,t = decompose_lam_assum c in
@@ -211,7 +211,7 @@ let build_id_coercion idf_opt source =
match idf_opt with
| Some idf -> idf
| None ->
- let cl,_ = find_class_type Evd.empty t in
+ let cl,u,_ = find_class_type Evd.empty t in
Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
(ident_key_of_class cl))
in
@@ -221,6 +221,9 @@ let build_id_coercion idf_opt source =
(mkCast (val_f, DEFAULTcast, typ_f),Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = Some typ_f;
+ const_entry_proj = None;
+ const_entry_polymorphic = poly;
+ const_entry_universes = Univ.ContextSet.to_context ctx;
const_entry_opaque = false;
const_entry_inline_code = true;
const_entry_feedback = None;
@@ -244,14 +247,14 @@ booleen "coercion identite'?"
lorque source est None alors target est None aussi.
*)
-let add_new_coercion_core coef stre source target isid =
+let add_new_coercion_core coef stre poly source target isid =
check_source source;
- let t = Global.type_of_global coef in
+ let t = Global.type_of_global_unsafe coef in
if coercion_exists coef then raise (CoercionError AlreadyExists);
let tg,lp = prods_of t in
let llp = List.length lp in
if Int.equal llp 0 then raise (CoercionError NotAFunction);
- let (cls,lvs,ind) =
+ let (cls,us,lvs,ind) =
try
get_source lp source
with Not_found ->
@@ -275,44 +278,45 @@ let add_new_coercion_core coef stre source target isid =
in
declare_coercion coef ~local ~isid ~src:cls ~target:clt ~params:(List.length lvs)
-let try_add_new_coercion_core ref ~local c d e =
- try add_new_coercion_core ref (loc_of_bool local) c d e
+
+let try_add_new_coercion_core ref ~local c d e f =
+ try add_new_coercion_core ref (loc_of_bool local) c d e f
with CoercionError e ->
errorlabstrm "try_add_new_coercion_core"
(explain_coercion_error ref e ++ str ".")
-let try_add_new_coercion ref ~local =
- try_add_new_coercion_core ref ~local None None false
+let try_add_new_coercion ref ~local poly =
+ try_add_new_coercion_core ref ~local poly None None false
-let try_add_new_coercion_subclass cl ~local =
- let coe_ref = build_id_coercion None cl in
- try_add_new_coercion_core coe_ref ~local (Some cl) None true
+let try_add_new_coercion_subclass cl ~local poly =
+ let coe_ref = build_id_coercion None cl poly in
+ try_add_new_coercion_core coe_ref ~local poly (Some cl) None true
-let try_add_new_coercion_with_target ref ~local ~source ~target =
- try_add_new_coercion_core ref ~local (Some source) (Some target) false
+let try_add_new_coercion_with_target ref ~local poly ~source ~target =
+ try_add_new_coercion_core ref ~local poly (Some source) (Some target) false
-let try_add_new_identity_coercion id ~local ~source ~target =
- let ref = build_id_coercion (Some id) source in
- try_add_new_coercion_core ref ~local (Some source) (Some target) true
+let try_add_new_identity_coercion id ~local poly ~source ~target =
+ let ref = build_id_coercion (Some id) source poly in
+ try_add_new_coercion_core ref ~local poly (Some source) (Some target) true
-let try_add_new_coercion_with_source ref ~local ~source =
- try_add_new_coercion_core ref ~local (Some source) None false
+let try_add_new_coercion_with_source ref ~local poly ~source =
+ try_add_new_coercion_core ref ~local poly (Some source) None false
-let add_coercion_hook local ref =
+let add_coercion_hook poly local ref =
let stre = match local with
| Local -> true
| Global -> false
| Discharge -> assert false
in
- let () = try_add_new_coercion ref stre in
+ let () = try_add_new_coercion ref stre poly in
let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
Flags.if_verbose msg_info msg
-let add_subclass_hook local ref =
+let add_subclass_hook poly local ref =
let stre = match local with
| Local -> true
| Global -> false
| Discharge -> assert false
in
let cl = class_of_global ref in
- try_add_new_coercion_subclass cl stre
+ try_add_new_coercion_subclass cl stre poly
diff --git a/toplevel/class.mli b/toplevel/class.mli
index 8bb3eb7ce..d472bd984 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -14,32 +14,35 @@ open Globnames
(** [try_add_new_coercion_with_target ref s src tg] declares [ref] as a coercion
from [src] to [tg] *)
-val try_add_new_coercion_with_target : global_reference -> local:bool ->
+val try_add_new_coercion_with_target : global_reference -> local:bool ->
+ Decl_kinds.polymorphic ->
source:cl_typ -> target:cl_typ -> unit
(** [try_add_new_coercion ref s] declares [ref], assumed to be of type
[(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *)
-val try_add_new_coercion : global_reference -> local:bool -> unit
+val try_add_new_coercion : global_reference -> local:bool ->
+ Decl_kinds.polymorphic -> unit
(** [try_add_new_coercion_subclass cst s] expects that [cst] denotes a
transparent constant which unfolds to some class [tg]; it declares
an identity coercion from [cst] to [tg], named something like
["Id_cst_tg"] *)
-val try_add_new_coercion_subclass : cl_typ -> local:bool -> unit
+val try_add_new_coercion_subclass : cl_typ -> local:bool ->
+ Decl_kinds.polymorphic -> unit
(** [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion
from [src] to [tg] where the target is inferred from the type of [ref] *)
-val try_add_new_coercion_with_source : global_reference -> local:bool ->
- source:cl_typ -> unit
+val try_add_new_coercion_with_source : global_reference -> local:bool ->
+ Decl_kinds.polymorphic -> source:cl_typ -> unit
(** [try_add_new_identity_coercion id s src tg] enriches the
environment with a new definition of name [id] declared as an
identity coercion from [src] to [tg] *)
-val try_add_new_identity_coercion : Id.t -> local:bool ->
- source:cl_typ -> target:cl_typ -> unit
+val try_add_new_identity_coercion : Id.t -> local:bool ->
+ Decl_kinds.polymorphic -> source:cl_typ -> target:cl_typ -> unit
-val add_coercion_hook : unit Tacexpr.declaration_hook
+val add_coercion_hook : Decl_kinds.polymorphic -> unit Tacexpr.declaration_hook
-val add_subclass_hook : unit Tacexpr.declaration_hook
+val add_subclass_hook : Decl_kinds.polymorphic -> unit Tacexpr.declaration_hook
val class_of_global : global_reference -> cl_typ
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 2e17f646b..cf47abf44 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -33,11 +33,14 @@ let set_typeclass_transparency c local b =
let _ =
Hook.set Typeclasses.add_instance_hint_hook
- (fun inst path local pri ->
+ (fun inst path local pri poly ->
+ let inst' = match inst with IsConstr c -> Auto.IsConstr (c, Univ.ContextSet.empty)
+ | IsGlobal gr -> Auto.IsGlobRef gr
+ in
Flags.silently (fun () ->
Auto.add_hints local [typeclasses_db]
(Auto.HintsResolveEntry
- [pri, false, Auto.PathHints path, inst])) ());
+ [pri, poly, false, Auto.PathHints path, inst'])) ());
Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
Hook.set Typeclasses.classes_transparent_state_hook
(fun () -> Auto.Hint_db.transparent_state (Auto.searchtable_map typeclasses_db))
@@ -52,10 +55,11 @@ let declare_class g =
(** TODO: add subinstances *)
let existing_instance glob g pri =
let c = global g in
- let instance = Typing.type_of (Global.env ()) Evd.empty (constr_of_global c) in
+ let instance = Typing.type_of (Global.env ()) Evd.empty (Universes.constr_of_global c) in
let _, r = decompose_prod_assum instance in
match class_of_constr r with
- | Some (_, (tc, _)) -> add_instance (new_instance tc pri glob c)
+ | Some (_, ((tc,u), _)) -> add_instance (new_instance tc pri glob
+ (*FIXME*) (Flags.use_polymorphic_flag ()) c)
| None -> user_err_loc (loc_of_reference g, "declare_instance",
Pp.str "Constant does not build instances of a declared type class.")
@@ -95,27 +99,22 @@ let instance_hook k pri global imps ?hook cst =
Typeclasses.declare_instance pri (not global) cst;
(match hook with Some h -> h cst | None -> ())
-let declare_instance_constant k pri global imps ?hook id term termtype =
+let declare_instance_constant k pri global imps ?hook id poly uctx term termtype =
let kind = IsDefinition Instance in
- let entry = {
- const_entry_body = Future.from_val term;
- const_entry_secctx = None;
- const_entry_type = Some termtype;
- const_entry_opaque = false;
- const_entry_inline_code = false;
- const_entry_feedback = None;
- } in
+ let entry =
+ Declare.definition_entry ~types:termtype ~poly ~univs:uctx term
+ in
let cdecl = (DefinitionEntry entry, kind) in
let kn = Declare.declare_constant id cdecl in
Declare.definition_message id;
instance_hook k pri global imps ?hook (ConstRef kn);
id
-let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
+let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) props
?(generalize=true)
?(tac:unit Proofview.tactic option) ?hook pri =
let env = Global.env() in
- let evars = ref Evd.empty in
+ let evars = ref (Evd.from_env env) in
let tclass, ids =
match bk with
| Implicit ->
@@ -129,15 +128,19 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
cl
| Explicit -> cl, Id.Set.empty
in
- let tclass = if generalize then CGeneralization (Loc.ghost, Implicit, Some AbsPi, tclass) else tclass in
- let k, cty, ctx', ctx, len, imps, subst =
+ let tclass =
+ if generalize then CGeneralization (Loc.ghost, Implicit, Some AbsPi, tclass)
+ else tclass
+ in
+ let k, u, cty, ctx', ctx, len, imps, subst =
let impls, ((env', ctx), imps) = interp_context_evars evars env ctx in
let c', imps' = interp_type_evars_impls ~impls evars env' tclass in
let len = List.length ctx in
let imps = imps @ Impargs.lift_implicits len imps' in
let ctx', c = decompose_prod_assum c' in
let ctx'' = ctx' @ ctx in
- let cl, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) c in
+ let k, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) c in
+ let cl, u = Typeclasses.typeclass_univ_instance k in
let _, args =
List.fold_right (fun (na, b, t) (args, args') ->
match b with
@@ -145,7 +148,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
| Some b -> (args, substl args' b :: args'))
(snd cl.cl_context) (args, [])
in
- cl, c', ctx', ctx, len, imps, args
+ cl, u, c', ctx', ctx, len, imps, args
in
let id =
match snd instid with
@@ -161,19 +164,23 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
let env' = push_rel_context ctx env in
evars := Evarutil.nf_evar_map !evars;
evars := resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env !evars;
- let sigma = !evars in
- let subst = List.map (Evarutil.nf_evar sigma) subst in
+ let subst = List.map (Evarutil.nf_evar !evars) subst in
if abstract then
begin
- let _, ty_constr = instance_constructor k (List.rev subst) in
+ let subst = List.fold_left2
+ (fun subst' s (_, b, _) -> if Option.is_empty b then s :: subst' else subst')
+ [] subst (snd k.cl_context)
+ in
+ let (_, ty_constr) = instance_constructor (k,u) subst in
let termtype =
let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
- Evarutil.nf_evar !evars t
+ fst (Evarutil.e_nf_evars_and_universes evars) t
in
Evarutil.check_evars env Evd.empty !evars termtype;
+ let ctx = Evd.universe_context !evars in
let cst = Declare.declare_constant ~internal:Declare.KernelSilent id
(Entries.ParameterEntry
- (None,termtype,None), Decl_kinds.IsAssumption Decl_kinds.Logical)
+ (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
in instance_hook k None global imps ?hook (ConstRef cst); id
end
else (
@@ -203,11 +210,11 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
let props, rest =
List.fold_left
(fun (props, rest) (id,b,_) ->
- if Option.is_empty b then
- try
- let is_id (id', _) = match id, get_id id' with
- | Name id, (_, id') -> Id.equal id id'
- | Anonymous, _ -> false
+ if Option.is_empty b then
+ try
+ let is_id (id', _) = match id, get_id id' with
+ | Name id, (_, id') -> Id.equal id id'
+ | Anonymous, _ -> false
in
let (loc_mid, c) =
List.find is_id rest
@@ -242,7 +249,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
(fun subst' s (_, b, _) -> if Option.is_empty b then s :: subst' else subst')
[] subst (k.cl_props @ snd k.cl_context)
in
- let app, ty_constr = instance_constructor k subst in
+ let (app, ty_constr) = instance_constructor (k,u) subst in
let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
Some term, termtype
@@ -259,17 +266,19 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false
env !evars
in
- let termtype = Evarutil.nf_evar !evars termtype in
+ let _ = evars := Evarutil.nf_evar_map_undefined !evars in
+ let evm, nf = Evarutil.nf_evar_map_universes !evars in
+ let termtype = nf termtype in
let _ = (* Check that the type is free of evars now. *)
- Evarutil.check_evars env Evd.empty !evars termtype
+ Evarutil.check_evars env Evd.empty evm termtype
in
- let term = Option.map (Evarutil.nf_evar !evars) term in
- let evm = Evarutil.nf_evar_map_undefined !evars in
+ let term = Option.map nf term in
if not (Evd.has_undefined evm) && not (Option.is_empty term) then
+ let ctx = Evd.universe_context evm in
declare_instance_constant k pri global imps ?hook id
- (Option.get term,Declareops.no_seff) termtype
+ poly ctx (Option.get term) termtype
else begin
- let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
+ let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
if Flags.is_program_mode () then
let hook vis gr =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
@@ -280,17 +289,18 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
match term with
| Some t ->
let obls, _, constr, typ =
- Obligations.eterm_obligations env id !evars 0 t termtype
+ Obligations.eterm_obligations env id evm 0 t termtype
in obls, Some constr, typ
| None -> [||], None, termtype
in
+ let ctx = Evd.get_universe_context_set evm in
ignore (Obligations.add_definition id ?term:constr
- typ ~kind:(Global,Instance) ~hook obls);
+ typ ctx ~kind:(Global,poly,Instance) ~hook obls);
id
else
(Flags.silently
(fun () ->
- Lemmas.start_proof id kind termtype
+ Lemmas.start_proof id kind (termtype, Evd.get_universe_context_set evm)
(fun _ -> instance_hook k pri global imps ?hook);
(* spiwack: I don't know what to do with the status here. *)
if not (Option.is_empty term) then
@@ -315,7 +325,8 @@ let context l =
let env = Global.env() in
let evars = ref Evd.empty in
let _, ((env', fullctx), impls) = interp_context_evars evars env l in
- let fullctx = Evarutil.nf_rel_context_evar !evars fullctx in
+ let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in
+ let fullctx = Context.map_rel_context subst fullctx in
let ce t = Evarutil.check_evars env Evd.empty !evars t in
let () = List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx in
let ctx =
@@ -323,13 +334,17 @@ let context l =
with e when Errors.noncritical e ->
error "Anonymous variables not allowed in contexts."
in
- let fn status (id, _, t) =
+ let uctx = Evd.get_universe_context_set !evars in
+ let fn status (id, b, t) =
+ let uctx = Universes.shrink_universe_context uctx (Universes.universes_of_constr t) in
if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
- let decl = (ParameterEntry (None,t,None), IsAssumption Logical) in
+ let uctx = Univ.ContextSet.to_context uctx in
+ let decl = (ParameterEntry (None,false,(t,uctx),None), IsAssumption Logical) in
let cst = Declare.declare_constant ~internal:Declare.KernelSilent id decl in
match class_of_constr t with
- | Some (rels, (tc, args) as _cl) ->
- add_instance (Typeclasses.new_instance tc None false (ConstRef cst));
+ | Some (rels, ((tc,_), args) as _cl) ->
+ add_instance (Typeclasses.new_instance tc None false (*FIXME*)
+ (Flags.use_polymorphic_flag ()) (ConstRef cst));
status
(* declare_subclasses (ConstRef cst) cl *)
| None -> status
@@ -339,9 +354,9 @@ let context l =
| _ -> false
in
let impl = List.exists test impls in
- let decl = (Discharge, Definitional) in
+ let decl = (Discharge, (Flags.use_polymorphic_flag ()), Definitional) in
let nstatus =
- snd (Command.declare_assumption false decl t [] impl
+ snd (Command.declare_assumption false decl (t, uctx) [] impl
Vernacexpr.NoInline (Loc.ghost, id))
in
status && nstatus
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index de62ff369..4dd62ba9f 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -36,13 +36,16 @@ val declare_instance_constant :
Impargs.manual_explicitation list -> (** implicits *)
?hook:(Globnames.global_reference -> unit) ->
Id.t -> (** name *)
- Entries.proof_output -> (** body *)
+ bool -> (* polymorphic *)
+ Univ.universe_context -> (* Universes *)
+ Constr.t -> (** body *)
Term.types -> (** type *)
Names.Id.t
val new_instance :
?abstract:bool -> (** Not abstract by default. *)
?global:bool -> (** Not global by default. *)
+ Decl_kinds.polymorphic ->
local_binder list ->
typeclass_constraint ->
constr_expr option ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f41acaba2..d2111f0fb 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -56,8 +56,8 @@ let rec complete_conclusion a cs = function
user_err_loc (loc,"",
strbrk"Cannot infer the non constant arguments of the conclusion of "
++ pr_id cs ++ str ".");
- let args = List.map (fun id -> CRef(Ident(loc,id))) params in
- CAppExpl (loc,(None,Ident(loc,name)),List.rev args)
+ let args = List.map (fun id -> CRef(Ident(loc,id),None)) params in
+ CAppExpl (loc,(None,Ident(loc,name),None),List.rev args)
| c -> c
(* Commands of the interface *)
@@ -74,29 +74,34 @@ let red_constant_entry n ce = function
under_binders env
(fst (reduction_of_red_expr env red)) n body,eff) }
-let interp_definition bl red_option c ctypopt =
+let interp_definition bl p red_option c ctypopt =
let env = Global.env() in
- let evdref = ref Evd.empty in
+ let evdref = ref (Evd.from_env env) in
let impls, ((env_bl, ctx), imps1) = interp_context_evars evdref env bl in
let nb_args = List.length ctx in
let imps,ce =
match ctypopt with
None ->
+ let subst = evd_comb0 Evd.nf_univ_variables evdref in
+ let ctx = map_rel_context (Vars.subst_univs_constr subst) ctx in
+ let env_bl = push_rel_context ctx env in
let c, imps2 = interp_constr_evars_impls ~impls evdref env_bl c in
- let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
- imps1@(Impargs.lift_implicits nb_args imps2),
- { const_entry_body = Future.from_val (body,Declareops.no_seff);
- const_entry_secctx = None;
- const_entry_type = None;
- const_entry_opaque = false;
- const_entry_inline_code = false;
- const_entry_feedback = None;
- }
+ let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
+ let body = nf (it_mkLambda_or_LetIn c ctx) in
+ let vars = Universes.universes_of_constr body in
+ let ctx = Universes.restrict_universe_context
+ (Evd.get_universe_context_set !evdref) vars in
+ imps1@(Impargs.lift_implicits nb_args imps2),
+ definition_entry ~univs:(Univ.ContextSet.to_context ctx) ~poly:p body
| Some ctyp ->
let ty, impsty = interp_type_evars_impls ~impls evdref env_bl ctyp in
+ let subst = evd_comb0 Evd.nf_univ_variables evdref in
+ let ctx = map_rel_context (Vars.subst_univs_constr subst) ctx in
+ let env_bl = push_rel_context ctx env in
let c, imps2 = interp_casted_constr_evars_impls ~impls evdref env_bl c ty in
- let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
- let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in
+ let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
+ let body = nf (it_mkLambda_or_LetIn c ctx) in
+ let typ = nf (it_mkProd_or_LetIn ty ctx) in
let beq b1 b2 = if b1 then b2 else not b2 in
let impl_eq (x,y,z) (x',y',z') = beq x x' && beq y y' && beq z z' in
(* Check that all implicit arguments inferable from the term
@@ -108,14 +113,13 @@ let interp_definition bl red_option c ctypopt =
then msg_warning
(strbrk "Implicit arguments declaration relies on type." ++ spc () ++
strbrk "The term declares more implicits than the type here.");
+ let vars = Univ.LSet.union (Universes.universes_of_constr body)
+ (Universes.universes_of_constr typ) in
+ let ctx = Universes.restrict_universe_context
+ (Evd.get_universe_context_set !evdref) vars in
imps1@(Impargs.lift_implicits nb_args impsty),
- { const_entry_body = Future.from_val(body,Declareops.no_seff);
- const_entry_secctx = None;
- const_entry_type = Some typ;
- const_entry_opaque = false;
- const_entry_inline_code = false;
- const_entry_feedback = None;
- }
+ definition_entry ~types:typ ~poly:p
+ ~univs:(Univ.ContextSet.to_context ctx) body
in
red_constant_entry (rel_context_length ctx) ce red_option, !evdref, imps
@@ -144,7 +148,7 @@ let declare_definition_hook = ref ignore
let set_declare_definition_hook = (:=) declare_definition_hook
let get_declare_definition_hook () = !declare_definition_hook
-let declare_definition ident (local,k) ce imps hook =
+let declare_definition ident (local, p, k) ce imps hook =
let () = !declare_definition_hook ce in
let r = match local with
| Discharge when Lib.sections_are_opened () ->
@@ -164,7 +168,7 @@ let declare_definition ident (local,k) ce imps hook =
let _ = Obligations.declare_definition_ref := declare_definition
let do_definition ident k bl red_option c ctypopt hook =
- let (ce, evd, imps as def) = interp_definition bl red_option c ctypopt in
+ let (ce, evd, imps as def) = interp_definition bl (pi2 k) red_option c ctypopt in
if Flags.is_program_mode () then
let env = Global.env () in
let c,sideff = Future.force ce.const_entry_body in
@@ -177,16 +181,17 @@ let do_definition ident k bl red_option c ctypopt hook =
let obls, _, c, cty =
Obligations.eterm_obligations env ident evd 0 c typ
in
- ignore(Obligations.add_definition ident ~term:c cty ~implicits:imps ~kind:k ~hook obls)
+ let ctx = Evd.get_universe_context_set evd in
+ ignore(Obligations.add_definition ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
else let ce = check_definition def in
ignore(declare_definition ident k ce imps
(fun l r -> hook l r;r))
(* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
-let declare_assumption is_coe (local, kind) c imps impl nl (_,ident) = match local with
+let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = match local with
| Discharge when Lib.sections_are_opened () ->
- let decl = (Lib.cwd(), SectionLocalAssum (c,impl), IsAssumption kind) in
+ let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in
let _ = declare_variable ident decl in
let () = assumption_message ident in
let () =
@@ -196,8 +201,9 @@ let declare_assumption is_coe (local, kind) c imps impl nl (_,ident) = match loc
in
let r = VarRef ident in
let () = Typeclasses.declare_instance None true r in
- let () = if is_coe then Class.try_add_new_coercion r ~local:true in
+ let () = if is_coe then Class.try_add_new_coercion r ~local:true false in
(r,true)
+
| Global | Local | Discharge ->
let local = get_locality ident local in
let inl = match nl with
@@ -205,18 +211,25 @@ let declare_assumption is_coe (local, kind) c imps impl nl (_,ident) = match loc
| DefaultInline -> Some (Flags.get_inline_level())
| InlineAt i -> Some i
in
- let decl = (ParameterEntry (None,c,inl), IsAssumption kind) in
+ let ctx = Univ.ContextSet.to_context ctx in
+ let decl = (ParameterEntry (None,p,(c,ctx),inl), IsAssumption kind) in
let kn = declare_constant ident ~local decl in
let gr = ConstRef kn in
let () = maybe_declare_manual_implicits false gr imps in
let () = assumption_message ident in
let () = Typeclasses.declare_instance None false gr in
- let () = if is_coe then Class.try_add_new_coercion gr local in
+ let () = if is_coe then Class.try_add_new_coercion gr local p in
(gr,Lib.is_modtype_strict ())
+let declare_assumptions_hook = ref ignore
+let set_declare_assumptions_hook = (:=) declare_assumptions_hook
+
let interp_assumption evdref env bl c =
let c = prod_constr_expr c bl in
- interp_type_evars_impls evdref env c
+ let ty, impls = interp_type_evars_impls evdref env c in
+ let evd, nf = nf_evars_and_universes !evdref in
+ let ctx = Evd.get_universe_context_set evd in
+ ((nf ty, ctx), impls)
let declare_assumptions idl is_coe k c imps impl_is_on nl =
let refs, status =
@@ -229,16 +242,16 @@ let do_assumptions kind nl l =
let env = Global.env () in
let evdref = ref Evd.empty in
let _,l = List.fold_map (fun env (is_coe,(idl,c)) ->
- let t,imps = interp_assumption evdref env [] c in
+ let (t,ctx),imps = interp_assumption evdref env [] c in
let env =
push_named_context (List.map (fun (_,id) -> (id,None,t)) idl) env in
- (env,((is_coe,idl),t,imps))) env l in
+ (env,((is_coe,idl),t,(ctx,imps)))) env l in
let evd = solve_remaining_evars all_and_fail_flags env Evd.empty !evdref in
let l = List.map (on_pi2 (nf_evar evd)) l in
- snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,imps) ->
+ snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,(ctx,imps)) ->
let t = replace_vars subst t in
- let (refs,status') = declare_assumptions idl is_coe kind t imps false nl in
- let subst' = List.map2 (fun (_,id) c -> (id,constr_of_global c)) idl refs in
+ let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) imps false nl in
+ let subst' = List.map2 (fun (_,id) c -> (id,Universes.constr_of_global c)) idl refs in
(subst'@subst, status' && status)) ([],true) l)
(* 3a| Elimination schemes for mutual inductive definitions *)
@@ -290,6 +303,23 @@ let prepare_param = function
| (na,None,t) -> out_name na, LocalAssum t
| (na,Some b,_) -> out_name na, LocalDef b
+
+let make_conclusion_flexible evdref ty =
+ if isArity ty then
+ let _, concl = destArity ty in
+ match concl with
+ | Type u ->
+ (match Univ.universe_level u with
+ | Some u -> evdref := Evd.make_flexible_variable !evdref true u
+ | None -> ())
+ | _ -> ()
+ else ()
+
+let is_impredicative env u =
+ u = Prop Null ||
+ (engagement env = Some Declarations.ImpredicativeSet && u = Prop Pos)
+
+(** Make the arity conclusion flexible to avoid generating an upper bound universe now. *)
let interp_ind_arity evdref env ind =
interp_type_evars_impls evdref env ind.ind_arity
@@ -301,10 +331,88 @@ let interp_cstrs evdref env impls mldata arity ind =
let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls evdref env ~impls) ctyps') in
(cnames, ctyps'', cimpls)
-let interp_mutual_inductive (paramsl,indl) notations finite =
+let sign_level env evd sign =
+ fst (List.fold_right
+ (fun (_,_,t as d) (lev,env) ->
+ let s = destSort (Reduction.whd_betadeltaiota env
+ (nf_evar evd (Retyping.get_type_of env evd t)))
+ in
+ let u = univ_of_sort s in
+ (Univ.sup u lev, push_rel d env))
+ sign (Univ.type0m_univ,env))
+
+let sup_list = List.fold_left Univ.sup Univ.type0m_univ
+
+let extract_level env evd tys =
+ let sorts = List.map (fun ty ->
+ let ctx, concl = Reduction.dest_prod_assum env ty in
+ sign_level env evd ctx) tys
+ in sup_list sorts
+
+let inductive_levels env evdref arities inds =
+ let destarities = List.map (Reduction.dest_arity env) arities in
+ let levels = List.map (fun (ctx,a) ->
+ if a = Prop Null then None
+ else Some (univ_of_sort a)) destarities
+ in
+ let cstrs_levels, min_levels, sizes =
+ CList.split3
+ (List.map2 (fun (_,tys,_) (ctx,du) ->
+ let len = List.length tys in
+ let clev = extract_level env !evdref tys in
+ let minlev =
+ if len > 1 && not (is_impredicative env du) then
+ Univ.type0_univ
+ else Univ.type0m_univ
+ in
+ (clev, minlev, len)) inds destarities)
+ in
+ (* Take the transitive closure of the system of constructors *)
+ (* level constraints and remove the recursive dependencies *)
+ let levels' = Univ.solve_constraints_system (Array.of_list levels)
+ (Array.of_list cstrs_levels) (Array.of_list min_levels)
+ in
+ let evd =
+ CList.fold_left3 (fun evd cu (ctx,du) len ->
+ if is_impredicative env du then
+ (** Any product is allowed here. *)
+ evd
+ else (** If in a predicative sort, or asked to infer the type,
+ we take the max of:
+ - indices (if in indices-matter mode)
+ - constructors
+ - Type(1) if there is more than 1 constructor
+ *)
+ let evd =
+ (** Indices contribute. *)
+ if Indtypes.is_indices_matter () then (
+ let ilev = sign_level env !evdref ctx in
+ Evd.set_leq_sort evd (Type ilev) du)
+ else evd
+ in
+ (** Constructors contribute. *)
+ let evd =
+ if Sorts.is_set du then
+ if not (Evd.check_leq evd cu Univ.type0_univ) then
+ raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType)
+ else evd
+ else Evd.set_leq_sort evd (Type cu) du
+ in
+ let evd =
+ if len >= 2 && Univ.is_type0m_univ cu then
+ (** "Polymorphic" type constraint and more than one constructor,
+ should not land in Prop. Add constraint only if it would
+ land in Prop directly (no informative arguments as well). *)
+ Evd.set_leq_sort evd (Prop Pos) du
+ else evd
+ in evd)
+ !evdref (Array.to_list levels') destarities sizes
+ in evdref := evd; arities
+
+let interp_mutual_inductive (paramsl,indl) notations poly finite =
check_all_names_different indl;
let env0 = Global.env() in
- let evdref = ref Evd.empty in
+ let evdref = ref Evd.(from_env env0) in
let _, ((env_params, ctx_params), userimpls) =
interp_context_evars evdref env0 paramsl
in
@@ -316,12 +424,14 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
(* Interpret the arities *)
let arities = List.map (interp_ind_arity evdref env_params) indl in
+
let fullarities = List.map (fun (c, _) -> it_mkProd_or_LetIn c ctx_params) arities in
let env_ar = push_types env0 indnames fullarities in
let env_ar_params = push_rel_context ctx_params env_ar in
(* Compute interpretation metadatas *)
- let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (rel_context_nhyps ctx_params) impls) arities in
+ let indimpls = List.map (fun (_, impls) -> userimpls @
+ lift_implicits (rel_context_nhyps ctx_params) impls) arities in
let arities = List.map fst arities in
let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in
let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
@@ -336,9 +446,24 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
(* Try further to solve evars, and instantiate them *)
let sigma = solve_remaining_evars all_and_fail_flags env_params Evd.empty !evdref in
- let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
- let ctx_params = Context.map_rel_context (nf_evar sigma) ctx_params in
- let arities = List.map (nf_evar sigma) arities in
+ evdref := sigma;
+ (* Compute renewed arities *)
+ let nf,_ = e_nf_evars_and_universes evdref in
+ let arities = List.map nf arities in
+ let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
+ let _ = List.iter (fun ty -> make_conclusion_flexible evdref ty) arities in
+ let arities = inductive_levels env_ar_params evdref arities constructors in
+ let nf',_ = e_nf_evars_and_universes evdref in
+ let nf x = nf' (nf x) in
+ let arities = List.map nf' arities in
+ let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
+ let ctx_params = map_rel_context nf ctx_params in
+ let evd = !evdref in
+ List.iter (check_evars env_params Evd.empty evd) arities;
+ iter_rel_context (check_evars env0 Evd.empty evd) ctx_params;
+ List.iter (fun (_,ctyps,_) ->
+ List.iter (check_evars env_ar_params Evd.empty evd) ctyps)
+ constructors;
(* Build the inductive entries *)
let entries = List.map3 (fun ind arity (cnames,ctypes,cimpls) -> {
@@ -357,7 +482,9 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
{ mind_entry_params = List.map prepare_param ctx_params;
mind_entry_record = false;
mind_entry_finite = finite;
- mind_entry_inds = entries },
+ mind_entry_inds = entries;
+ mind_entry_polymorphic = poly;
+ mind_entry_universes = Evd.universe_context evd },
impls
(* Very syntactical equality *)
@@ -412,16 +539,19 @@ type one_inductive_impls =
Impargs.manual_explicitation list (* for inds *)*
Impargs.manual_explicitation list list (* for constrs *)
-let do_mutual_inductive indl finite =
+type one_inductive_expr =
+ lident * local_binder list * constr_expr option * constructor_expr list
+
+let do_mutual_inductive indl poly finite =
let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in
(* Interpret the types *)
- let mie,impls = interp_mutual_inductive indl ntns finite in
+ let mie,impls = interp_mutual_inductive indl ntns poly finite in
(* Declare the mutual inductive block with its associated schemes *)
ignore (declare_mutual_inductive_with_eliminations UserVerbose mie impls);
(* Declare the possible notations of inductive types *)
List.iter Metasyntax.add_notation_interpretation ntns;
(* Declare the coercions *)
- List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false) coes
+ List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes
(* 3c| Fixpoints and co-fixpoints *)
@@ -525,11 +655,14 @@ let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
-let declare_fix kind f def t imps =
+let declare_fix (_,poly,_ as kind) ctx f def t imps =
let ce = {
const_entry_body = Future.from_val def;
const_entry_secctx = None;
const_entry_type = Some t;
+ const_entry_polymorphic = poly;
+ const_entry_universes = ctx;
+ const_entry_proj = None;
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None;
@@ -576,7 +709,7 @@ let fix_sub_ref = make_ref fixsub_module "Fix_sub"
let measure_on_R_ref = make_ref fixsub_module "MR"
let well_founded = init_constant ["Init"; "Wf"] "well_founded"
let mkSubset name typ prop =
- mkApp ((delayed_force build_sigma).typ,
+ mkApp (Universes.constr_of_global (delayed_force build_sigma).typ,
[| typ; mkLambda (name, typ, prop) |])
let sigT = Lazy.lazy_from_fun build_sigma_type
@@ -591,15 +724,19 @@ let rec telescope = function
List.fold_left
(fun (ty, tys, (k, constr)) (n, b, t) ->
let pred = mkLambda (n, t, ty) in
- let sigty = mkApp ((Lazy.force sigT).typ, [|t; pred|]) in
- let intro = mkApp ((Lazy.force sigT).intro, [|lift k t; lift k pred; mkRel k; constr|]) in
+ let ty = Universes.constr_of_global (Lazy.force sigT).typ in
+ let intro = Universes.constr_of_global (Lazy.force sigT).intro in
+ let sigty = mkApp (ty, [|t; pred|]) in
+ let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in
(sigty, pred :: tys, (succ k, intro)))
(t, [], (2, mkRel 1)) tl
in
let (last, subst) = List.fold_right2
(fun pred (n, b, t) (prev, subst) ->
- let proj1 = applistc (Lazy.force sigT).proj1 [t; pred; prev] in
- let proj2 = applistc (Lazy.force sigT).proj2 [t; pred; prev] in
+ let p1 = Universes.constr_of_global (Lazy.force sigT).proj1 in
+ let p2 = Universes.constr_of_global (Lazy.force sigT).proj2 in
+ let proj1 = applistc p1 [t; pred; prev] in
+ let proj2 = applistc p2 [t; pred; prev] in
(lift 1 proj2, (n, Some proj1, t) :: subst))
(List.rev tys) tl (mkRel 1, [])
in ty, ((n, Some last, t) :: subst), constr
@@ -648,7 +785,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
it_mkLambda_or_LetIn measure letbinders,
it_mkLambda_or_LetIn measure binders
in
- let comb = constr_of_global (delayed_force measure_on_R_ref) in
+ let comb = Universes.constr_of_global (delayed_force measure_on_R_ref) in
let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
let wf_rel_fun x y =
mkApp (rel, [| subst1 x measure_body;
@@ -663,7 +800,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
in
let intern_bl = wfarg 1 :: [arg] in
let _intern_env = push_rel_context intern_bl env in
- let proj = (delayed_force build_sigma).Coqlib.proj1 in
+ let proj = (*FIXME*)Universes.constr_of_global (delayed_force build_sigma).Coqlib.proj1 in
let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
let projection = (* in wfarg :: arg :: before *)
mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
@@ -676,7 +813,8 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
let intern_fun_binder = (Name (add_suffix recname "'"), None, intern_fun_arity_prod) in
let curry_fun =
let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
- let arg = mkApp ((delayed_force build_sigma).intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
+ let intro = (*FIXME*)Universes.constr_of_global (delayed_force build_sigma).Coqlib.intro in
+ let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
let rcurry = mkApp (rel, [| measure; lift len measure |]) in
let lam = (Name (Id.of_string "recproof"), None, rcurry) in
@@ -701,7 +839,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
let prop = mkLambda (Name argname, argtyp, top_arity_let) in
let def =
- mkApp (constr_of_global (delayed_force fix_sub_ref),
+ mkApp (Universes.constr_of_global (delayed_force fix_sub_ref),
[| argtyp ; wf_rel ;
Evarutil.e_new_evar evdref env
~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
@@ -715,16 +853,20 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
if List.length binders_rel > 1 then
let name = add_suffix recname "_func" in
let hook l gr =
- let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in
+ let body = it_mkLambda_or_LetIn (mkApp (Universes.constr_of_global gr, [|make|])) binders_rel in
let ty = it_mkProd_or_LetIn top_arity binders_rel in
let ce =
{ const_entry_body = Future.from_val (Evarutil.nf_evar !evdref body,Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = Some ty;
- const_entry_opaque = false;
- const_entry_inline_code = false;
+ (* FIXME *)
+ const_entry_proj = None;
+ const_entry_polymorphic = false;
+ const_entry_universes = Evd.universe_context !evdref;
const_entry_feedback = None;
- } in
+ const_entry_opaque = false;
+ const_entry_inline_code = false}
+ in
(** FIXME: include locality *)
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
let gr = ConstRef c in
@@ -746,9 +888,9 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
let evars, _, evars_def, evars_typ =
Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp
in
- ignore(Obligations.add_definition
- recname ~term:evars_def evars_typ evars ~hook)
-
+ let ctx = Evd.get_universe_context_set !evdref in
+ ignore(Obligations.add_definition recname ~term:evars_def
+ evars_typ ctx evars ~hook)
let interp_recursive isfix fixl notations =
let env = Global.env() in
@@ -794,8 +936,9 @@ let interp_recursive isfix fixl notations =
(* Instantiate evars and check all are resolved *)
let evd = consider_remaining_unif_problems env_rec !evdref in
- let fixdefs = List.map (Option.map (nf_evar evd)) fixdefs in
- let fixtypes = List.map (nf_evar evd) fixtypes in
+ let evd, nf = nf_evars_and_universes evd in
+ let fixdefs = List.map (Option.map nf) fixdefs in
+ let fixtypes = List.map nf fixtypes in
let fixctxnames = List.map (fun (_,ctx) -> List.map pi1 ctx) fixctxs in
(* Build the fix declaration block *)
@@ -811,25 +954,25 @@ let check_recursive isfix env evd (fixnames,fixdefs,_) =
let interp_fixpoint l ntns =
let (env,_,evd),fix,info = interp_recursive true l ntns in
check_recursive true env evd fix;
- fix,info
+ (fix,Evd.get_universe_context_set evd,info)
let interp_cofixpoint l ntns =
let (env,_,evd),fix,info = interp_recursive false l ntns in
check_recursive false env evd fix;
- fix,info
+ fix,Evd.get_universe_context_set evd,info
-let declare_fixpoint local ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
+let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexes ntns =
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
let thms =
- List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
+ List.map3 (fun id t (len,imps,_) -> (id,((t,ctx),(len,imps)))) fixnames fixtypes fiximps in
let init_tac =
Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
fixdefs) in
let init_tac =
Option.map (List.map Proofview.V82.tactic) init_tac
in
- Lemmas.start_proof_with_initialization (Global,DefinitionBody Fixpoint)
+ Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint)
(Some(false,indexes,init_tac)) thms None (fun _ _ -> ())
else begin
(* We shortcut the proof process *)
@@ -841,25 +984,27 @@ let declare_fixpoint local ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
let fixdecls =
List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
let fixdecls = List.map (fun c -> c, Declareops.no_seff) fixdecls in
- ignore (List.map4 (declare_fix (local, Fixpoint)) fixnames fixdecls fixtypes fiximps);
+ let ctx = Univ.ContextSet.to_context ctx in
+ ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx)
+ fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
fixpoint_message (Some indexes) fixnames;
end;
(* Declare notations *)
List.iter Metasyntax.add_notation_interpretation ntns
-let declare_cofixpoint local ((fixnames,fixdefs,fixtypes),fiximps) ntns =
+let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns =
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
let thms =
- List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
+ List.map3 (fun id t (len,imps,_) -> (id,((t,ctx),(len,imps)))) fixnames fixtypes fiximps in
let init_tac =
Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
fixdefs) in
let init_tac =
Option.map (List.map Proofview.V82.tactic) init_tac
in
- Lemmas.start_proof_with_initialization (Global,DefinitionBody CoFixpoint)
+ Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
(Some(true,[],init_tac)) thms None (fun _ _ -> ())
else begin
(* We shortcut the proof process *)
@@ -868,7 +1013,9 @@ let declare_cofixpoint local ((fixnames,fixdefs,fixtypes),fiximps) ntns =
let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
let fixdecls = List.map (fun c-> c,Declareops.no_seff) fixdecls in
let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
- ignore (List.map4 (declare_fix (local, CoFixpoint)) fixnames fixdecls fixtypes fiximps);
+ let ctx = Univ.ContextSet.to_context ctx in
+ ignore (List.map4 (declare_fix (local, poly, CoFixpoint) ctx)
+ fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
cofixpoint_message fixnames
end;
@@ -898,7 +1045,12 @@ let out_def = function
| Some def -> def
| None -> error "Program Fixpoint needs defined bodies."
-let do_program_recursive local fixkind fixl ntns =
+let collect_evars_of_term evd c ty =
+ let evars = Evar.Set.union (evars_of_term c) (evars_of_term ty) in
+ Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
+ evars Evd.empty
+
+let do_program_recursive local p fixkind fixl ntns =
let isfix = fixkind != Obligations.IsCoFixpoint in
let (env, rec_sign, evd), fix, info =
interp_recursive isfix fixl ntns
@@ -934,13 +1086,14 @@ let do_program_recursive local fixkind fixl ntns =
Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in
List.iteri (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl
end in
+ let ctx = Evd.get_universe_context_set evd in
let kind = match fixkind with
- | Obligations.IsFixpoint _ -> (local, Fixpoint)
- | Obligations.IsCoFixpoint -> (local, CoFixpoint)
+ | Obligations.IsFixpoint _ -> (local, p, Fixpoint)
+ | Obligations.IsCoFixpoint -> (local, p, CoFixpoint)
in
- Obligations.add_mutual_definitions defs ~kind ntns fixkind
+ Obligations.add_mutual_definitions defs ~kind ctx ntns fixkind
-let do_program_fixpoint local l =
+let do_program_fixpoint local poly l =
let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
match g, l with
| [(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
@@ -954,30 +1107,30 @@ let do_program_fixpoint local l =
| [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] ->
build_wellfounded (id, n, bl, typ, out_def def)
- (Option.default (CRef lt_ref) r) m ntn
+ (Option.default (CRef (lt_ref,None)) r) m ntn
| _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g ->
let fixl,ntns = extract_fixpoint_components true l in
let fixkind = Obligations.IsFixpoint g in
- do_program_recursive local fixkind fixl ntns
+ do_program_recursive local poly fixkind fixl ntns
| _, _ ->
errorlabstrm "do_program_fixpoint"
(str "Well-founded fixpoints not allowed in mutually recursive blocks")
-let do_fixpoint local l =
- if Flags.is_program_mode () then do_program_fixpoint local l
+let do_fixpoint local poly l =
+ if Flags.is_program_mode () then do_program_fixpoint local poly l
else
let fixl, ntns = extract_fixpoint_components true l in
let fix = interp_fixpoint fixl ntns in
let possible_indexes =
- List.map compute_possible_guardness_evidences (snd fix) in
- declare_fixpoint local fix possible_indexes ntns
+ List.map compute_possible_guardness_evidences (pi3 fix) in
+ declare_fixpoint local poly fix possible_indexes ntns
-let do_cofixpoint local l =
+let do_cofixpoint local poly l =
let fixl,ntns = extract_cofixpoint_components l in
if Flags.is_program_mode () then
- do_program_recursive local Obligations.IsCoFixpoint fixl ntns
+ do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns
else
let cofix = interp_cofixpoint fixl ntns in
- declare_cofixpoint local cofix ntns
+ declare_cofixpoint local poly cofix ntns
diff --git a/toplevel/command.mli b/toplevel/command.mli
index d2ebdc561..b2ba23ef2 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -29,7 +29,7 @@ val get_declare_definition_hook : unit -> (definition_entry -> unit)
(** {6 Definitions/Let} *)
val interp_definition :
- local_binder list -> red_expr option -> constr_expr ->
+ local_binder list -> polymorphic -> red_expr option -> constr_expr ->
constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits
val declare_definition : Id.t -> definition_kind ->
@@ -42,16 +42,25 @@ val do_definition : Id.t -> definition_kind ->
(** {6 Parameters/Assumptions} *)
+(* val interp_assumption : env -> evar_map ref -> *)
+(* local_binder list -> constr_expr -> *)
+(* types Univ.in_universe_context_set * Impargs.manual_implicits *)
+
(** returns [false] if the assumption is neither local to a section,
nor in a module type and meant to be instantiated. *)
-val declare_assumption : coercion_flag -> assumption_kind -> types ->
+val declare_assumption : coercion_flag -> assumption_kind ->
+ types Univ.in_universe_context_set ->
Impargs.manual_implicits ->
bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located ->
global_reference * bool
-val do_assumptions : locality * assumption_object_kind ->
+val do_assumptions : locality * polymorphic * assumption_object_kind ->
Vernacexpr.inline -> simple_binder with_coercion list -> bool
+(* val declare_assumptions : variable Loc.located list -> *)
+(* coercion_flag -> assumption_kind -> types Univ.in_universe_context_set -> *)
+(* Impargs.manual_implicits -> bool -> Vernacexpr.inline -> bool *)
+
(** {6 Inductive and coinductive types} *)
(** Extracting the semantical components out of the raw syntax of mutual
@@ -77,7 +86,7 @@ type one_inductive_impls =
Impargs.manual_implicits list (** for constrs *)
val interp_mutual_inductive :
- structured_inductive_expr -> decl_notation list -> bool ->
+ structured_inductive_expr -> decl_notation list -> polymorphic -> bool(*finite*) ->
mutual_inductive_entry * one_inductive_impls list
(** Registering a mutual inductive definition together with its
@@ -90,7 +99,7 @@ val declare_mutual_inductive_with_eliminations :
(** Entry points for the vernacular commands Inductive and CoInductive *)
val do_mutual_inductive :
- (one_inductive_expr * decl_notation list) list -> bool -> unit
+ (one_inductive_expr * decl_notation list) list -> polymorphic -> bool -> unit
(** {6 Fixpoints and cofixpoints} *)
@@ -120,33 +129,38 @@ type recursive_preentry =
val interp_fixpoint :
structured_fixpoint_expr list -> decl_notation list ->
- recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list
+ recursive_preentry * Univ.universe_context_set *
+ (Name.t list * Impargs.manual_implicits * int option) list
val interp_cofixpoint :
structured_fixpoint_expr list -> decl_notation list ->
- recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list
+ recursive_preentry * Univ.universe_context_set *
+ (Name.t list * Impargs.manual_implicits * int option) list
(** Registering fixpoints and cofixpoints in the environment *)
val declare_fixpoint :
- locality -> recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list ->
+ locality -> polymorphic ->
+ recursive_preentry * Univ.universe_context_set *
+ (Name.t list * Impargs.manual_implicits * int option) list ->
lemma_possible_guards -> decl_notation list -> unit
-val declare_cofixpoint :
- locality -> recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list ->
- decl_notation list -> unit
+val declare_cofixpoint : locality -> polymorphic ->
+ recursive_preentry * Univ.universe_context_set *
+ (Name.t list * Impargs.manual_implicits * int option) list ->
+ decl_notation list -> unit
(** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
val do_fixpoint :
- locality -> (fixpoint_expr * decl_notation list) list -> unit
+ locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
val do_cofixpoint :
- locality -> (cofixpoint_expr * decl_notation list) list -> unit
+ locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
(** Utils *)
val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
-val declare_fix : definition_kind -> Id.t ->
+val declare_fix : definition_kind -> Univ.universe_context -> Id.t ->
Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 51dc8d5bb..d772171e5 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -382,6 +382,7 @@ let parse_args arglist =
Serialize.document Xml_printer.to_string_fmt; exit 0
|"-ideslave" -> Flags.ide_slave := true
|"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet
+ |"-indices-matter" -> Indtypes.enforce_indices_matter ()
|"-just-parsing" -> Vernac.just_parsing := true
|"-lazy-load-proofs" -> Flags.load_proofs := Flags.Lazy
|"-m"|"--memory" -> memory_stat := true
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index b9ffbaea5..55475a378 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -69,14 +69,9 @@ let abstract_inductive hyps nparams inds =
in (params',ind'')
let refresh_polymorphic_type_of_inductive (_,mip) =
- match mip.mind_arity with
- | Monomorphic s ->
- s.mind_user_arity
- | Polymorphic ar ->
- let ctx = List.rev mip.mind_arity_ctxt in
- mkArity (List.rev ctx,Termops.new_Type_sort())
+ mip.mind_arity.mind_user_arity
-let process_inductive sechyps modlist mib =
+let process_inductive (sechyps,abs_ctx) modlist mib =
let nparams = mib.mind_nparams in
let inds =
Array.map_to_list
@@ -90,7 +85,11 @@ let process_inductive sechyps modlist mib =
mib.mind_packets in
let sechyps' = map_named_context (expmod_constr modlist) sechyps in
let (params',inds') = abstract_inductive sechyps' nparams inds in
- { mind_entry_record = mib.mind_record;
+ let univs = Univ.UContext.union abs_ctx mib.mind_universes in
+ { mind_entry_record = mib.mind_record <> None;
mind_entry_finite = mib.mind_finite;
mind_entry_params = params';
- mind_entry_inds = inds' }
+ mind_entry_inds = inds';
+ mind_entry_polymorphic = mib.mind_polymorphic;
+ mind_entry_universes = univs
+ }
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index 6cef31c8a..c074a1cc8 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -12,4 +12,4 @@ open Entries
open Opaqueproof
val process_inductive :
- named_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
+ named_context Univ.in_universe_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index fd74f9c06..9d6e9756d 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -65,7 +65,7 @@ let contract3' env a b c = function
contract3 env a b c, ConversionFailed (env',t1,t2)
| NotSameArgSize | NotSameHead | NoCanonicalStructure
| MetaOccurInBody _ | InstanceNotSameType _
- | UnifUnivInconsistency as x -> contract3 env a b c, x
+ | UnifUnivInconsistency _ as x -> contract3 env a b c, x
(** Printers *)
@@ -143,9 +143,15 @@ let rec pr_disjunction pr = function
| a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l
| [] -> assert false
+let pr_puniverses f env (c,u) =
+ f env c ++
+ (if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then
+ str"(*" ++ Univ.Instance.pr u ++ str"*)"
+ else mt())
+
let explain_elim_arity env ind sorts c pj okinds =
let env = make_all_name_different env in
- let pi = pr_inductive env ind in
+ let pi = pr_inductive env (fst ind) in
let pc = pr_lconstr_env env c in
let msg = match okinds with
| Some(kp,ki,explanation) ->
@@ -200,14 +206,14 @@ let explain_number_branches env sigma cj expn =
str "expects " ++ int expn ++ str " branches."
let explain_ill_formed_branch env sigma c ci actty expty =
- let simp t = Reduction.nf_betaiota (Evarutil.nf_evar sigma t) in
+ let simp t = Reduction.nf_betaiota env (Evarutil.nf_evar sigma t) in
let c = Evarutil.nf_evar sigma c in
let env = make_all_name_different env in
let pc = pr_lconstr_env env c in
let pa, pe = pr_explicit env (simp actty) (simp expty) in
strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++
spc () ++ strbrk "the branch for constructor" ++ spc () ++
- quote (pr_constructor env ci) ++
+ quote (pr_puniverses pr_constructor env ci) ++
spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++
str "which should be" ++ brk(1,1) ++ pe ++ str "."
@@ -260,8 +266,12 @@ let explain_unification_error env sigma p1 p2 = function
quote (pr_existential_key evk) ++ str ":" ++ spc () ++
str "cannot unify" ++ t ++ spc () ++ str "and" ++ spc () ++
u ++ str ")"
- | UnifUnivInconsistency ->
- spc () ++ str "(Universe inconsistency)"
+ | UnifUnivInconsistency p ->
+ if !Constrextern.print_universes then
+ spc () ++ str "(Universe inconsistency: " ++
+ Univ.explain_universe_inconsistency p ++ str")"
+ else
+ spc () ++ str "(Universe inconsistency)"
let explain_actual_type env sigma j t reason =
let env = make_all_name_different env in
@@ -513,7 +523,7 @@ let explain_var_not_found env id =
spc () ++ str "was not found" ++
spc () ++ str "in the current" ++ spc () ++ str "environment" ++ str "."
-let explain_wrong_case_info env ind ci =
+let explain_wrong_case_info env (ind,u) ci =
let pi = pr_inductive (Global.env()) ind in
if eq_ind ci.ci_ind ind then
str "Pattern-matching expression on an object of inductive type" ++
@@ -584,6 +594,10 @@ let explain_non_linear_unification env m t =
strbrk " which would require to abstract twice on " ++
pr_lconstr_env env t ++ str "."
+let explain_unsatisfied_constraints env cst =
+ strbrk "Unsatisfied constraints: " ++ Univ.pr_constraints cst ++
+ spc () ++ str "(maybe a bugged tactic)."
+
let explain_type_error env sigma err =
let env = make_all_name_different env in
match err with
@@ -619,6 +633,8 @@ let explain_type_error env sigma err =
explain_ill_typed_rec_body env sigma i lna vdefj vargs
| WrongCaseInfo (ind,ci) ->
explain_wrong_case_info env ind ci
+ | UnsatisfiedConstraints cst ->
+ explain_unsatisfied_constraints env cst
let explain_pretype_error env sigma err =
let env = Evarutil.env_nf_betaiotaevar sigma env in
@@ -998,7 +1014,7 @@ let error_not_allowed_case_analysis isrec kind i =
str (if isrec then "Induction" else "Case analysis") ++
strbrk " on sort " ++ pr_sort kind ++
strbrk " is not allowed for inductive definition " ++
- pr_inductive (Global.env()) i ++ str "."
+ pr_inductive (Global.env()) (fst i) ++ str "."
let error_not_mutual_in_scheme ind ind' =
if eq_ind ind ind' then
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index f5ee027f1..2a408e03d 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -27,13 +27,18 @@ open Decl_kinds
(**********************************************************************)
(* Registering schemes in the environment *)
-type mutual_scheme_object_function = mutual_inductive -> constr array * Declareops.side_effects
-type individual_scheme_object_function = inductive -> constr * Declareops.side_effects
+
+type mutual_scheme_object_function =
+ mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
+type individual_scheme_object_function =
+ inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
type 'a scheme_kind = string
let scheme_map = Summary.ref Indmap.empty ~name:"Schemes"
+let pr_scheme_kind = Pp.str
+
let cache_one_scheme kind (ind,const) =
let map = try Indmap.find ind !scheme_map with Not_found -> String.Map.empty in
scheme_map := Indmap.add ind (String.Map.add kind const map) !scheme_map
@@ -41,9 +46,9 @@ let cache_one_scheme kind (ind,const) =
let cache_scheme (_,(kind,l)) =
Array.iter (cache_one_scheme kind) l
-let subst_one_scheme subst ((mind,i),const) =
+let subst_one_scheme subst (ind,const) =
(* Remark: const is a def: the result of substitution is a constant *)
- ((subst_ind subst mind,i),fst (subst_con subst const))
+ (subst_ind subst ind,subst_constant subst const)
let subst_scheme (subst,(kind,l)) =
(kind,Array.map (subst_one_scheme subst) l)
@@ -67,8 +72,8 @@ type individual
type mutual
type scheme_object_function =
- | MutualSchemeFunction of (mutual_inductive -> constr array * Declareops.side_effects)
- | IndividualSchemeFunction of (inductive -> constr * Declareops.side_effects)
+ | MutualSchemeFunction of mutual_scheme_object_function
+ | IndividualSchemeFunction of individual_scheme_object_function
let scheme_object_table =
(Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t)
@@ -111,31 +116,37 @@ let compute_name internal id =
| KernelSilent ->
Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
-let define internal id c =
+let define internal id c p univs =
let fd = declare_constant ~internal in
let id = compute_name internal id in
+ let ctx = Evd.normalize_evar_universe_context univs in
+ let c = Vars.subst_univs_fn_constr
+ (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in
let entry = {
const_entry_body = Future.from_val (c,Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = None;
+ const_entry_proj = None;
+ const_entry_polymorphic = p;
+ const_entry_universes = Evd.evar_context_universe_context ctx;
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None;
} in
let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
let () = match internal with
- | KernelSilent -> ()
- | _-> definition_message id
+ | KernelSilent -> ()
+ | _-> definition_message id
in
kn
let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) =
- let c, eff = f ind in
+ let (c, ctx), eff = f ind in
let mib = Global.lookup_mind mind in
let id = match idopt with
| Some id -> id
| None -> add_suffix mib.mind_packets.(i).mind_typename suff in
- let const = define internal id c in
+ let const = define internal id c mib.mind_polymorphic ctx in
declare_scheme kind [|ind,const|];
const, Declareops.cons_side_effects
(Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff
@@ -147,12 +158,14 @@ let define_individual_scheme kind internal names (mind,i as ind) =
define_individual_scheme_base kind s f internal names ind
let define_mutual_scheme_base kind suff f internal names mind =
- let cl, eff = f mind in
+ let (cl, ctx), eff = f mind in
let mib = Global.lookup_mind mind in
let ids = Array.init (Array.length mib.mind_packets) (fun i ->
try Int.List.assoc i names
with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
- let consts = Array.map2 (define internal) ids cl in
+
+ let consts = Array.map2 (fun id cl ->
+ define internal id cl mib.mind_polymorphic ctx) ids cl in
let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
declare_scheme kind schemes;
consts,
@@ -185,4 +198,3 @@ let find_scheme kind (mind,i as ind) =
let check_scheme kind ind =
try let _ = find_scheme_on_env_too kind ind in true
with Not_found -> false
-
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index d57f1556d..7f84843a9 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -19,9 +19,9 @@ type individual
type 'a scheme_kind
type mutual_scheme_object_function =
- mutual_inductive -> constr array * Declareops.side_effects
+ mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
type individual_scheme_object_function =
- inductive -> constr * Declareops.side_effects
+ inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
(** Main functions to register a scheme builder *)
@@ -49,3 +49,6 @@ val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** inter
val find_scheme : 'a scheme_kind -> inductive -> constant * Declareops.side_effects
val check_scheme : 'a scheme_kind -> inductive -> bool
+
+
+val pr_scheme_kind : 'a scheme_kind -> Pp.std_ppcmds
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 2cc98feea..c139f1910 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -113,13 +113,16 @@ let _ =
(* Util *)
-let define id internal c t =
+let define id internal ctx c t =
let f = declare_constant ~internal in
let kn = f id
(DefinitionEntry
{ const_entry_body = c;
const_entry_secctx = None;
const_entry_type = t;
+ const_entry_proj = None;
+ const_entry_polymorphic = true;
+ const_entry_universes = Evd.universe_context ctx; (* FIXME *)
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None;
@@ -292,6 +295,7 @@ let declare_sym_scheme ind =
(* Scheme command *)
+let smart_global_inductive y = smart_global_inductive y
let rec split_scheme l =
let env = Global.env() in
match l with
@@ -311,7 +315,7 @@ requested
let names inds recs isdep y z =
let ind = smart_global_inductive y in
let sort_of_ind = inductive_sort_family (snd (lookup_mind_specif env ind)) in
- let z' = family_of_sort (interp_sort z) in
+ let z' = interp_elimination_sort z in
let suffix = (
match sort_of_ind with
| InProp ->
@@ -345,19 +349,20 @@ requested
let do_mutual_induction_scheme lnamedepindsort =
let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort
- and sigma = Evd.empty
and env0 = Global.env() in
- let lrecspec =
- List.map
- (fun (_,dep,ind,sort) -> (ind,dep,interp_elimination_sort sort))
- lnamedepindsort
+ let sigma, lrecspec =
+ List.fold_left
+ (fun (evd, l) (_,dep,ind,sort) ->
+ let evd, indu = Evd.fresh_inductive_instance env0 evd ind in
+ (evd, (indu,dep,interp_elimination_sort sort) :: l))
+ (Evd.from_env env0,[]) lnamedepindsort
in
- let listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in
+ let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in
let declare decl fi lrecref =
- let decltype = Retyping.get_type_of env0 Evd.empty decl in
- let decltype = refresh_universes decltype in
+ let decltype = Retyping.get_type_of env0 sigma decl in
+ (* let decltype = refresh_universes decltype in *)
let proof_output = Future.from_val (decl,Declareops.no_seff) in
- let cst = define fi UserVerbose proof_output (Some decltype) in
+ let cst = define fi UserVerbose sigma proof_output (Some decltype) in
ConstRef cst :: lrecref
in
let _ = List.fold_right2 declare listdecl lrecnames [] in
@@ -407,7 +412,9 @@ let fold_left' f = function
| hd :: tl -> List.fold_left f hd tl
let build_combined_scheme env schemes =
- let defs = List.map (fun cst -> (cst, Typeops.type_of_constant env cst)) schemes in
+ let defs = List.map (fun cst -> (* FIXME *)
+ let evd, c = Evd.fresh_constant_instance env Evd.empty cst in
+ (c, Typeops.type_of_constant_in env c)) schemes in
(* let nschemes = List.length schemes in *)
let find_inductive ty =
let (ctx, arity) = decompose_prod ty in
@@ -415,7 +422,7 @@ let build_combined_scheme env schemes =
match kind_of_term last with
| App (ind, args) ->
let ind = destInd ind in
- let (_,spec) = Inductive.lookup_mind_specif env ind in
+ let (_,spec) = Inductive.lookup_mind_specif env (fst ind) in
ctx, ind, spec.mind_nrealargs
| _ -> ctx, destInd last, 0
in
@@ -426,8 +433,8 @@ let build_combined_scheme env schemes =
let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in
let relargs = rel_vect 0 prods in
let concls = List.rev_map
- (fun (cst, t) ->
- mkApp(mkConst cst, relargs),
+ (fun (cst, t) -> (* FIXME *)
+ mkApp(mkConstU cst, relargs),
snd (decompose_prod_n prods t)) defs in
let concl_bod, concl_typ =
fold_left'
@@ -451,10 +458,9 @@ let do_combined_scheme name schemes =
with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared."))
schemes
in
- let env = Global.env () in
- let body,typ = build_combined_scheme env csts in
+ let body,typ = build_combined_scheme (Global.env ()) csts in
let proof_output = Future.from_val (body,Declareops.no_seff) in
- ignore (define (snd name) UserVerbose proof_output (Some typ));
+ ignore (define (snd name) UserVerbose Evd.empty proof_output (Some typ));
fixpoint_message None [snd name]
(**********************************************************************)
@@ -464,7 +470,7 @@ let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done
let declare_default_schemes kn =
let mib = Global.lookup_mind kn in
let n = Array.length mib.mind_packets in
- if !elim_flag && (not mib.mind_record || !record_elim_flag) then
+ if !elim_flag && (mib.mind_record = None || !record_elim_flag) then
declare_induction_schemes kn;
if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n;
if is_eq_flag() then try_declare_beq_scheme kn;
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 761f9c214..3b86cf72f 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1269,7 +1269,7 @@ let add_notation local c ((loc,df),modifiers) sc =
(* Infix notations *)
-let inject_var x = CRef (Ident (Loc.ghost, Id.of_string x))
+let inject_var x = CRef (Ident (Loc.ghost, Id.of_string x),None)
let add_infix local ((loc,inf),modifiers) pr sc =
check_infix_modifiers modifiers;
@@ -1323,7 +1323,7 @@ let add_class_scope scope cl =
(* Check if abbreviation to a name and avoid early insertion of
maximal implicit arguments *)
let try_interp_name_alias = function
- | [], CRef ref -> intern_reference ref
+ | [], CRef (ref,_) -> intern_reference ref
| _ -> raise Not_found
let add_syntactic_definition ident (vars,c) local onlyparse =
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index d772af3c1..d937c400a 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -21,7 +21,7 @@ open Pp
open Errors
open Util
-let declare_fix_ref = ref (fun _ _ _ _ _ -> assert false)
+let declare_fix_ref = ref (fun _ _ _ _ _ _ -> assert false)
let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
let trace s =
@@ -298,11 +298,15 @@ type obligation_info =
(Names.Id.t * Term.types * Evar_kinds.t Loc.located *
Evar_kinds.obligation_definition_status * Int.Set.t * unit Proofview.tactic option) array
+type 'a obligation_body =
+ | DefinedObl of 'a
+ | TermObl of constr
+
type obligation =
{ obl_name : Id.t;
obl_type : types;
obl_location : Evar_kinds.t Loc.located;
- obl_body : constr option;
+ obl_body : constant obligation_body option;
obl_status : Evar_kinds.obligation_definition_status;
obl_deps : Int.Set.t;
obl_tac : unit Proofview.tactic option;
@@ -320,6 +324,8 @@ type program_info = {
prg_name: Id.t;
prg_body: constr;
prg_type: constr;
+ prg_ctx: Univ.universe_context_set;
+ prg_subst : Universes.universe_opt_subst;
prg_obligations: obligations;
prg_deps : Id.t list;
prg_fixkind : fixpoint_kind option ;
@@ -383,27 +389,43 @@ let _ =
let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
-let get_obligation_body expand obl =
- let c = Option.get obl.obl_body in
+let get_body subst obl =
+ match obl.obl_body with
+ | None -> assert false
+ | Some (DefinedObl c) ->
+ let _, ctx = Environ.constant_type_in_ctx (Global.env ()) c in
+ let pc = subst_univs_fn_puniverses (Univ.level_subst_of subst) (c, Univ.UContext.instance ctx) in
+ DefinedObl pc
+ | Some (TermObl c) ->
+ TermObl (subst_univs_fn_constr subst c)
+
+let get_obligation_body expand subst obl =
+ let c = get_body subst obl in
+ let c' =
if expand && obl.obl_status == Evar_kinds.Expand then
- match kind_of_term c with
- | Const c -> constant_value (Global.env ()) c
- | _ -> c
- else c
-
-let obl_substitution expand obls deps =
+ (match c with
+ | DefinedObl pc -> constant_value_in (Global.env ()) pc
+ | TermObl c -> c)
+ else (match c with
+ | DefinedObl pc -> mkConstU pc
+ | TermObl c -> c)
+ in c'
+
+let obl_substitution expand subst obls deps =
Int.Set.fold
(fun x acc ->
let xobl = obls.(x) in
let oblb =
- try get_obligation_body expand xobl
+ try get_obligation_body expand subst xobl
with e when Errors.noncritical e -> assert false
in (xobl.obl_name, (xobl.obl_type, oblb)) :: acc)
deps []
-let subst_deps expand obls deps t =
- let subst = obl_substitution expand obls deps in
- Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) subst) t
+let subst_deps expand subst obls deps t =
+ let subst = Universes.make_opt_subst subst in
+ let osubst = obl_substitution expand subst obls deps in
+ Vars.subst_univs_fn_constr subst
+ (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t)
let rec prod_app t n =
match kind_of_term (strip_outer_cast t) with
@@ -431,17 +453,18 @@ let replace_appvars subst =
in map_constr aux
let subst_prog expand obls ints prg =
- let subst = obl_substitution expand obls ints in
+ let usubst = Universes.make_opt_subst prg.prg_subst in
+ let subst = obl_substitution expand usubst obls ints in
if get_hide_obligations () then
(replace_appvars subst prg.prg_body,
- replace_appvars subst (Termops.refresh_universes prg.prg_type))
+ replace_appvars subst ((* Termops.refresh_universes *) prg.prg_type))
else
let subst' = List.map (fun (n, (_, b)) -> n, b) subst in
(Vars.replace_vars subst' prg.prg_body,
- Vars.replace_vars subst' (Termops.refresh_universes prg.prg_type))
+ Vars.replace_vars subst' ((* Termops.refresh_universes *) prg.prg_type))
-let subst_deps_obl obls obl =
- let t' = subst_deps true obls obl.obl_deps obl.obl_type in
+let subst_deps_obl subst obls obl =
+ let t' = subst_deps true subst obls obl.obl_deps obl.obl_type in
{ obl with obl_type = t' }
module ProgMap = Map.Make(Id)
@@ -509,6 +532,9 @@ let declare_definition prg =
{ const_entry_body = Future.from_val (body,Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = Some typ;
+ const_entry_proj = None;
+ const_entry_polymorphic = pi2 prg.prg_kind;
+ const_entry_universes = Univ.ContextSet.to_context prg.prg_ctx;
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None;
@@ -556,10 +582,9 @@ let declare_mutual_definition l =
let fixkind = Option.get first.prg_fixkind in
let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
+ let (local,poly,kind) = first.prg_kind in
let fixnames = first.prg_deps in
- let kind =
- fst first.prg_kind,
- if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in
+ let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in
let indexes, fixdecls =
match fixkind with
| IsFixpoint wfl ->
@@ -578,13 +603,15 @@ let declare_mutual_definition l =
mkCoFix (i,fixdecls),Declareops.no_seff) 0 l
in
(* Declare the recursive definitions *)
- let kns = List.map4 (!declare_fix_ref kind) fixnames fixdecls fixtypes fiximps in
+ let ctx = Univ.ContextSet.to_context first.prg_ctx in
+ let kns = List.map4 (!declare_fix_ref (local, poly, kind) ctx)
+ fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
List.iter Metasyntax.add_notation_interpretation first.prg_notations;
Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
let gr = List.hd kns in
let kn = match gr with ConstRef kn -> kn | _ -> assert false in
- first.prg_hook (fst first.prg_kind) gr;
+ first.prg_hook local gr;
List.iter progmap_remove l; kn
let shrink_body c =
@@ -597,20 +624,25 @@ let shrink_body c =
(b, 1, []) ctx
in List.map (fun (c,t) -> (c,None,t)) ctx, b', Array.of_list args
-let declare_obligation prg obl body =
+let declare_obligation prg obl body uctx =
let body = prg.prg_reduce body in
let ty = prg.prg_reduce obl.obl_type in
match obl.obl_status with
- | Evar_kinds.Expand -> { obl with obl_body = Some body }
+ | Evar_kinds.Expand -> { obl with obl_body = Some (TermObl body) }
| Evar_kinds.Define opaque ->
let opaque = if get_proofs_transparency () then false else opaque in
+ let poly = pi2 prg.prg_kind in
let ctx, body, args =
- if get_shrink_obligations () then shrink_body body else [], body, [||]
+ if get_shrink_obligations () && not poly then
+ shrink_body body else [], body, [||]
in
let ce =
{ const_entry_body = Future.from_val(body,Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = if List.is_empty ctx then Some ty else None;
+ const_entry_proj = None;
+ const_entry_polymorphic = poly;
+ const_entry_universes = uctx;
const_entry_opaque = opaque;
const_entry_inline_code = false;
const_entry_feedback = None;
@@ -623,9 +655,13 @@ let declare_obligation prg obl body =
Auto.add_hints false [Id.to_string prg.prg_name]
(Auto.HintsUnfoldEntry [EvalConstRef constant]);
definition_message obl.obl_name;
- { obl with obl_body = Some (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx) }
+ { obl with obl_body =
+ if poly then
+ Some (DefinedObl constant)
+ else
+ Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) }
-let init_prog_info n b t deps fixkind notations obls impls k reduce hook =
+let init_prog_info n b t ctx deps fixkind notations obls impls kind reduce hook =
let obls', b =
match b with
| None ->
@@ -645,9 +681,10 @@ let init_prog_info n b t deps fixkind notations obls impls k reduce hook =
obls, b
in
{ prg_name = n ; prg_body = b; prg_type = reduce t;
+ prg_ctx = ctx; prg_subst = Univ.LMap.empty;
prg_obligations = (obls', Array.length obls');
prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
- prg_implicits = impls; prg_kind = k; prg_reduce = reduce;
+ prg_implicits = impls; prg_kind = kind; prg_reduce = reduce;
prg_hook = hook; }
let get_prog name =
@@ -734,14 +771,14 @@ let dependencies obls n =
obls;
!res
-let goal_kind = Decl_kinds.Local, Decl_kinds.DefinitionBody Decl_kinds.Definition
+let goal_kind poly = Decl_kinds.Local, poly, Decl_kinds.DefinitionBody Decl_kinds.Definition
-let goal_proof_kind = Decl_kinds.Local, Decl_kinds.Proof Decl_kinds.Lemma
+let goal_proof_kind poly = Decl_kinds.Local, poly, Decl_kinds.Proof Decl_kinds.Lemma
-let kind_of_opacity o =
+let kind_of_obligation poly o =
match o with
- | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind
- | _ -> goal_proof_kind
+ | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind poly
+ | _ -> goal_proof_kind poly
let not_transp_msg =
str "Obligation should be transparent but was declared opaque." ++ spc () ++
@@ -755,17 +792,37 @@ let rec string_of_list sep f = function
| x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl
(* Solve an obligation using tactics, return the corresponding proof term *)
-let solve_by_tac evi t =
+
+let solve_by_tac evi t poly subst ctx =
let id = Id.of_string "H" in
+ let concl = Universes.subst_opt_univs_constr subst evi.evar_concl in
(* spiwack: the status is dropped *)
- let (entry,_) = Pfedit.build_constant_by_tactic
- id ~goal_kind evi.evar_hyps evi.evar_concl (Tacticals.New.tclCOMPLETE t) in
+ let (entry,_,subst) = Pfedit.build_constant_by_tactic
+ id ~goal_kind:(goal_kind poly) evi.evar_hyps (concl, ctx) (Tacticals.New.tclCOMPLETE t) in
let env = Global.env () in
let entry = Term_typing.handle_side_effects env entry in
let body, eff = Future.force entry.Entries.const_entry_body in
assert(Declareops.side_effects_is_empty eff);
Inductiveops.control_only_guard (Global.env ()) body;
- body
+ body, subst, entry.Entries.const_entry_universes
+
+ (* try *)
+ (* let substref = ref (Univ.LMap.empty, Univ.UContext.empty) in *)
+ (* Pfedit.start_proof id (goal_kind poly) evi.evar_hyps *)
+ (* (Universes.subst_opt_univs_constr subst evi.evar_concl, ctx) *)
+ (* (fun subst-> substref:=subst; fun _ _ -> ()); *)
+ (* Pfedit.by (tclCOMPLETE t); *)
+ (* let _,(const,_,_,_) = Pfedit.cook_proof ignore in *)
+ (* Pfedit.delete_current_proof (); *)
+ (* Inductiveops.control_only_guard (Global.env ()) *)
+ (* const.Entries.const_entry_body; *)
+ (* let subst, ctx = !substref in *)
+ (* subst_univs_fn_constr (Universes.make_opt_subst subst) const.Entries.const_entry_body, *)
+ (* subst, const.Entries.const_entry_universes *)
+ (* with reraise -> *)
+ (* let reraise = Errors.push reraise in *)
+ (* Pfedit.delete_current_proof(); *)
+ (* raise reraise *)
let rec solve_obligation prg num tac =
let user_num = succ num in
@@ -776,9 +833,12 @@ let rec solve_obligation prg num tac =
else
match deps_remaining obls obl.obl_deps with
| [] ->
- let obl = subst_deps_obl obls obl in
- Lemmas.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type
- (fun strength gr ->
+ let ctx = prg.prg_ctx in
+ let obl = subst_deps_obl prg.prg_subst obls obl in
+ let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in
+ Lemmas.start_proof obl.obl_name kind
+ (Universes.subst_opt_univs_constr prg.prg_subst obl.obl_type, ctx)
+ (fun strength gr ->
let cst = match gr with ConstRef cst -> cst | _ -> assert false in
let obl =
let transparent = evaluable_constant cst (Global.env ()) in
@@ -786,10 +846,10 @@ let rec solve_obligation prg num tac =
match obl.obl_status with
| Evar_kinds.Expand ->
if not transparent then error_not_transp ()
- else constant_value (Global.env ()) cst
+ else DefinedObl cst
| Evar_kinds.Define opaque ->
if not opaque && not transparent then error_not_transp ()
- else Globnames.constr_of_global gr
+ else DefinedObl cst
in
if transparent then
Auto.add_hints true [Id.to_string prg.prg_name]
@@ -798,8 +858,15 @@ let rec solve_obligation prg num tac =
in
let obls = Array.copy obls in
let _ = obls.(num) <- obl in
- let res =
- try update_obls prg obls (pred rem)
+(* let ctx = Univ.ContextSet.of_context ctx in *)
+ let subst = Univ.LMap.empty (** FIXME *) in
+ let res =
+ try update_obls
+ {prg with prg_body = Universes.subst_opt_univs_constr subst prg.prg_body;
+ prg_type = Universes.subst_opt_univs_constr subst prg.prg_type;
+ prg_ctx = ctx;
+ prg_subst = Univ.LMap.union prg.prg_subst subst}
+ obls (pred rem)
with e when Errors.noncritical e ->
pperror (Errors.print (Cerrors.process_vernac_interp_error e))
in
@@ -835,7 +902,7 @@ and solve_obligation_by_tac prg obls i tac =
| None ->
try
if List.is_empty (deps_remaining obls obl.obl_deps) then
- let obl = subst_deps_obl obls obl in
+ let obl = subst_deps_obl prg.prg_subst obls obl in
let tac =
match tac with
| Some t -> t
@@ -844,8 +911,11 @@ and solve_obligation_by_tac prg obls i tac =
| Some t -> t
| None -> snd (get_default_tactic ())
in
- let t = solve_by_tac (evar_of_obligation obl) tac in
- obls.(i) <- declare_obligation prg obl t;
+ let t, subst, ctx =
+ solve_by_tac (evar_of_obligation obl) tac
+ (pi2 prg.prg_kind) prg.prg_subst prg.prg_ctx
+ in
+ obls.(i) <- declare_obligation {prg with prg_subst = subst} obl t ctx;
true
else false
with e when Errors.noncritical e ->
@@ -929,10 +999,10 @@ let show_term n =
Printer.pr_constr_env (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
++ Printer.pr_constr_env (Global.env ()) prg.prg_body)
-let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
+let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
let info = str (Id.to_string n) ++ str " has type-checked" in
- let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in
+ let prg = init_prog_info n term t ctx [] None [] obls implicits kind reduce hook in
let obls,_ = prg.prg_obligations in
if Int.equal (Array.length obls) 0 then (
Flags.if_verbose msg_info (info ++ str ".");
@@ -947,12 +1017,12 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
| _ -> res)
-let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce)
+let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
?(hook=fun _ _ -> ()) notations fixkind =
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
List.iter
(fun (n, b, t, imps, obls) ->
- let prg = init_prog_info n (Some b) t deps (Some fixkind)
+ let prg = init_prog_info n (Some b) t ctx deps (Some fixkind)
notations obls imps kind reduce hook
in progmap_add n prg) l;
let _defined =
@@ -975,13 +1045,13 @@ let admit_prog prg =
(fun i x ->
match x.obl_body with
| None ->
- let x = subst_deps_obl obls x in
- (** ppedrot: seems legit to have admitted obligations as local *)
+ let x = subst_deps_obl prg.prg_subst obls x in
+ let ctx = Univ.ContextSet.to_context prg.prg_ctx in
let kn = Declare.declare_constant x.obl_name ~local:true
- (ParameterEntry (None, x.obl_type,None), IsAssumption Conjectural)
+ (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural)
in
assumption_message x.obl_name;
- obls.(i) <- { x with obl_body = Some (mkConst kn) }
+ obls.(i) <- { x with obl_body = Some (DefinedObl kn) }
| Some _ -> ())
obls;
ignore(update_obls prg obls 0)
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 746b4ed14..f03e6c446 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -17,7 +17,7 @@ open Decl_kinds
open Tacexpr
(** Forward declaration. *)
-val declare_fix_ref : (definition_kind -> Id.t ->
+val declare_fix_ref : (definition_kind -> Univ.universe_context -> Id.t ->
Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref
val declare_definition_ref :
@@ -64,6 +64,7 @@ val set_proofs_transparency : bool -> unit (* true = All transparent, false = Op
val get_proofs_transparency : unit -> bool
val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types ->
+ Univ.universe_context_set ->
?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
?kind:Decl_kinds.definition_kind ->
?tactic:unit Proofview.tactic ->
@@ -80,6 +81,7 @@ type fixpoint_kind =
val add_mutual_definitions :
(Names.Id.t * Term.constr * Term.types *
(Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
+ Univ.universe_context_set ->
?tactic:unit Proofview.tactic ->
?kind:Decl_kinds.definition_kind ->
?reduce:(Term.constr -> Term.constr) ->
diff --git a/toplevel/record.ml b/toplevel/record.ml
index dc38d2519..7411a6377 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -13,6 +13,7 @@ open Names
open Globnames
open Nameops
open Term
+open Context
open Vars
open Environ
open Declarations
@@ -23,9 +24,21 @@ open Decl_kinds
open Type_errors
open Constrexpr
open Constrexpr_ops
+open Goptions
(********** definition d'un record (structure) **************)
+(** Flag governing use of primitive projections. Disabled by default. *)
+let primitive_flag = ref false
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "use of primitive projections";
+ optkey = ["Primitive";"Projections"];
+ optread = (fun () -> !primitive_flag) ;
+ optwrite = (fun b -> primitive_flag := b) }
+
let interp_fields_evars evars env impls_env nots l =
List.fold_left2
(fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
@@ -41,15 +54,25 @@ let interp_fields_evars evars env impls_env nots l =
(push_rel d env, impl :: uimpls, d::params, impls))
(env, [], [], impls_env) nots l
+let compute_constructor_level evars env l =
+ List.fold_right (fun (n,b,t as d) (env, univ) ->
+ let univ =
+ if b = None then
+ let s = Retyping.get_sort_of env evars t in
+ Univ.sup (univ_of_sort s) univ
+ else univ
+ in (push_rel d env, univ))
+ l (env, Univ.type0m_univ)
+
let binder_of_decl = function
| Vernacexpr.AssumExpr(n,t) -> (n,None,t)
| Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c | None -> CHole (fst n, None, None))
let binders_of_decls = List.map binder_of_decl
-let typecheck_params_and_fields id t ps nots fs =
+let typecheck_params_and_fields def id t ps nots fs =
let env0 = Global.env () in
- let evars = ref Evd.empty in
+ let evars = ref (Evd.from_env ~ctx:(Univ.ContextSet.empty) env0) in
let _ =
let error bk (loc, name) =
match bk, name with
@@ -62,15 +85,48 @@ let typecheck_params_and_fields id t ps nots fs =
| LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls) ps
in
let impls_env, ((env1,newps), imps) = interp_context_evars evars env0 ps in
- let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (Termops.new_Type ()) t) newps in
+ let t' = match t with
+ | Some t ->
+ let env = push_rel_context newps env0 in
+ let s = interp_type_evars evars env ~impls:empty_internalization_env t in
+ let sred = Reductionops.whd_betadeltaiota env !evars s in
+ (match kind_of_term sred with
+ | Sort s' ->
+ (match Evd.is_sort_variable !evars s' with
+ | Some (l, _) -> evars := Evd.make_flexible_variable !evars true (* (not def) *) l; sred
+ | None -> s)
+ | _ -> user_err_loc (constr_loc t,"", str"Sort expected."))
+ | None ->
+ let uvarkind = if (* not def *) true then Evd.univ_flexible_alg else Evd.univ_flexible in
+ mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars)
+ in
+ let fullarity = it_mkProd_or_LetIn t' newps in
let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
let env2,impls,newfs,data =
interp_fields_evars evars env_ar impls_env nots (binders_of_decls fs)
in
- let sigma = Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar Evd.empty !evars in
- let newps = Evarutil.nf_rel_context_evar sigma newps in
- let newfs = Evarutil.nf_rel_context_evar sigma newfs in
- imps, newps, impls, newfs
+ let sigma =
+ Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar Evd.empty !evars in
+ let evars, nf = Evarutil.nf_evars_and_universes sigma in
+ let arity = nf t' in
+ let evars =
+ let _, univ = compute_constructor_level evars env_ar newfs in
+ let aritysort = destSort arity in
+ if Sorts.is_prop aritysort ||
+ (Sorts.is_set aritysort && engagement env0 = Some ImpredicativeSet) then
+ evars
+ else Evd.set_leq_sort evars (Type univ) aritysort
+ (* try Evarconv.the_conv_x_leq env_ar ty arity evars *)
+ (* with Reduction.NotConvertible -> *)
+ (* Pretype_errors.error_cannot_unify env_ar evars (ty, arity) *)
+ in
+ let evars, nf = Evarutil.nf_evars_and_universes evars in
+ let newps = map_rel_context nf newps in
+ let newfs = map_rel_context nf newfs in
+ let ce t = Evarutil.check_evars env0 Evd.empty evars t in
+ List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newps);
+ List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newfs);
+ Evd.universe_context evars, nf arity, imps, newps, impls, newfs
let degenerate_decl (na,b,t) =
let id = match na with
@@ -147,21 +203,25 @@ let subst_projection fid l c =
raise (NotDefinable (MissingProj (fid,List.rev !bad_projs)));
c''
-let instantiate_possibly_recursive_type indsp paramdecls fields =
+let instantiate_possibly_recursive_type indu paramdecls fields =
let subst = List.map_i (fun i _ -> mkRel i) 1 paramdecls in
- Termops.substl_rel_context (subst@[mkInd indsp]) fields
+ Termops.substl_rel_context (subst@[mkIndU indu]) fields
(* We build projections *)
let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls fields =
let env = Global.env() in
let (mib,mip) = Global.lookup_inductive indsp in
let paramdecls = mib.mind_params_ctxt in
- let r = mkInd indsp in
+ let poly = mib.mind_polymorphic and ctx = mib.mind_universes in
+ let u = Inductive.inductive_instance mib in
+ let indu = indsp, u in
+ let r = mkIndU (indsp,u) in
let rp = applist (r, Termops.extended_rel_list 0 paramdecls) in
let paramargs = Termops.extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
let x = match name with Some n -> Name n | None -> Namegen.named_hd (Global.env()) r Anonymous in
- let fields = instantiate_possibly_recursive_type indsp paramdecls fields in
+ let fields = instantiate_possibly_recursive_type indu paramdecls fields in
let lifted_fields = Termops.lift_rel_context 1 fields in
+ let nfields = List.length fields in
let (_,kinds,sp_projs,_) =
List.fold_left3
(fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) impls ->
@@ -181,18 +241,29 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
let p = mkLambda (x, lift 1 rp, ccl') in
let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
let ci = Inductiveops.make_case_info env indsp LetStyle in
- mkCase (ci, p, mkRel 1, [|branch|]) in
+ mkCase (ci, p, mkRel 1, [|branch|])
+ in
let proj =
it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
let projtyp =
it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
let kn =
try
+ let projinfo =
+ (fst indsp, mib.mind_nparams, nfields - nfi, ccl)
+ in
+ let projinfo =
+ if !primitive_flag && optci = None then Some projinfo
+ else None
+ in
let cie = {
const_entry_body =
Future.from_val (proj,Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = Some projtyp;
+ const_entry_polymorphic = poly;
+ const_entry_universes = ctx;
+ const_entry_proj = projinfo;
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None;
@@ -204,15 +275,18 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
with Type_errors.TypeError (ctx,te) ->
raise (NotDefinable (BadTypedProj (fid,ctx,te))) in
let refi = ConstRef kn in
- let constr_fi = mkConst kn in
Impargs.maybe_declare_manual_implicits false refi impls;
if coe then begin
let cl = Class.class_of_global (IndRef indsp) in
- Class.try_add_new_coercion_with_source refi ~local:false ~source:cl
+ Class.try_add_new_coercion_with_source refi ~local:false poly ~source:cl
end;
- let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
- let constr_fip = applist (constr_fi,proj_args) in
- (Some kn::sp_projs, Projection constr_fip::subst)
+ let constr_fip =
+ if !primitive_flag then mkProj (kn,mkRel 1)
+ else
+ let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
+ applist (mkConstU (kn,u),proj_args)
+ in
+ (Some kn::sp_projs, Projection constr_fip::subst)
with NotDefinable why ->
warning_or_error coe indsp why;
(None::sp_projs,NoProjection fi::subst) in
@@ -238,7 +312,7 @@ let structure_signature ctx =
open Typeclasses
-let declare_structure finite infer id idbuild paramimpls params arity fieldimpls fields
+let declare_structure finite infer poly ctx id idbuild paramimpls params arity fieldimpls fields
?(kind=StructureComponent) ?name is_coe coers sign =
let nparams = List.length params and nfields = List.length fields in
let args = Termops.extended_rel_list nfields params in
@@ -256,20 +330,23 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls
begin match finite with
| BiFinite ->
if Termops.dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) then
- error "Records declared with the keyword Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command."
+ error ("Records declared with the keyword Record or Structure cannot be recursive." ^
+ "You can, however, define recursive records using the Inductive or CoInductive command.")
| _ -> ()
end;
let mie =
{ mind_entry_params = List.map degenerate_decl params;
mind_entry_record = true;
mind_entry_finite = finite != CoFinite;
- mind_entry_inds = [mie_ind] } in
+ mind_entry_inds = [mie_ind];
+ mind_entry_polymorphic = poly;
+ mind_entry_universes = ctx } in
let kn = Command.declare_mutual_inductive_with_eliminations KernelVerbose mie [(paramimpls,[])] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
let cstr = (rsp,1) in
let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in
let build = ConstructRef cstr in
- let () = if is_coe then Class.try_add_new_coercion build ~local:false in
+ let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs);
rsp
@@ -282,43 +359,34 @@ let implicits_of_context ctx =
in ExplByPos (i, explname), (true, true, true))
1 (List.rev (Anonymous :: (List.map pi1 ctx)))
-let declare_class finite def infer id idbuild paramimpls params arity fieldimpls fields
+let declare_class finite def infer poly ctx id idbuild paramimpls params arity fieldimpls fields
?(kind=StructureComponent) ?name is_coe coers priorities sign =
let fieldimpls =
- (* Make the class and all params implicits in the projections *)
- let ctx_impls = implicits_of_context params in
- let len = succ (List.length params) in
- List.map (fun x -> ctx_impls @ Impargs.lift_implicits len x) fieldimpls
+ (* Make the class implicit in the projections, and the params if applicable. *)
+ (* if def then *)
+ let len = List.length params in
+ let impls = implicits_of_context params in
+ List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls
+ (* else List.map (fun x -> (ExplByPos (1, None), (true, true, true)) :: *)
+ (* Impargs.lift_implicits 1 x) fieldimpls *)
in
let impl, projs =
match fields with
| [(Name proj_name, _, field)] when def ->
let class_body = it_mkLambda_or_LetIn field params in
- let class_type = Option.map (fun ar -> it_mkProd_or_LetIn ar params) arity in
- let class_entry =
- { const_entry_body =
- Future.from_val (class_body,Declareops.no_seff);
- const_entry_secctx = None;
- const_entry_type = class_type;
- const_entry_opaque = false;
- const_entry_inline_code = false;
- const_entry_feedback = None;
- } in
+ let _class_type = it_mkProd_or_LetIn arity params in
+ let class_entry =
+ Declare.definition_entry (* ?types:class_type *) ~poly ~univs:ctx class_body in
let cst = Declare.declare_constant (snd id)
(DefinitionEntry class_entry, IsDefinition Definition)
in
- let inst_type = appvectc (mkConst cst) (Termops.rel_vect 0 (List.length params)) in
- let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in
- let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in
- let proj_entry =
- { const_entry_body =
- Future.from_val (proj_body,Declareops.no_seff);
- const_entry_secctx = None;
- const_entry_type = Some proj_type;
- const_entry_opaque = false;
- const_entry_inline_code = false;
- const_entry_feedback = None;
- } in
+ let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in
+ let inst_type = appvectc (mkConstU cstu) (Termops.rel_vect 0 (List.length params)) in
+ let proj_type =
+ it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in
+ let proj_body =
+ it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in
+ let proj_entry = Declare.definition_entry ~types:proj_type ~poly ~univs:ctx proj_body in
let proj_cst = Declare.declare_constant proj_name
(DefinitionEntry proj_entry, IsDefinition Definition)
in
@@ -326,16 +394,20 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
Impargs.declare_manual_implicits false cref [paramimpls];
Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
Classes.set_typeclass_transparency (EvalConstRef cst) false false;
- let sub = match List.hd coers with Some b -> Some ((if b then Backward else Forward), List.hd priorities) | None -> None in
+ let sub = match List.hd coers with
+ | Some b -> Some ((if b then Backward else Forward), List.hd priorities)
+ | None -> None
+ in
cref, [Name proj_name, sub, Some proj_cst]
| _ ->
let idarg = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in
- let ind = declare_structure BiFinite infer (snd id) idbuild paramimpls
- params (Option.default (Termops.new_Type ()) arity) fieldimpls fields
+ let ind = declare_structure BiFinite infer poly ctx (snd id) idbuild paramimpls
+ params arity fieldimpls fields
~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign
in
let coers = List.map2 (fun coe pri ->
- Option.map (fun b -> if b then Backward, pri else Forward, pri) coe)
+ Option.map (fun b ->
+ if b then Backward, pri else Forward, pri) coe)
coers priorities
in
IndRef ind, (List.map3 (fun (id, _, _) b y -> (id, b, y))
@@ -344,7 +416,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
let ctx_context =
List.map (fun (na, b, t) ->
match Typeclasses.class_of_constr t with
- | Some (_, (cl, _)) -> Some (cl.cl_impl, true) (*List.exists (fun (_, n) -> n = na) supnames)*)
+ | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true) (*FIXME: ignore universes?*)
| None -> None)
params, params
in
@@ -359,19 +431,12 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
(* k.cl_projs coers priorities; *)
add_class k; impl
-let interp_and_check_sort sort =
- Option.map (fun sort ->
- let env = Global.env() and sigma = Evd.empty in
- let s = interp_constr sigma env sort in
- if isSort (Reductionops.whd_betadeltaiota env sigma s) then s
- else user_err_loc (constr_loc sort,"", str"Sort expected.")) sort
-
open Vernacexpr
(* [fs] corresponds to fields and [ps] to parameters; [coers] is a
list telling if the corresponding fields must me declared as coercions
or subinstances *)
-let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
+let definition_structure (kind,poly,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
let cfs,notations = List.split cfs in
let cfs,priorities = List.split cfs in
let coers,fs = List.split cfs in
@@ -386,20 +451,20 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil
if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
error "Priorities only allowed for type class substructures";
(* Now, younger decl in params and fields is on top *)
- let sc = interp_and_check_sort s in
- let implpars, params, implfs, fields =
+ let ctx, arity, implpars, params, implfs, fields =
States.with_state_protection (fun () ->
- typecheck_params_and_fields idstruc sc ps notations fs) () in
+ typecheck_params_and_fields (kind = Class true) idstruc s ps notations fs) () in
let sign = structure_signature (fields@params) in
match kind with
| Class def ->
- let gr = declare_class finite def infer (loc,idstruc) idbuild
- implpars params sc implfs fields is_coe coers priorities sign in
+ let gr = declare_class finite def infer poly ctx (loc,idstruc) idbuild
+ implpars params arity implfs fields is_coe coers priorities sign in
gr
| _ ->
- let arity = Option.default (Termops.new_Type ()) sc in
let implfs = List.map
- (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in
- let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs
+ (fun impls -> implpars @ Impargs.lift_implicits
+ (succ (List.length params)) impls) implfs in
+ let ind = declare_structure finite infer poly ctx idstruc
+ idbuild implpars params arity implfs
fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
IndRef ind
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 018366667..dac8636cb 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -14,6 +14,8 @@ open Constrexpr
open Impargs
open Globnames
+val primitive_flag : bool ref
+
(** [declare_projections ref name coers params fields] declare projections of
record [ref] (if allowed) using the given [name] as argument, and put them
as coercions accordingly to [coers]; it returns the absolute names of projections *)
@@ -24,7 +26,8 @@ val declare_projections :
(Name.t * bool) list * constant option list
val declare_structure : Decl_kinds.recursivity_kind ->
- bool (**infer?*) -> Id.t -> Id.t ->
+ bool (**infer?*) -> bool (** polymorphic?*) -> Univ.universe_context ->
+ Id.t -> Id.t ->
manual_explicitation list -> rel_context -> (** params *) constr -> (** arity *)
Impargs.manual_explicitation list list -> rel_context -> (** fields *)
?kind:Decl_kinds.definition_object_kind -> ?name:Id.t ->
@@ -34,6 +37,6 @@ val declare_structure : Decl_kinds.recursivity_kind ->
inductive
val definition_structure :
- inductive_kind * Decl_kinds.recursivity_kind * bool(**infer?*)* lident with_coercion * local_binder list *
+ inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * bool(**infer?*)* lident with_coercion * local_binder list *
(local_decl_expr with_instance with_priority with_notation) list *
Id.t * constr_expr option -> global_reference
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 38717850c..1535ae617 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -45,7 +45,7 @@ module SearchBlacklist =
let iter_constructors indsp fn env nconstr =
for i = 1 to nconstr do
- let typ = Inductiveops.type_of_constructor env (indsp, i) in
+ let typ, _ = Inductiveops.type_of_constructor_in_ctx env (indsp, i) in
fn (ConstructRef (indsp, i)) env typ
done
@@ -60,14 +60,15 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
with Not_found -> (* we are in a section *) () end
| "CONSTANT" ->
let cst = Global.constant_of_delta_kn kn in
- let typ = Typeops.type_of_constant env cst in
+ let typ, _ = Environ.constant_type_in_ctx env cst in
fn (ConstRef cst) env typ
| "INDUCTIVE" ->
let mind = Global.mind_of_delta_kn kn in
let mib = Global.lookup_mind mind in
let iter_packet i mip =
let ind = (mind, i) in
- let typ = Inductiveops.type_of_inductive env ind in
+ let i = (ind, Univ.UContext.instance mib.mind_universes) in
+ let typ = Inductiveops.type_of_inductive env i in
let () = fn (IndRef ind) env typ in
let len = Array.length mip.mind_user_lc in
iter_constructors ind fn env len
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 73a509577..9851cfe87 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -66,6 +66,7 @@ let print_usage_channel co command =
\n -dump-glob f dump globalizations in file f (to be used by coqdoc)\
\n -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\
\n -impredicative-set set sort Set impredicative\
+\n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\
\n -force-load-proofs load opaque proofs in memory initially\
\n -lazy-load-proofs load opaque proofs in memory by necessity (default)\
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d5559f976..2e9bfedc7 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -252,11 +252,7 @@ let print_namespace ns =
print_list pr_id qn
in
let print_constant k body =
- let t =
- match body.Declarations.const_type with
- | Declarations.PolymorphicArity (ctx,a) -> mkArity (ctx, Term.Type a.Declarations.poly_level)
- | Declarations.NonPolymorphicType t -> t
- in
+ let t = body.Declarations.const_type in
print_kn k ++ str":" ++ spc() ++ Printer.pr_type t
in
let matches mp = match match_modulepath ns mp with
@@ -457,22 +453,22 @@ let start_proof_and_print k l hook =
let no_hook _ _ = ()
-let vernac_definition_hook = function
-| Coercion -> Class.add_coercion_hook
-| CanonicalStructure -> (fun _ -> Recordops.declare_canonical_structure)
-| SubClass -> Class.add_subclass_hook
+let vernac_definition_hook p = function
+| Coercion -> Class.add_coercion_hook p
+| CanonicalStructure -> fun _ -> Recordops.declare_canonical_structure
+| SubClass -> Class.add_subclass_hook p
| _ -> no_hook
-let vernac_definition locality (local,k) (loc,id as lid) def =
+let vernac_definition locality p (local,k) (loc,id as lid) def =
let local = enforce_locality_exp locality local in
- let hook = vernac_definition_hook k in
+ let hook = vernac_definition_hook p k in
let () = match local with
| Discharge -> Dumpglob.dump_definition lid true "var"
| Local | Global -> Dumpglob.dump_definition lid false "def"
in
(match def with
| ProveBody (bl,t) -> (* local binders, typ *)
- start_proof_and_print (local,DefinitionBody Definition)
+ start_proof_and_print (local,p,DefinitionBody Definition)
[Some lid, (bl,t,None)] no_hook
| DefineBody (bl,red_option,c,typ_opt) ->
let red_option = match red_option with
@@ -480,9 +476,9 @@ let vernac_definition locality (local,k) (loc,id as lid) def =
| Some r ->
let (evc,env)= get_current_context () in
Some (snd (interp_redexp env evc r)) in
- do_definition id (local,k) bl red_option c typ_opt hook)
+ do_definition id (local,p,k) bl red_option c typ_opt hook)
-let vernac_start_proof kind l lettop =
+let vernac_start_proof p kind l lettop =
if Dumpglob.dump () then
List.iter (fun (id, _) ->
match id with
@@ -492,7 +488,7 @@ let vernac_start_proof kind l lettop =
if lettop then
errorlabstrm "Vernacentries.StartProof"
(str "Let declarations can only be used in proof editing mode.");
- start_proof_and_print (Global, Proof kind) l no_hook
+ start_proof_and_print (Global, p, Proof kind) l no_hook
let qed_display_script = ref true
@@ -512,10 +508,10 @@ let vernac_exact_proof c =
save_proof (Vernacexpr.Proved(true,None));
if not status then Pp.feedback Interface.AddedAxiom
-let vernac_assumption locality (local, kind) l nl =
+let vernac_assumption locality poly (local, kind) l nl =
let local = enforce_locality_exp locality local in
let global = local == Global in
- let kind = local, kind in
+ let kind = local, poly, kind in
List.iter (fun (is_coe,(idl,c)) ->
if Dumpglob.dump () then
List.iter (fun lid ->
@@ -524,7 +520,7 @@ let vernac_assumption locality (local, kind) l nl =
let status = do_assumptions kind nl l in
if not status then Pp.feedback Interface.AddedAxiom
-let vernac_record k finite infer struc binders sort nameopt cfs =
+let vernac_record k poly finite infer struc binders sort nameopt cfs =
let const = match nameopt with
| None -> add_prefix "Build_" (snd (snd struc))
| Some (_,id as lid) ->
@@ -535,9 +531,9 @@ let vernac_record k finite infer struc binders sort nameopt cfs =
match x with
| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
| _ -> ()) cfs);
- ignore(Record.definition_structure (k,finite,infer,struc,binders,cfs,const,sort))
+ ignore(Record.definition_structure (k,poly,finite,infer,struc,binders,cfs,const,sort))
-let vernac_inductive finite infer indl =
+let vernac_inductive poly finite infer indl =
if Dumpglob.dump () then
List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
match cstrs with
@@ -550,13 +546,13 @@ let vernac_inductive finite infer indl =
match indl with
| [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
vernac_record (match b with Class true -> Class false | _ -> b)
- finite infer id bl c oc fs
+ poly finite infer id bl c oc fs
| [ ( id , bl , c , Class true, Constructors [l]), _ ] ->
let f =
let (coe, ((loc, id), ce)) = l in
let coe' = if coe then Some true else None in
(((coe', AssumExpr ((loc, Name id), ce)), None), [])
- in vernac_record (Class true) finite infer id bl c None [f]
+ in vernac_record (Class true) poly finite infer id bl c None [f]
| [ ( id , bl , c , Class true, _), _ ] ->
Errors.error "Definitional classes must have a single method"
| [ ( id , bl , c , Class false, Constructors _), _ ] ->
@@ -568,19 +564,19 @@ let vernac_inductive finite infer indl =
| _ -> Errors.error "Cannot handle mutually (co)inductive records."
in
let indl = List.map unpack indl in
- do_mutual_inductive indl (finite != CoFinite)
+ do_mutual_inductive indl poly (finite != CoFinite)
-let vernac_fixpoint locality local l =
+let vernac_fixpoint locality poly local l =
let local = enforce_locality_exp locality local in
if Dumpglob.dump () then
List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
- do_fixpoint local l
+ do_fixpoint local poly l
-let vernac_cofixpoint locality local l =
+let vernac_cofixpoint locality poly local l =
let local = enforce_locality_exp locality local in
if Dumpglob.dump () then
List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
- do_cofixpoint local l
+ do_cofixpoint local poly l
let vernac_scheme l =
if Dumpglob.dump () then
@@ -766,27 +762,26 @@ let vernac_require import qidl =
let vernac_canonical r =
Recordops.declare_canonical_structure (smart_global r)
-let vernac_coercion locality local ref qids qidt =
+let vernac_coercion locality poly local ref qids qidt =
let local = enforce_locality locality local in
let target = cl_of_qualid qidt in
let source = cl_of_qualid qids in
let ref' = smart_global ref in
- Class.try_add_new_coercion_with_target ref' ~local ~source ~target;
+ Class.try_add_new_coercion_with_target ref' ~local poly ~source ~target;
if_verbose msg_info (pr_global ref' ++ str " is now a coercion")
-let vernac_identity_coercion locality local id qids qidt =
+let vernac_identity_coercion locality poly local id qids qidt =
let local = enforce_locality locality local in
let target = cl_of_qualid qidt in
let source = cl_of_qualid qids in
- Class.try_add_new_identity_coercion id ~local ~source ~target
+ Class.try_add_new_identity_coercion id ~local poly ~source ~target
(* Type classes *)
-let vernac_instance abst locality sup inst props pri =
+let vernac_instance abst locality poly sup inst props pri =
let global = not (make_section_locality locality) in
Dumpglob.dump_constraint inst false "inst";
- ignore(Classes.new_instance
- ~abstract:abst ~global sup inst props pri)
+ ignore(Classes.new_instance ~abstract:abst ~global poly sup inst props pri)
let vernac_context l =
if not (Classes.context l) then Pp.feedback Interface.AddedAxiom
@@ -909,9 +904,9 @@ let vernac_remove_hints locality dbs ids =
let local = make_module_locality locality in
Auto.remove_hints local dbs (List.map Smartlocate.global_with_alias ids)
-let vernac_hints locality local lb h =
+let vernac_hints locality poly local lb h =
let local = enforce_module_locality locality local in
- Auto.add_hints local lb (Auto.interp_hints h)
+ Auto.add_hints local lb (Auto.interp_hints poly h)
let vernac_syntactic_definition locality lid x local y =
Dumpglob.dump_definition lid false "syndef";
@@ -938,7 +933,8 @@ let vernac_declare_arguments locality r l nargs flags =
then error "Arguments names must be distinct.";
let sr = smart_global r in
let inf_names =
- Impargs.compute_implicits_names (Global.env()) (Global.type_of_global sr) in
+ let ty = Global.type_of_global_unsafe sr in
+ Impargs.compute_implicits_names (Global.env ()) ty in
let string_of_name = function Anonymous -> "_" | Name id -> Id.to_string id in
let rec check li ld ls = match li, ld, ls with
| [], [], [] -> ()
@@ -1051,7 +1047,7 @@ let default_env () = {
let vernac_reserve bl =
let sb_decl = (fun (idl,c) ->
- let t = Constrintern.interp_type Evd.empty (Global.env()) c in
+ let t,ctx = Constrintern.interp_type Evd.empty (Global.env()) c in
let t = Detyping.detype false [] [] t in
let t = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
Reserve.declare_reserved_type idl t)
@@ -1218,6 +1214,15 @@ let _ =
declare_bool_option
{ optsync = true;
optdepr = false;
+ optname = "universe polymorphism";
+ optkey = ["Universe"; "Polymorphism"];
+ optread = Flags.is_universe_polymorphism;
+ optwrite = Flags.make_universe_polymorphism }
+
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
optname = "use of virtual machine inside the kernel";
optkey = ["Virtual";"Machine"];
optread = (fun () -> Vconv.use_vm ());
@@ -1378,7 +1383,10 @@ let get_current_context_of_args = function
let vernac_check_may_eval redexp glopt rc =
let (sigma, env) = get_current_context_of_args glopt in
let sigma', c = interp_open_constr sigma env rc in
- Evarconv.check_problems_are_solved sigma';
+ let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in
+ Evarconv.check_problems_are_solved env sigma';
+ let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
+ let c = nf c in
let j =
try
Evarutil.check_evars env sigma sigma' c;
@@ -1402,8 +1410,9 @@ let vernac_declare_reduction locality s r =
let vernac_global_check c =
let evmap = Evd.empty in
let env = Global.env() in
- let c = interp_constr evmap env c in
+ let c,ctx = interp_constr evmap env c in
let senv = Global.safe_env() in
+ let senv = Safe_typing.add_constraints (snd ctx) senv in
let j = Safe_typing.typing senv c in
msg_notice (print_safe_judgment env j)
@@ -1453,7 +1462,7 @@ let vernac_print = function
dump_global qid; msg_notice (print_impargs qid)
| PrintAssumptions (o,t,r) ->
(* Prints all the axioms and section variables used by a term *)
- let cstr = constr_of_global (smart_global r) in
+ let cstr = printable_constr_of_global (smart_global r) in
let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in
let nassums =
Assumptions.assumptions st ~add_opaque:o ~add_transparent:t cstr in
@@ -1522,7 +1531,7 @@ let vernac_register id r =
error "Register inline: a constant is expected";
let kn = destConst t in
match r with
- | RegisterInline -> Global.register_inline kn
+ | RegisterInline -> Global.register_inline (Univ.out_punivs kn)
(********************)
(* Proof management *)
@@ -1651,7 +1660,7 @@ let vernac_load interp fname =
(* "locality" is the prefix "Local" attribute, while the "local" component
* is the outdated/deprecated "Local" attribute of some vernacular commands
* still parsed as the obsolete_locality grammar entry for retrocompatibility *)
-let interp ?proof locality c =
+let interp ?proof locality poly c =
prerr_endline ("interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
match c with
(* Done later in this file *)
@@ -1678,14 +1687,14 @@ let interp ?proof locality c =
vernac_notation locality local c infpl sc
(* Gallina *)
- | VernacDefinition (k,lid,d) -> vernac_definition locality k lid d
- | VernacStartTheoremProof (k,l,top) -> vernac_start_proof k l top
+ | VernacDefinition (k,lid,d) -> vernac_definition locality poly k lid d
+ | VernacStartTheoremProof (k,l,top) -> vernac_start_proof poly k l top
| VernacEndProof e -> vernac_end_proof ?proof e
| VernacExactProof c -> vernac_exact_proof c
- | VernacAssumption (stre,nl,l) -> vernac_assumption locality stre l nl
- | VernacInductive (finite,infer,l) -> vernac_inductive finite infer l
- | VernacFixpoint (local, l) -> vernac_fixpoint locality local l
- | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality local l
+ | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
+ | VernacInductive (finite,infer,l) -> vernac_inductive poly finite infer l
+ | VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l
+ | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l
| VernacScheme l -> vernac_scheme l
| VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
@@ -1706,13 +1715,13 @@ let interp ?proof locality c =
| VernacRequire (export, qidl) -> vernac_require export qidl
| VernacImport (export,qidl) -> vernac_import export qidl
| VernacCanonical qid -> vernac_canonical qid
- | VernacCoercion (local,r,s,t) -> vernac_coercion locality local r s t
+ | VernacCoercion (local,r,s,t) -> vernac_coercion locality poly local r s t
| VernacIdentityCoercion (local,(_,id),s,t) ->
- vernac_identity_coercion locality local id s t
+ vernac_identity_coercion locality poly local id s t
(* Type classes *)
| VernacInstance (abst, sup, inst, props, pri) ->
- vernac_instance abst locality sup inst props pri
+ vernac_instance abst locality poly sup inst props pri
| VernacContext sup -> vernac_context sup
| VernacDeclareInstances (ids, pri) -> vernac_declare_instances locality ids pri
| VernacDeclareClass id -> vernac_declare_class id
@@ -1744,7 +1753,7 @@ let interp ?proof locality c =
| VernacCreateHintDb (dbname,b) -> vernac_create_hintdb locality dbname b
| VernacRemoveHints (dbnames,ids) -> vernac_remove_hints locality dbnames ids
| VernacHints (local,dbnames,hints) ->
- vernac_hints locality local dbnames hints
+ vernac_hints locality poly local dbnames hints
| VernacSyntacticDefinition (id,c,local,b) ->
vernac_syntactic_definition locality id c local b
| VernacDeclareImplicits (qid,l) ->
@@ -1772,7 +1781,7 @@ let interp ?proof locality c =
| VernacNop -> ()
(* Proof management *)
- | VernacGoal t -> vernac_start_proof Theorem [None,([],t,None)] false
+ | VernacGoal t -> vernac_start_proof poly Theorem [None,([],t,None)] false
| VernacAbort id -> anomaly (str "VernacAbort not handled by Stm")
| VernacAbortAll -> anomaly (str "VernacAbortAll not handled by Stm")
| VernacRestart -> anomaly (str "VernacRestart not handled by Stm")
@@ -1801,6 +1810,7 @@ let interp ?proof locality c =
(* Handled elsewhere *)
| VernacProgram _
+ | VernacPolymorphic _
| VernacLocal _ -> assert false
(* Vernaculars that take a locality flag *)
@@ -1827,6 +1837,24 @@ let check_vernac_supports_locality c l =
| VernacExtend _ ) -> ()
| Some _, _ -> Errors.error "This command does not support Locality"
+(* Vernaculars that take a polymorphism flag *)
+let check_vernac_supports_polymorphism c p =
+ match p, c with
+ | None, _ -> ()
+ | Some _, (
+ VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
+ | VernacAssumption _ | VernacInductive _
+ | VernacStartTheoremProof _
+ | VernacCoercion _ | VernacIdentityCoercion _
+ | VernacInstance _ | VernacDeclareInstances _
+ | VernacHints _
+ | VernacExtend _ ) -> ()
+ | Some _, _ -> Errors.error "This command does not support Polymorphism"
+
+let enforce_polymorphism = function
+ | None -> Flags.is_universe_polymorphism ()
+ | Some b -> b
+
(** A global default timeout, controled by option "Set Default Timeout n".
Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
@@ -1883,13 +1911,17 @@ exception HasFailed of string
let interp ?(verbosely=true) ?proof (loc,c) =
let orig_program_mode = Flags.is_program_mode () in
- let rec aux ?locality isprogcmd = function
- | VernacProgram c when not isprogcmd -> aux ?locality true c
+ let rec aux ?locality ?polymorphism isprogcmd = function
+ | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c
| VernacProgram _ -> Errors.error "Program mode specified twice"
- | VernacLocal (b, c) when Option.is_empty locality -> aux ~locality:b isprogcmd c
+ | VernacLocal (b, c) when Option.is_empty locality ->
+ aux ~locality:b ?polymorphism isprogcmd c
+ | VernacPolymorphic (b, c) when polymorphism = None ->
+ aux ?locality ~polymorphism:b isprogcmd c
+ | VernacPolymorphic (b, c) -> Errors.error "Polymorphism specified twice"
| VernacLocal _ -> Errors.error "Locality specified twice"
- | VernacStm (Command c) -> aux ?locality isprogcmd c
- | VernacStm (PGLast c) -> aux ?locality isprogcmd c
+ | VernacStm (Command c) -> aux ?locality ?polymorphism isprogcmd c
+ | VernacStm (PGLast c) -> aux ?locality ?polymorphism isprogcmd c
| VernacStm _ -> assert false (* Done by Stm *)
| VernacFail v ->
begin try
@@ -1899,7 +1931,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
Future.purify
(fun v ->
try
- aux ?locality isprogcmd v;
+ aux ?locality ?polymorphism isprogcmd v;
raise HasNotFailed
with
| HasNotFailed as e -> raise e
@@ -1919,10 +1951,10 @@ let interp ?(verbosely=true) ?proof (loc,c) =
end
| VernacTimeout (n,v) ->
current_timeout := Some n;
- aux ?locality isprogcmd v
+ aux ?locality ?polymorphism isprogcmd v
| VernacTime v ->
let tstart = System.get_time() in
- aux ?locality isprogcmd v;
+ aux ?locality ?polymorphism isprogcmd v;
let tend = System.get_time() in
let msg = if !Flags.time then "" else "Finished transaction in " in
msg_info (str msg ++ System.fmt_time_difference tstart tend)
@@ -1930,11 +1962,13 @@ let interp ?(verbosely=true) ?proof (loc,c) =
| VernacLoad (_,fname) -> vernac_load (aux false) fname
| c ->
check_vernac_supports_locality c locality;
+ check_vernac_supports_polymorphism c polymorphism;
+ let poly = enforce_polymorphism polymorphism in
Obligations.set_program_mode isprogcmd;
let psh = default_set_timeout () in
try
- if verbosely then Flags.verbosely (interp ?proof locality) c
- else Flags.silently (interp ?proof locality) c;
+ if verbosely then Flags.verbosely (interp ?proof locality poly) c
+ else Flags.silently (interp ?proof locality poly) c;
restore_timeout psh;
if orig_program_mode || not !Flags.program_mode || isprogcmd then
Flags.program_mode := orig_program_mode
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 79673df32..2da4058c8 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -126,9 +126,9 @@ let uri_params f = function
let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp)
let section_parameters = function
- | GRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_))) ->
+ | GRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_)),_) ->
get_discharged_hyp_names (path_of_global (IndRef(induri,0)))
- | GRef (_,(ConstRef cst as ref)) ->
+ | GRef (_,(ConstRef cst as ref),_) ->
get_discharged_hyp_names (path_of_global ref)
| _ -> []
@@ -141,10 +141,10 @@ let merge vl al =
let rec uri_of_constr c =
match c with
| GVar (_,id) -> url_id id
- | GRef (_,ref) -> uri_of_global ref
+ | GRef (_,ref,_) -> uri_of_global ref
| GHole _ | GEvar _ -> url_string "?"
| GSort (_,s) -> url_string (whelp_of_glob_sort s)
- | _ -> url_paren (fun () -> match c with
+ | GProj _ -> assert false
| GApp (_,f,args) ->
let inst,rest = merge (section_parameters f) args in
uri_of_constr f; url_char ' '; uri_params uri_of_constr inst;
@@ -164,10 +164,10 @@ let rec uri_of_constr c =
uri_of_constr c; url_string ":"; uri_of_constr t
| GRec _ | GIf _ | GLetTuple _ | GCases _ ->
error "Whelp does not support pattern-matching and (co-)fixpoint."
- | GVar _ | GRef _ | GHole _ | GEvar _ | GSort _ | GCast (_,_, CastCoerce) ->
+ | GCast (_,_, CastCoerce) ->
anomaly (Pp.str "Written w/o parenthesis")
| GPatVar _ ->
- anomaly (Pp.str "Found constructors not supported in constr")) ()
+ anomaly (Pp.str "Found constructors not supported in constr")
let make_string f x = Buffer.reset b; f x; Buffer.contents b
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 21:23:48 +0000