aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/closure.ml18
-rw-r--r--checker/closure.mli5
-rw-r--r--checker/declarations.ml26
-rw-r--r--checker/indtypes.ml14
-rw-r--r--checker/reduction.ml8
-rw-r--r--checker/subtyping.ml13
-rw-r--r--checker/term.ml2
-rw-r--r--checker/univ.ml12
8 files changed, 52 insertions, 46 deletions
diff --git a/checker/closure.ml b/checker/closure.ml
index bfba6c161..66e69f225 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -135,22 +135,16 @@ let betaiotazeta = mkflags [fBETA;fIOTA;fZETA]
* instantiations (cbv or lazy) are.
*)
-type 'a tableKey =
- | ConstKey of 'a
- | VarKey of Id.t
- | RelKey of int
-
type table_key = Constant.t puniverses tableKey
+
+let eq_pconstant_key (c,u) (c',u') =
+ eq_constant_key c c' && Univ.Instance.equal u u'
+
module KeyHash =
struct
type t = table_key
- let equal k1 k2 = match k1, k2 with
- | ConstKey (c1,u1), ConstKey (c2,u2) -> Constant.UserOrd.equal c1 c2
- && Univ.Instance.equal u1 u2
- | VarKey id1, VarKey id2 -> Id.equal id1 id2
- | RelKey i1, RelKey i2 -> Int.equal i1 i2
- | (ConstKey _ | VarKey _ | RelKey _), _ -> false
+ let equal = Names.eq_table_key eq_pconstant_key
open Hashset.Combine
@@ -201,8 +195,6 @@ let defined_rels flags env =
let mind_equiv_infos info = mind_equiv info.i_env
-let eq_table_key = KeyHash.equal
-
let create mk_cl flgs env =
{ i_flags = flgs;
i_repr = mk_cl;
diff --git a/checker/closure.mli b/checker/closure.mli
index 4cf02ae2b..49b07f730 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -58,10 +58,6 @@ val betaiotazeta : reds
val betadeltaiotanolet : reds
(***********************************************************************)
-type 'a tableKey =
- | ConstKey of 'a
- | VarKey of Id.t
- | RelKey of int
type table_key = Constant.t puniverses tableKey
@@ -162,7 +158,6 @@ val unfold_reference : clos_infos -> table_key -> fconstr option
(* [mind_equiv] checks whether two inductive types are intentionally equal *)
val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool
-val eq_table_key : table_key -> table_key -> bool
(************************************************************************)
(*i This is for lazy debug *)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 2fe930dca..e1d2cf6d1 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -231,7 +231,7 @@ let rec map_kn f f' c =
in
let p' = func p in
let ct' = func ct in
- let l' = Array.smartmap func l in
+ let l' = Array.Smart.map func l in
if (ci.ci_ind==ci_ind && p'==p
&& l'==l && ct'==ct)then c
else
@@ -260,21 +260,21 @@ let rec map_kn f f' c =
else LetIn (na, b', t', ct')
| App (ct,l) ->
let ct' = func ct in
- let l' = Array.smartmap func l in
+ let l' = Array.Smart.map func l in
if (ct'== ct && l'==l) then c
else App (ct',l')
| Evar (e,l) ->
- let l' = Array.smartmap func l in
+ let l' = Array.Smart.map func l in
if (l'==l) then c
else Evar (e,l')
| Fix (ln,(lna,tl,bl)) ->
- let tl' = Array.smartmap func tl in
- let bl' = Array.smartmap func bl in
+ let tl' = Array.Smart.map func tl in
+ let bl' = Array.Smart.map func bl in
if (bl == bl'&& tl == tl') then c
else Fix (ln,(lna,tl',bl'))
| CoFix(ln,(lna,tl,bl)) ->
- let tl' = Array.smartmap func tl in
- let bl' = Array.smartmap func bl in
+ let tl' = Array.Smart.map func tl in
+ let bl' = Array.Smart.map func bl in
if (bl == bl'&& tl == tl') then c
else CoFix (ln,(lna,tl',bl'))
| _ -> c
@@ -480,7 +480,7 @@ let dest_subterms p =
let (_,cstrs) = Rtree.dest_node p in
Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs
-let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
+let subst_wf_paths sub p = Rtree.Smart.map (subst_recarg sub) p
let eq_recarg r1 r2 = match r1, r2 with
| Norec, Norec -> true
@@ -513,7 +513,7 @@ let subst_decl_arity f g sub ar =
let subst_rel_declaration sub =
Term.map_rel_decl (subst_mps sub)
-let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
+let subst_rel_context sub = List.Smart.map (subst_rel_declaration sub)
let constant_is_polymorphic cb =
match cb.const_universes with
@@ -544,10 +544,10 @@ let subst_mind_packet sub mbp =
mind_consnrealdecls = mbp.mind_consnrealdecls;
mind_consnrealargs = mbp.mind_consnrealargs;
mind_typename = mbp.mind_typename;
- mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc;
+ mind_nf_lc = Array.Smart.map (subst_mps sub) mbp.mind_nf_lc;
mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
mind_arity = subst_ind_arity sub mbp.mind_arity;
- mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc;
+ mind_user_lc = Array.Smart.map (subst_mps sub) mbp.mind_user_lc;
mind_nrealargs = mbp.mind_nrealargs;
mind_nrealdecls = mbp.mind_nrealdecls;
mind_kelim = mbp.mind_kelim;
@@ -560,7 +560,7 @@ let subst_mind_packet sub mbp =
let subst_mind sub mib =
{ mib with
mind_params_ctxt = map_rel_context (subst_mps sub) mib.mind_params_ctxt;
- mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets }
+ mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets }
(* Modules *)
@@ -599,7 +599,7 @@ and subst_body : 'a. (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generi
mod_mp = subst_mp sub mb.mod_mp;
mod_expr = subst_impl sub mb.mod_expr;
mod_type = subst_signature sub mb.mod_type;
- mod_type_alg = Option.smartmap (subst_expression sub) mb.mod_type_alg }
+ mod_type_alg = Option.Smart.map (subst_expression sub) mb.mod_type_alg }
and subst_module sub mb =
subst_body (fun sub e -> implem_map (subst_signature sub) (subst_expression sub) e) sub mb
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index f403834f5..916934a81 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -598,16 +598,18 @@ let check_subtyping cumi paramsctxt env inds =
let check_inductive env kn mib =
Flags.if_verbose Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn);
(* check mind_constraints: should be consistent with env *)
- let ind_ctx =
+ let env0 =
match mib.mind_universes with
- | Monomorphic_ind _ -> Univ.UContext.empty (** Already in the global environment *)
- | Polymorphic_ind auctx -> Univ.AUContext.repr auctx
+ | Monomorphic_ind _ -> env
+ | Polymorphic_ind auctx ->
+ let uctx = Univ.AUContext.repr auctx in
+ Environ.push_context uctx env
| Cumulative_ind cumi ->
- Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi)
+ let uctx = Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi) in
+ Environ.push_context uctx env
in
- let env = Environ.push_context ind_ctx env in
(** Locally set the oracle for further typechecking *)
- let env0 = Environ.set_oracle env mib.mind_typing_flags.conv_oracle in
+ let env0 = Environ.set_oracle env0 mib.mind_typing_flags.conv_oracle in
(* check mind_record : TODO ? check #constructor = 1 ? *)
(* check mind_finite : always OK *)
(* check mind_ntypes *)
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 072dec63f..4e508dc77 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -8,6 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+open Names
open CErrors
open Util
open Cic
@@ -297,6 +298,11 @@ let oracle_order infos l2r k1 k2 =
if Int.equal n1 n2 then l2r
else n1 < n2
+let eq_table_key univ =
+ Names.eq_table_key (fun (c1,u1) (c2,u2) ->
+ Constant.UserOrd.equal c1 c2 &&
+ Univ.Instance.check_eq univ u1 u2)
+
(* Conversion between [lft1]term1 and [lft2]term2 *)
let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 =
eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[]))
@@ -343,7 +349,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
(* 2 constants, 2 local defined vars or 2 defined rels *)
| (FFlex fl1, FFlex fl2) ->
(try (* try first intensional equality *)
- if eq_table_key fl1 fl2
+ if eq_table_key univ fl1 fl2
then convert_stacks univ infos lft1 lft2 v1 v2
else raise NotConvertible
with NotConvertible ->
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 5cb38cb81..5c672d04a 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -303,7 +303,18 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
| Constant cb1 ->
let cb1 = subst_const_body subst1 cb1 in
let cb2 = subst_const_body subst2 cb2 in
- (*Start by checking types*)
+ (*Start by checking universes *)
+ let env =
+ match cb1.const_universes, cb2.const_universes with
+ | Monomorphic_const _, Monomorphic_const _ -> env
+ | Polymorphic_const auctx1, Polymorphic_const auctx2 ->
+ check_polymorphic_instance error env auctx1 auctx2
+ | Monomorphic_const _, Polymorphic_const _ ->
+ error ()
+ | Polymorphic_const _, Monomorphic_const _ ->
+ error ()
+ in
+ (* Now check types *)
let typ1 = cb1.const_type in
let typ2 = cb2.const_type in
check_type env typ1 typ2;
diff --git a/checker/term.ml b/checker/term.ml
index 0236f7867..509634bdb 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -243,7 +243,7 @@ let map_rel_decl f = function
LocalDef (n, body', typ')
let map_rel_context f =
- List.smartmap (map_rel_decl f)
+ List.Smart.map (map_rel_decl f)
let extended_rel_list n hyps =
let rec reln l p = function
diff --git a/checker/univ.ml b/checker/univ.ml
index 7d285b6fe..15673736f 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -314,7 +314,7 @@ struct
let for_all = List.for_all
- let smartmap = List.smartmap
+ let smart_map = List.Smart.map
end
@@ -911,12 +911,12 @@ struct
let is_empty x = Int.equal (Array.length x) 0
let subst_fn fn t =
- let t' = CArray.smartmap fn t in
+ let t' = CArray.Smart.map fn t in
if t' == t then t else t'
let subst s t =
let t' =
- CArray.smartmap (fun x -> try LMap.find x s with Not_found -> x) t
+ CArray.Smart.map (fun x -> try LMap.find x s with Not_found -> x) t
in if t' == t then t else t'
let pr =
@@ -952,11 +952,11 @@ let subst_instance_level s l =
| _ -> l
let subst_instance_instance s i =
- Array.smartmap (fun l -> subst_instance_level s l) i
+ Array.Smart.map (fun l -> subst_instance_level s l) i
let subst_instance_universe s u =
let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
- let u' = Universe.smartmap f u in
+ let u' = Universe.smart_map f u in
if u == u' then u
else Universe.sort u'
@@ -1097,7 +1097,7 @@ let subst_univs_level_level subst l =
let subst_univs_level_universe subst u =
let f x = Universe.Expr.map (fun u -> subst_univs_level_level subst u) x in
- let u' = Universe.smartmap f u in
+ let u' = Universe.smart_map f u in
if u == u' then u
else Universe.sort u'
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 01:57:58 +0000