diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-01 13:32:47 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:13 +0200 |
commit | c1630c9dcdf91dc965b3c375d68e3338fb737531 (patch) | |
tree | bf77e70bf7f401ff83563f50621712955b7aa618 | |
parent | 67bdc25eb69ecd485ae1c8fa2dd71d1933f355d0 (diff) |
Univs: update checker
-rw-r--r-- | checker/cic.mli | 2 | ||||
-rw-r--r-- | checker/environ.ml | 19 | ||||
-rw-r--r-- | checker/environ.mli | 2 | ||||
-rw-r--r-- | checker/mod_checking.ml | 2 | ||||
-rw-r--r-- | checker/modops.ml | 7 | ||||
-rw-r--r-- | checker/safe_typing.ml | 4 | ||||
-rw-r--r-- | checker/univ.ml | 47 | ||||
-rw-r--r-- | checker/univ.mli | 15 | ||||
-rw-r--r-- | checker/values.ml | 6 |
9 files changed, 83 insertions, 21 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 881d3ca79..bd75111a2 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -380,7 +380,7 @@ and module_body = (** algebraic type, kept if it's relevant for extraction *) mod_type_alg : module_expression option; (** set of all constraints in the module *) - mod_constraints : Univ.constraints; + mod_constraints : Univ.ContextSet.t; (** quotiented set of equivalent constants and inductive names *) mod_delta : delta_resolver; mod_retroknowledge : action list } diff --git a/checker/environ.ml b/checker/environ.ml index 6dbc44d6b..f8f5c29b7 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -84,13 +84,20 @@ let push_rec_types (lna,typarray,_) env = Array.fold_left (fun e assum -> push_rel assum e) env ctxt (* Universe constraints *) -let add_constraints c env = - if c == Univ.Constraint.empty then - env - else - let s = env.env_stratification in +let map_universes f env = + let s = env.env_stratification in { env with env_stratification = - { s with env_universes = Univ.merge_constraints c s.env_universes } } + { s with env_universes = f s.env_universes } } + +let add_constraints c env = + if c == Univ.Constraint.empty then env + else map_universes (Univ.merge_constraints c) env + +let push_context ?(strict=false) ctx env = + map_universes (Univ.merge_context strict ctx) env + +let push_context_set ?(strict=false) ctx env = + map_universes (Univ.merge_context_set strict ctx) env let check_constraints cst env = Univ.check_constraints cst env.env_stratification.env_universes diff --git a/checker/environ.mli b/checker/environ.mli index f3b2dd839..87f143d1b 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -39,6 +39,8 @@ val push_rec_types : name array * constr array * 'a -> env -> env (* Universes *) val universes : env -> Univ.universes val add_constraints : Univ.constraints -> env -> env +val push_context : ?strict:bool -> Univ.universe_context -> env -> env +val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env val check_constraints : Univ.constraints -> env -> bool (* Constants *) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 998e23c6e..78fff1bbe 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -69,7 +69,7 @@ let mk_mtb mp sign delta = mod_expr = Abstract; mod_type = sign; mod_type_alg = None; - mod_constraints = Univ.Constraint.empty; + mod_constraints = Univ.ContextSet.empty; mod_delta = delta; mod_retroknowledge = []; } diff --git a/checker/modops.ml b/checker/modops.ml index 8ccf118d3..7f07f8bf8 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -83,12 +83,13 @@ let strengthen_const mp_from l cb resolver = | Def _ -> cb | _ -> let con = Constant.make2 mp_from l in - (* let con = constant_of_delta resolver con in*) let u = - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes + if cb.const_polymorphic then + Univ.make_abstract_instance cb.const_universes else Univ.Instance.empty in - { cb with const_body = Def (Declarations.from_val (Const (con,u))) } + { cb with + const_body = Def (Declarations.from_val (Const (con,u))) } let rec strengthen_mod mp_from mp_to mb = if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index dd9482313..d3bc8373a 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -27,7 +27,7 @@ let set_engagement c = (* full_add_module adds module with universes and constraints *) let full_add_module dp mb univs digest = let env = !genv in - let env = add_constraints mb.mod_constraints env in + let env = push_context_set ~strict:true mb.mod_constraints env in let env = add_constraints univs env in let env = Modops.add_module mb env in genv := add_digest env dp digest @@ -84,7 +84,7 @@ let import file clib univs digest = let mb = clib.comp_mod in Mod_checking.check_module (add_constraints univs - (add_constraints mb.mod_constraints env)) mb.mod_mp mb; + (push_context_set ~strict:true mb.mod_constraints env)) mb.mod_mp mb; stamp_library file digest; full_add_module clib.comp_name mb univs digest diff --git a/checker/univ.ml b/checker/univ.ml index 3bcb3bc95..50c0367bb 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -244,7 +244,8 @@ module Level = struct let set = make Set let prop = make Prop - + let var i = make (Var i) + let is_small x = match data x with | Level _ -> false @@ -281,8 +282,8 @@ module Level = struct end (** Level sets and maps *) -module LSet = Set.Make (Level) -module LMap = Map.Make (Level) +module LMap = HMap.Make (Level) +module LSet = LMap.Set type 'a universe_map = 'a LMap.t @@ -559,6 +560,8 @@ let repr g u = in repr_rec u +let get_set_arc g = repr g Level.set + (* [safe_repr] also search for the canonical representative, but if the graph doesn't contain the searched universe, we add it. *) @@ -573,6 +576,24 @@ let safe_repr g u = let can = terminal u in enter_arc can g, can +exception AlreadyDeclared + +let add_universe vlev strict g = + try + let _arcv = UMap.find vlev g in + raise AlreadyDeclared + with Not_found -> + let v = terminal vlev in + let arc = + let arc = get_set_arc g in + if strict then + { arc with lt=vlev::arc.lt} + else + { arc with le=vlev::arc.le} + in + let g = enter_arc arc g in + enter_arc v g + (* reprleq : canonical_arc -> canonical_arc list *) (* All canonical arcv such that arcu<=arcv with arcv#arcu *) let reprleq g arcu = @@ -970,7 +991,7 @@ module Constraint = Set.Make(UConstraintOrd) let empty_constraint = Constraint.empty let merge_constraints c g = Constraint.fold enforce_constraint c g - + type constraints = Constraint.t (** A value with universe constraints. *) @@ -1158,6 +1179,7 @@ struct type t = LSet.t constrained let empty = LSet.empty, Constraint.empty let constraints (_, cst) = cst + let levels (ctx, _) = ctx end type universe_context_set = ContextSet.t @@ -1207,6 +1229,9 @@ let subst_instance_constraints s csts = (fun c csts -> Constraint.add (subst_instance_constraint s c) csts) csts Constraint.empty +let make_abstract_instance (ctx, _) = + Array.mapi (fun i l -> Level.var i) ctx + (** Substitute instance inst for ctx in csts *) let instantiate_univ_context (ctx, csts) = (ctx, subst_instance_constraints ctx csts) @@ -1238,6 +1263,20 @@ let subst_univs_universe fn ul = List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u)) substs nosubst +let merge_context strict ctx g = + let g = Array.fold_left + (* Be lenient, module typing reintroduces universes and + constraints due to includes *) + (fun g v -> try add_universe v strict g with AlreadyDeclared -> g) + g (UContext.instance ctx) + in merge_constraints (UContext.constraints ctx) g + +let merge_context_set strict ctx g = + let g = LSet.fold + (fun v g -> try add_universe v strict g with AlreadyDeclared -> g) + (ContextSet.levels ctx) g + in merge_constraints (ContextSet.constraints ctx) g + (** Pretty-printing *) let pr_arc = function diff --git a/checker/univ.mli b/checker/univ.mli index 742ef91ae..459adfcd6 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -74,6 +74,13 @@ val check_eq : universe check_function (** The initial graph of universes: Prop < Set *) val initial_universes : universes +(** Adds a universe to the graph, ensuring it is >= or > Set. + @raises AlreadyDeclared if the level is already declared in the graph. *) + +exception AlreadyDeclared + +val add_universe : universe_level -> bool -> universes -> universes + (** {6 Constraints. } *) type constraint_type = Lt | Le | Eq @@ -117,7 +124,7 @@ type univ_inconsistency = constraint_type * universe * universe exception UniverseInconsistency of univ_inconsistency val merge_constraints : constraints -> universes -> universes - + val check_constraints : constraints -> universes -> bool (** {6 Support for universe polymorphism } *) @@ -193,6 +200,9 @@ module ContextSet : type universe_context = UContext.t type universe_context_set = ContextSet.t +val merge_context : bool -> universe_context -> universes -> universes +val merge_context_set : bool -> universe_context_set -> universes -> universes + val empty_level_subst : universe_level_subst val is_empty_level_subst : universe_level_subst -> bool @@ -219,6 +229,9 @@ val subst_instance_constraints : universe_instance -> constraints -> constraints val instantiate_univ_context : universe_context -> universe_context val instantiate_univ_constraints : universe_instance -> universe_context -> constraints +(** Build the relative instance corresponding to the context *) +val make_abstract_instance : universe_context -> universe_instance + (** {6 Pretty-printing of universes. } *) val pr_universes : universes -> Pp.std_ppcmds diff --git a/checker/values.ml b/checker/values.ml index 45220bd05..34de511c8 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 8b7e75b4b94a2d8506a62508e0374c0a checker/cic.mli +MD5 76312d06933f47498a1981a6261c9f75 checker/cic.mli *) @@ -307,10 +307,10 @@ and v_impl = and v_noimpl = v_enum "no_impl" 1 (* Abstract is mandatory for mtb *) and v_module = Tuple ("module_body", - [|v_mp;v_impl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|]) + [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|]) and v_modtype = Tuple ("module_type_body", - [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|]) + [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|]) (** kernel/safe_typing *) |