diff options
Diffstat (limited to 'checker')
-rw-r--r-- | checker/cic.mli | 2 | ||||
-rw-r--r-- | checker/closure.ml | 18 | ||||
-rw-r--r-- | checker/closure.mli | 5 | ||||
-rw-r--r-- | checker/declarations.ml | 26 | ||||
-rw-r--r-- | checker/environ.ml | 20 | ||||
-rw-r--r-- | checker/environ.mli | 1 | ||||
-rw-r--r-- | checker/indtypes.ml | 14 | ||||
-rw-r--r-- | checker/mod_checking.ml | 9 | ||||
-rw-r--r-- | checker/reduction.ml | 8 | ||||
-rw-r--r-- | checker/subtyping.ml | 13 | ||||
-rw-r--r-- | checker/term.ml | 2 | ||||
-rw-r--r-- | checker/univ.ml | 20 | ||||
-rw-r--r-- | checker/univ.mli | 12 | ||||
-rw-r--r-- | checker/values.ml | 4 |
14 files changed, 90 insertions, 64 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index c4b00d0dc..27e2a479f 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -241,7 +241,7 @@ type constant_body = { const_type : constr; const_body_code : to_patch_substituted; const_universes : constant_universes; - const_proj : projection_body option; + const_proj : bool; const_inline_code : bool; const_typing_flags : typing_flags; } diff --git a/checker/closure.ml b/checker/closure.ml index 3f6dfd30f..b9ae4daa8 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/environ.ml b/checker/environ.ml index bbd043c8e..809150cea 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -7,6 +7,7 @@ open Declarations type globals = { env_constants : constant_body Cmap_env.t; + env_projections : projection_body Cmap_env.t; env_inductives : mutual_inductive_body Mindmap_env.t; env_inductives_eq : KerName.t KNmap.t; env_modules : module_body MPmap.t; @@ -34,6 +35,7 @@ let empty_oracle = { let empty_env = { env_globals = { env_constants = Cmap_env.empty; + env_projections = Cmap_env.empty; env_inductives = Mindmap_env.empty; env_inductives_eq = KNmap.empty; env_modules = MPmap.empty; @@ -165,12 +167,10 @@ let evaluable_constant cst env = with Not_found | NotEvaluableConst _ -> false let is_projection cst env = - not (Option.is_empty (lookup_constant cst env).const_proj) + (lookup_constant cst env).const_proj let lookup_projection p env = - match (lookup_constant (Projection.constant p) env).const_proj with - | Some pb -> pb - | None -> anomaly ("lookup_projection: constant is not a projection.") + Cmap_env.find (Projection.constant p) env.env_globals.env_projections (* Mutual Inductives *) let scrape_mind env kn= @@ -194,6 +194,13 @@ let add_mind kn mib env = Printf.ksprintf anomaly ("Inductive %s is already defined.") (MutInd.to_string kn); let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in + let new_projections = match mib.mind_record with + | None | Some None -> env.env_globals.env_projections + | Some (Some (id, kns, pbs)) -> + Array.fold_left2 (fun projs kn pb -> + Cmap_env.add kn pb projs) + env.env_globals.env_projections kns pbs + in let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in let new_inds_eq = if KerName.equal kn1 kn2 then env.env_globals.env_inductives_eq @@ -201,8 +208,9 @@ let add_mind kn mib env = KNmap.add kn1 kn2 env.env_globals.env_inductives_eq in let new_globals = { env.env_globals with - env_inductives = new_inds; - env_inductives_eq = new_inds_eq} in + env_inductives = new_inds; + env_projections = new_projections; + env_inductives_eq = new_inds_eq} in { env with env_globals = new_globals } diff --git a/checker/environ.mli b/checker/environ.mli index 81da83875..4a7597249 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -5,6 +5,7 @@ open Cic type globals = { env_constants : constant_body Cmap_env.t; + env_projections : projection_body Cmap_env.t; env_inductives : mutual_inductive_body Mindmap_env.t; env_inductives_eq : KerName.t KNmap.t; env_modules : module_body MPmap.t; 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/mod_checking.ml b/checker/mod_checking.ml index 7685863ea..ca9581167 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -47,13 +47,8 @@ let check_constant_declaration env kn cb = let () = match body_of_constant cb with | Some bd -> - (match cb.const_proj with - | None -> let j = infer envty bd in - conv_leq envty j ty - | Some pb -> - let env' = add_constant kn cb env' in - let j = infer env' bd in - conv_leq envty j ty) + let j = infer envty bd in + conv_leq envty j ty | None -> () in let env = 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 fc0764077..15673736f 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -142,7 +142,13 @@ end (** Level sets and maps *) module LMap = HMap.Make (Level) -module LSet = LMap.Set +module LSet = struct + include LMap.Set + + let pr s = + str"{" ++ prlist_with_sep spc Level.pr (elements s) ++ str"}" + +end type 'a universe_map = 'a LMap.t @@ -308,7 +314,7 @@ struct let for_all = List.for_all - let smartmap = List.smartmap + let smart_map = List.Smart.map end @@ -905,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 = @@ -946,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' @@ -1091,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' diff --git a/checker/univ.mli b/checker/univ.mli index 935f0a2b8..6cd3b3638 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -49,6 +49,7 @@ sig val make : Level.t -> t (** Create a universe representing the given level. *) + val pr : t -> Pp.t end type universe = Universe.t @@ -140,7 +141,14 @@ val check_constraints : constraints -> universes -> bool (** Polymorphic maps from universe levels to 'a *) module LMap : CSig.MapS with type key = universe_level -module LSet : CSig.SetS with type elt = universe_level +module LSet : +sig + include CSig.SetS with type elt = Level.t + + val pr : t -> Pp.t + (** Pretty-printing *) +end + type 'a universe_map = 'a LMap.t (** {6 Substitution} *) @@ -216,6 +224,8 @@ sig val instantiate : Instance.t -> t -> Constraint.t val repr : t -> UContext.t + val pr : (Level.t -> Pp.t) -> t -> Pp.t + end type abstract_universe_context = AUContext.t diff --git a/checker/values.ml b/checker/values.ml index 1ac8d7cef..f7ab95fe2 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -15,7 +15,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 c4fdf8a846aed45c27b5acb1add7d1c6 checker/cic.mli +MD5 92de14d7bf9134532e8a0cff5618bd50 checker/cic.mli *) @@ -240,7 +240,7 @@ let v_cb = v_tuple "constant_body" v_constr; Any; v_const_univs; - Opt v_projbody; + v_bool; v_bool; v_typing_flags|] |