diff options
author | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:23:14 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:23:14 +0200 |
commit | 86535d84cc3cffeee1dcd8545343f234e7285530 (patch) | |
tree | 9b221c283c2971f7ac151397231059e1d239e723 /kernel | |
parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) | |
parent | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff) |
Remove non-DFSG contentsupstream/8.4_gamma0+really8.4beta2+dfsg
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/declarations.mli | 4 | ||||
-rw-r--r-- | kernel/mod_typing.ml | 82 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 56 | ||||
-rw-r--r-- | kernel/safe_typing.mli | 2 | ||||
-rw-r--r-- | kernel/subtyping.ml | 74 | ||||
-rw-r--r-- | kernel/term.ml | 1 | ||||
-rw-r--r-- | kernel/term.mli | 6 | ||||
-rw-r--r-- | kernel/univ.ml | 111 | ||||
-rw-r--r-- | kernel/univ.mli | 4 |
9 files changed, 195 insertions, 145 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 5b800ede..7cf74ba3 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -192,6 +192,10 @@ type structure_field_body = | SFBmodule of module_body | SFBmodtype of module_type_body +(** NB: we may encounter now (at most) twice the same label in + a [structure_body], once for a module ([SFBmodule] or [SFBmodtype]) + and once for an object ([SFBconst] or [SFBmind]) *) + and structure_body = (label * structure_field_body) list and struct_expr_body = diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index a384c836..bfc6f3c7 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -35,10 +35,14 @@ let rec mp_from_mexpr = function | MSEfunctor (_,_,expr) -> mp_from_mexpr expr | MSEwith (expr,_) -> mp_from_mexpr expr -let rec list_split_assoc k rev_before = function +let is_modular = function + | SFBmodule _ | SFBmodtype _ -> true + | SFBconst _ | SFBmind _ -> false + +let rec list_split_assoc ((k,m) as km) rev_before = function | [] -> raise Not_found - | (k',b)::after when k=k' -> rev_before,b,after - | h::tail -> list_split_assoc k (h::rev_before) tail + | (k',b)::after when k=k' && is_modular b = m -> rev_before,b,after + | h::tail -> list_split_assoc km (h::rev_before) tail let discr_resolver env mtb = match mtb.typ_expr with @@ -54,35 +58,34 @@ let rec rebuild_mp mp l = let rec check_with env sign with_decl alg_sign mp equiv = let sign,wd,equiv,cst= match with_decl with - | With_Definition (id,_) -> - let sign,cb,cst = check_with_aux_def env sign with_decl mp equiv in - sign,With_definition_body(id,cb),equiv,cst - | With_Module (id,mp1) -> - let sign,equiv,cst = - check_with_aux_mod env sign with_decl mp equiv in - sign,With_module_body(id,mp1),equiv,cst in + | With_Definition (idl,c) -> + let sign,cb,cst = check_with_def env sign (idl,c) mp equiv in + sign,With_definition_body(idl,cb),equiv,cst + | With_Module (idl,mp1) -> + let sign,equiv,cst = check_with_mod env sign (idl,mp1) mp equiv in + sign,With_module_body(idl,mp1),equiv,cst + in if alg_sign = None then sign,None,equiv,cst else sign,Some (SEBwith(Option.get(alg_sign),wd)),equiv,cst -and check_with_aux_def env sign with_decl mp equiv = +and check_with_def env sign (idl,c) mp equiv = let sig_b = match sign with | SEBstruct(sig_b) -> sig_b | _ -> error_signature_expected sign in - let id,idl = match with_decl with - | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl - | With_Definition ([],_) | With_Module ([],_) -> assert false + let id,idl = match idl with + | [] -> assert false + | id::idl -> id,idl in let l = label_of_id id in try - let rev_before,spec,after = list_split_assoc l [] sig_b in + let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in let before = List.rev rev_before in let env' = Modops.add_signature mp before equiv env in - match with_decl with - | With_Definition ([],_) -> assert false - | With_Definition ([id],c) -> + if idl = [] then + (* Toplevel definition *) let cb = match spec with | SFBconst cb -> cb | _ -> error_not_a_constant l @@ -115,8 +118,9 @@ and check_with_aux_def env sign with_decl mp equiv = Cemitcodes.from_val (compile_constant_body env' def); const_constraints = cst } in - SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst - | With_Definition (_::_,c) -> + SEBstruct(before@(l,SFBconst(cb'))::after),cb',cst + else + (* Definition inside a sub-module *) let old = match spec with | SFBmodule msb -> msb | _ -> error_not_a_module (string_of_label l) @@ -124,43 +128,36 @@ and check_with_aux_def env sign with_decl mp equiv = begin match old.mod_expr with | None -> - let new_with_decl = With_Definition (idl,c) in let sign,cb,cst = - check_with_aux_def env' old.mod_type new_with_decl + check_with_def env' old.mod_type (idl,c) (MPdot(mp,l)) old.mod_delta in let new_spec = SFBmodule({old with mod_type = sign; mod_type_alg = None}) in - SEBstruct(before@((l,new_spec)::after)),cb,cst + SEBstruct(before@(l,new_spec)::after),cb,cst | Some msb -> error_generative_module_expected l end - | _ -> anomaly "Modtyping:incorrect use of with" with | Not_found -> error_no_such_label l | Reduction.NotConvertible -> error_incorrect_with_constraint l -and check_with_aux_mod env sign with_decl mp equiv = +and check_with_mod env sign (idl,mp1) mp equiv = let sig_b = match sign with | SEBstruct(sig_b) ->sig_b | _ -> error_signature_expected sign in - let id,idl = match with_decl with - | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl - | With_Definition ([],_) | With_Module ([],_) -> assert false + let id,idl = match idl with + | [] -> assert false + | id::idl -> id,idl in let l = label_of_id id in try - let rev_before,spec,after = list_split_assoc l [] sig_b in + let rev_before,spec,after = list_split_assoc (l,true) [] sig_b in let before = List.rev rev_before in - let rec mp_rec = function - | [] -> mp - | i::r -> MPdot(mp_rec r,label_of_id i) - in let env' = Modops.add_signature mp before equiv env in - match with_decl with - | With_Module ([],_) -> assert false - | With_Module ([id], mp1) -> + if idl = [] then + (* Toplevel module definition *) let old = match spec with SFBmodule msb -> msb | _ -> error_not_a_module (string_of_label l) @@ -194,7 +191,8 @@ and check_with_aux_mod env sign with_decl mp equiv = let id_subst = map_mp (MPdot(mp,l)) (MPdot(mp,l)) new_mb.mod_delta in SEBstruct(before@(l,new_spec)::subst_signature id_subst after), add_delta_resolver equiv new_mb.mod_delta,cst - | With_Module (idc,mp1) -> + else + (* Module definition of a sub-module *) let old = match spec with SFBmodule msb -> msb | _ -> error_not_a_module (string_of_label l) @@ -202,10 +200,9 @@ and check_with_aux_mod env sign with_decl mp equiv = begin match old.mod_expr with None -> - let new_with_decl = With_Module (idl,mp1) in let sign,equiv',cst = - check_with_aux_mod env' - old.mod_type new_with_decl (MPdot(mp,l)) old.mod_delta in + check_with_mod env' + old.mod_type (idl,mp1) (MPdot(mp,l)) old.mod_delta in let new_equiv = add_delta_resolver equiv equiv' in let new_spec = SFBmodule {old with mod_type = sign; @@ -223,7 +220,6 @@ and check_with_aux_mod env sign with_decl mp equiv = | _ -> error_generative_module_expected l end - | _ -> anomaly "Modtyping:incorrect use of with" with Not_found -> error_no_such_label l | Reduction.NotConvertible -> error_incorrect_with_constraint l @@ -368,7 +364,7 @@ let rec add_struct_expr_constraints env = function | SEBstruct (structure_body) -> List.fold_left - (fun env (l,item) -> add_struct_elem_constraints env item) + (fun env (_,item) -> add_struct_elem_constraints env item) env structure_body @@ -413,7 +409,7 @@ let rec struct_expr_constraints cst = function | SEBstruct (structure_body) -> List.fold_left - (fun cst (l,item) -> struct_elem_constraints cst item) + (fun cst (_,item) -> struct_elem_constraints cst item) cst structure_body diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index c2d71ebb..d7a8b005 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -101,7 +101,8 @@ type safe_environment = { old : safe_environment; env : env; modinfo : module_info; - labset : Labset.t; + modlabels : Labset.t; + objlabels : Labset.t; revstruct : structure_body; univ : Univ.constraints; engagement : engagement option; @@ -109,13 +110,16 @@ type safe_environment = loads : (module_path * module_body) list; local_retroknowledge : Retroknowledge.action list} -let exists_label l senv = Labset.mem l senv.labset +let exists_modlabel l senv = Labset.mem l senv.modlabels +let exists_objlabel l senv = Labset.mem l senv.objlabels -let check_label l senv = - if exists_label l senv then error_existing_label l +let check_modlabel l senv = + if exists_modlabel l senv then error_existing_label l +let check_objlabel l senv = + if exists_objlabel l senv then error_existing_label l -let check_labels ls senv = - Labset.iter (fun l -> check_label l senv) ls +let check_objlabels ls senv = + Labset.iter (fun l -> check_objlabel l senv) ls let labels_of_mib mib = let add,get = @@ -140,7 +144,8 @@ let rec empty_environment = variant = NONE; resolver = empty_delta_resolver; resolver_of_param = empty_delta_resolver}; - labset = Labset.empty; + modlabels = Labset.empty; + objlabels = Labset.empty; revstruct = []; univ = Univ.empty_constraint; engagement = None; @@ -172,11 +177,15 @@ type generic_name = | M let add_field ((l,sfb) as field) gn senv = - let labels = match sfb with - | SFBmind mib -> labels_of_mib mib - | _ -> Labset.singleton l + let mlabs,olabs = match sfb with + | SFBmind mib -> + let l = labels_of_mib mib in + check_objlabels l senv; (Labset.empty,l) + | SFBconst _ -> + check_objlabel l senv; (Labset.empty, Labset.singleton l) + | SFBmodule _ | SFBmodtype _ -> + check_modlabel l senv; (Labset.singleton l, Labset.empty) in - check_labels labels senv; let senv = add_constraints (constraints_of_sfb sfb) senv in let env' = match sfb, gn with | SFBconst cb, C con -> Environ.add_constant con cb senv.env @@ -187,7 +196,8 @@ let add_field ((l,sfb) as field) gn senv = in { senv with env = env'; - labset = Labset.union labels senv.labset; + modlabels = Labset.union mlabs senv.modlabels; + objlabels = Labset.union olabs senv.objlabels; revstruct = field :: senv.revstruct } (* Applying a certain function to the resolver of a safe environment *) @@ -320,7 +330,7 @@ let add_module l me inl senv = (* Interactive modules *) let start_module l senv = - check_label l senv; + check_modlabel l senv; let mp = MPdot(senv.modinfo.modpath, l) in let modinfo = { modpath = mp; label = l; @@ -331,7 +341,8 @@ let start_module l senv = mp, { old = senv; env = senv.env; modinfo = modinfo; - labset = Labset.empty; + modlabels = Labset.empty; + objlabels = Labset.empty; revstruct = []; univ = Univ.empty_constraint; engagement = None; @@ -415,7 +426,8 @@ let end_module l restype senv = mp,resolver,{ old = oldsenv.old; env = newenv; modinfo = modinfo; - labset = Labset.add l oldsenv.labset; + modlabels = Labset.add l oldsenv.modlabels; + objlabels = oldsenv.objlabels; revstruct = (l,SFBmodule mb)::oldsenv.revstruct; univ = Univ.union_constraints senv'.univ oldsenv.univ; (* engagement is propagated to the upper level *) @@ -510,7 +522,8 @@ let add_module_parameter mbid mte inl senv = variant = new_variant; resolver_of_param = add_delta_resolver resolver_of_param senv.modinfo.resolver_of_param}; - labset = senv.labset; + modlabels = senv.modlabels; + objlabels = senv.objlabels; revstruct = []; univ = senv.univ; engagement = senv.engagement; @@ -522,7 +535,7 @@ let add_module_parameter mbid mte inl senv = (* Interactive module types *) let start_modtype l senv = - check_label l senv; + check_modlabel l senv; let mp = MPdot(senv.modinfo.modpath, l) in let modinfo = { modpath = mp; label = l; @@ -533,7 +546,8 @@ let start_modtype l senv = mp, { old = senv; env = senv.env; modinfo = modinfo; - labset = Labset.empty; + modlabels = Labset.empty; + objlabels = Labset.empty; revstruct = []; univ = Univ.empty_constraint; engagement = None; @@ -584,7 +598,8 @@ let end_modtype l senv = mp, { old = oldsenv.old; env = newenv; modinfo = oldsenv.modinfo; - labset = Labset.add l oldsenv.labset; + modlabels = Labset.add l oldsenv.modlabels; + objlabels = oldsenv.objlabels; revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct; univ = Univ.union_constraints senv.univ oldsenv.univ; engagement = senv.engagement; @@ -643,7 +658,8 @@ let start_library dir senv = mp, { old = senv; env = senv.env; modinfo = modinfo; - labset = Labset.empty; + modlabels = Labset.empty; + objlabels = Labset.empty; revstruct = []; univ = Univ.empty_constraint; engagement = None; diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 6f46a45b..ad275d49 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -138,7 +138,7 @@ val typing : safe_environment -> constr -> judgment (** {7 Query } *) -val exists_label : label -> safe_environment -> bool +val exists_objlabel : label -> safe_environment -> bool (*spiwack: safe retroknowledge functionalities *) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index c141a02a..08ee67b4 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -32,15 +32,18 @@ type namedobject = | Constant of constant_body | IndType of inductive * mutual_inductive_body | IndConstr of constructor * mutual_inductive_body + +type namedmodule = | Module of module_body | Modtype of module_type_body (* adds above information about one mutual inductive: all types and constructors *) -let add_nameobjects_of_mib ln mib map = - let add_nameobjects_of_one j oib map = - let ip = (ln,j) in +let add_mib_nameobjects mp l mib map = + let ind = make_mind mp empty_dirpath l in + let add_mip_nameobjects j oib map = + let ip = (ind,j) in let map = array_fold_right_i (fun i id map -> @@ -50,22 +53,33 @@ let add_nameobjects_of_mib ln mib map = in Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map in - array_fold_right_i add_nameobjects_of_one mib.mind_packets map + array_fold_right_i add_mip_nameobjects mib.mind_packets map + + +(* creates (namedobject/namedmodule) map for the whole signature *) + +type labmap = { objs : namedobject Labmap.t; mods : namedmodule Labmap.t } +let empty_labmap = { objs = Labmap.empty; mods = Labmap.empty } -(* creates namedobject map for the whole signature *) +let get_obj mp map l = + try Labmap.find l map.objs + with Not_found -> error_no_such_label_sub l (string_of_mp mp) -let make_label_map mp list = +let get_mod mp map l = + try Labmap.find l map.mods + with Not_found -> error_no_such_label_sub l (string_of_mp mp) + +let make_labmap mp list = let add_one (l,e) map = - let add_map obj = Labmap.add l obj map in match e with - | SFBconst cb -> add_map (Constant cb) - | SFBmind mib -> - add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map - | SFBmodule mb -> add_map (Module mb) - | SFBmodtype mtb -> add_map (Modtype mtb) + | SFBconst cb -> { map with objs = Labmap.add l (Constant cb) map.objs } + | SFBmind mib -> { map with objs = add_mib_nameobjects mp l mib map.objs } + | SFBmodule mb -> { map with mods = Labmap.add l (Module mb) map.mods } + | SFBmodtype mtb -> { map with mods = Labmap.add l (Modtype mtb) map.mods } in - List.fold_right add_one list Labmap.empty + List.fold_right add_one list empty_labmap + let check_conv_error error why cst f env a1 a2 = try @@ -299,7 +313,6 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in let ty2 = Typeops.type_of_constant_type env cb2.const_type in check_conv NotConvertibleTypeField cst conv env ty1 ty2 - | _ -> error DefinitionFieldExpected let rec check_modules cst env msb1 msb2 subst1 subst2 = let mty1 = module_type_of_module None msb1 in @@ -308,33 +321,24 @@ let rec check_modules cst env msb1 msb2 subst1 subst2 = cst and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= - let map1 = make_label_map mp1 sig1 in + let map1 = make_labmap mp1 sig1 in let check_one_body cst (l,spec2) = - let info1 = - try - Labmap.find l map1 - with - Not_found -> error_no_such_label_sub l - (string_of_mp mp1) - in - match spec2 with + match spec2 with | SFBconst cb2 -> - check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 + check_constant cst env mp1 l (get_obj mp1 map1 l) + cb2 spec2 subst1 subst2 | SFBmind mib2 -> - check_inductive cst env - mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 + check_inductive cst env mp1 l (get_obj mp1 map1 l) + mp2 mib2 spec2 subst1 subst2 reso1 reso2 | SFBmodule msb2 -> - begin - match info1 with - | Module msb -> check_modules cst env msb msb2 - subst1 subst2 - | _ -> error_signature_mismatch l spec2 ModuleFieldExpected + begin match get_mod mp1 map1 l with + | Module msb -> check_modules cst env msb msb2 subst1 subst2 + | _ -> error_signature_mismatch l spec2 ModuleFieldExpected end | SFBmodtype mtb2 -> - let mtb1 = - match info1 with - | Modtype mtb -> mtb - | _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected + let mtb1 = match get_mod mp1 map1 l with + | Modtype mtb -> mtb + | _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected in let env = add_module (module_body_of_type mtb2.typ_mp mtb2) (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in diff --git a/kernel/term.ml b/kernel/term.ml index dcb63cf7..46bc7c56 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -322,6 +322,7 @@ let isCast c = match kind_of_term c with Cast _ -> true | _ -> false (* Tests if a de Bruijn index *) let isRel c = match kind_of_term c with Rel _ -> true | _ -> false +let isRelN n c = match kind_of_term c with Rel n' -> n = n' | _ -> false (* Tests if a variable *) let isVar c = match kind_of_term c with Var _ -> true | _ -> false diff --git a/kernel/term.mli b/kernel/term.mli index d5899f18..e83be6d6 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -229,8 +229,9 @@ val kind_of_type : types -> (constr, types) kind_of_type (** {6 Simple term case analysis. } *) val isRel : constr -> bool +val isRelN : int -> constr -> bool val isVar : constr -> bool -val isVarId : identifier -> constr -> bool +val isVarId : identifier -> constr -> bool val isInd : constr -> bool val isEvar : constr -> bool val isMeta : constr -> bool @@ -435,8 +436,7 @@ val it_mkProd_or_LetIn : types -> rel_context -> types (** {6 Other term destructors. } *) (** Transforms a product term {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %} into the pair - {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a product. - It includes also local definitions *) + {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a product. *) val decompose_prod : constr -> (name*constr) list * constr (** Transforms a lambda term {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair diff --git a/kernel/univ.ml b/kernel/univ.ml index a8934544..0193542a 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -260,46 +260,62 @@ type order = EQ | LT | LE | NLE (** [compare_neq] : is [arcv] in the transitive upward closure of [arcu] ? - We try to avoid visiting unneeded parts of this transitive closure, - by stopping as soon as [arcv] is encountered. During the recursive - traversal, [lt_done] and [le_done] are universes we have already - visited, they do not contain [arcv]. The 3rd arg is - [(lt_todo,le_todo)], two lists of universes not yet considered, - known to be above [arcu], strictly or not. + In [strict] mode, we fully distinguish between LE and LT, while in + non-strict mode, we simply answer LE for both situations. + + If [arcv] is encountered in a LT part, we could directly answer + without visiting unneeded parts of this transitive closure. + In [strict] mode, if [arcv] is encountered in a LE part, we could only + change the default answer (1st arg [c]) from NLE to LE, since a strict + constraint may appear later. During the recursive traversal, + [lt_done] and [le_done] are universes we have already visited, + they do not contain [arcv]. The 4rd arg is [(lt_todo,le_todo)], + two lists of universes not yet considered, known to be above [arcu], + strictly or not. We use depth-first search, but the presence of [arcv] in [new_lt] is checked as soon as possible : this seems to be slightly faster on a test. *) -let compare_neq g arcu arcv = - let rec cmp lt_done le_done = function - | [],[] -> NLE +let compare_neq strict g arcu arcv = + let rec cmp c lt_done le_done = function + | [],[] -> c | arc::lt_todo, le_todo -> if List.memq arc lt_done then - cmp lt_done le_done (lt_todo,le_todo) + cmp c lt_done le_done (lt_todo,le_todo) else let lt_new = can g (arc.lt@arc.le) in - if List.memq arcv lt_new then LT - else cmp (arc::lt_done) le_done (lt_new@lt_todo,le_todo) + if List.memq arcv lt_new then + if strict then LT else LE + else cmp c (arc::lt_done) le_done (lt_new@lt_todo,le_todo) | [], arc::le_todo -> - if arc == arcv then LE - (* No need to continue inspecting universes above arc: - if arcv is strictly above arc, then we would have a cycle *) + if arc == arcv then + (* No need to continue inspecting universes above arc: + if arcv is strictly above arc, then we would have a cycle. + But we cannot answer LE yet, a stronger constraint may + come later from [le_todo]. *) + if strict then cmp LE lt_done le_done ([],le_todo) else LE else if (List.memq arc lt_done) || (List.memq arc le_done) then - cmp lt_done le_done ([],le_todo) + cmp c lt_done le_done ([],le_todo) else let lt_new = can g arc.lt in - if List.memq arcv lt_new then LT + if List.memq arcv lt_new then + if strict then LT else LE else let le_new = can g arc.le in - cmp lt_done (arc::le_done) (lt_new, le_new@le_todo) + cmp c lt_done (arc::le_done) (lt_new, le_new@le_todo) in - cmp [] [] ([],[arcu]) + cmp NLE [] [] ([],[arcu]) let compare g arcu arcv = - if arcu == arcv then EQ else compare_neq g arcu arcv + if arcu == arcv then EQ else compare_neq true g arcu arcv + +let is_leq g arcu arcv = + arcu == arcv || (compare_neq false g arcu arcv = LE) + +let is_lt g arcu arcv = (compare g arcu arcv = LT) (* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ compare(u,v) = LT or LE => compare(v,u) = NLE @@ -337,11 +353,11 @@ let rec check_eq g u v = let compare_greater g strict u v = let g, arcu = safe_repr g u in let g, arcv = safe_repr g v in - if not strict && arcv == snd (safe_repr g UniverseLevel.Set) then true else - match compare g arcv arcu with - | (EQ|LE) -> not strict - | LT -> true - | NLE -> false + if strict then + is_lt g arcv arcu + else + arcv == snd (safe_repr g UniverseLevel.Set) || is_leq g arcv arcu + (* let compare_greater g strict u v = let b = compare_greater g strict u v in @@ -368,9 +384,8 @@ let setlt g arcu arcv = (* checks that non-redundant *) let setlt_if (g,arcu) v = let arcv = repr g v in - match compare g arcu arcv with - | LT -> g, arcu - | _ -> setlt g arcu arcv + if is_lt g arcu arcv then g, arcu + else setlt g arcu arcv (* setleq : UniverseLevel.t -> UniverseLevel.t -> unit *) (* forces u >= v *) @@ -383,9 +398,8 @@ let setleq g arcu arcv = (* checks that non-redundant *) let setleq_if (g,arcu) v = let arcv = repr g v in - match compare g arcu arcv with - | NLE -> setleq g arcu arcv - | _ -> g, arcu + if is_leq g arcu arcv then g, arcu + else setleq g arcu arcv (* merge : UniverseLevel.t -> UniverseLevel.t -> unit *) (* we assume compare(u,v) = LE *) @@ -429,14 +443,12 @@ let error_inconsistency o u v = raise (UniverseInconsistency (o,Atom u,Atom v)) let enforce_univ_leq u v g = let g,arcu = safe_repr g u in let g,arcv = safe_repr g v in - match compare g arcu arcv with - | NLE -> - (match compare g arcv arcu with - | LT -> error_inconsistency Le u v - | LE -> merge g arcv arcu - | NLE -> fst (setleq g arcu arcv) - | EQ -> anomaly "Univ.compare") - | _ -> g + if is_leq g arcu arcv then g + else match compare g arcv arcu with + | LT -> error_inconsistency Le u v + | LE -> merge g arcv arcu + | NLE -> fst (setleq g arcu arcv) + | EQ -> anomaly "Univ.compare" (* enforc_univ_eq : UniverseLevel.t -> UniverseLevel.t -> unit *) (* enforc_univ_eq u v will force u=v if possible, will fail otherwise *) @@ -463,9 +475,8 @@ let enforce_univ_lt u v g = | LE -> fst (setlt g arcu arcv) | EQ -> error_inconsistency Lt u v | NLE -> - (match compare g arcv arcu with - | NLE -> fst (setlt g arcu arcv) - | _ -> error_inconsistency Lt u v) + if is_leq g arcv arcu then error_inconsistency Lt u v + else fst (setlt g arcu arcv) (* Constraints and sets of consrtaints. *) @@ -480,7 +491,13 @@ let enforce_constraint cst g = module Constraint = Set.Make( struct type t = univ_constraint - let compare = Pervasives.compare + let compare (u,c,v) (u',c',v') = + let i = Pervasives.compare c c' in + if i <> 0 then i + else + let i' = UniverseLevel.compare u u' in + if i' <> 0 then i' + else UniverseLevel.compare v v' end) type constraints = Constraint.t @@ -784,6 +801,14 @@ let no_upper_constraints u cst = | Atom u -> Constraint.for_all (fun (u1,_,_) -> u1 <> u) cst | Max _ -> anomaly "no_upper_constraints" +(* Is u mentionned in v (or equals to v) ? *) + +let univ_depends u v = + match u, v with + | Atom u, Atom v -> u = v + | Atom u, Max (gel,gtl) -> List.mem u gel || List.mem u gtl + | _ -> anomaly "univ_depends given a non-atomic 1st arg" + (* Pretty-printing *) let pr_arc = function diff --git a/kernel/univ.mli b/kernel/univ.mli index 8b3f6291..e4e66915 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -91,6 +91,10 @@ val subst_large_constraints : val no_upper_constraints : universe -> constraints -> bool +(** Is u mentionned in v (or equals to v) ? *) + +val univ_depends : universe -> universe -> bool + (** {6 Pretty-printing of universes. } *) val pr_uni_level : universe_level -> Pp.std_ppcmds |