diff options
Diffstat (limited to 'kernel')
36 files changed, 1492 insertions, 1195 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index ef0c9af4f..5ba93eda0 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -29,11 +29,19 @@ let patch_char4 buff pos c1 c2 c3 c4 = String.unsafe_set buff (pos + 2) c3; String.unsafe_set buff (pos + 3) c4 -let patch_int buff pos n = +let patch buff (pos, n) = patch_char4 buff pos (Char.unsafe_chr n) (Char.unsafe_chr (n asr 8)) (Char.unsafe_chr (n asr 16)) (Char.unsafe_chr (n asr 24)) +let patch_int buff patches = + (* copy code *before* patching because of nested evaluations: + the code we are patching might be called (and thus "concurrently" patched) + and results in wrong results. Side-effects... *) + let buff = String.copy buff in + let () = List.iter (fun p -> patch buff p) patches in + buff + (* Buffering of bytecode *) let out_buffer = ref(String.create 1024) @@ -366,6 +374,8 @@ let to_memory (init_code, fun_code, fv) = emit fun_code; let code = String.create !out_position in String.unsafe_blit !out_buffer 0 code 0 !out_position; + (** Later uses of this string are all purely functional *) + let code = CString.hcons code in let reloc = List.rev !reloc_info in Array.iter (fun lbl -> (match lbl with diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index 10f3a6087..c80edd596 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -13,11 +13,9 @@ val subst_patch : Mod_subst.substitution -> patch -> patch type emitcodes -val copy : emitcodes -> emitcodes - val length : emitcodes -> int -val patch_int : emitcodes -> (*pos*)int -> int -> unit +val patch_int : emitcodes -> ((*pos*)int * int) list -> emitcodes type to_patch = emitcodes * (patch list) * fv diff --git a/kernel/closure.ml b/kernel/closure.ml index 03e70495f..1a50478e0 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -346,7 +346,6 @@ and fterm = | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs - | FCase of case_info * fconstr * fconstr * fconstr array | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) | FLambda of int * (Name.t * constr) list * constr * fconstr subs | FProd of Name.t * fconstr * fconstr @@ -376,7 +375,6 @@ let update v1 no t = type stack_member = | Zapp of fconstr array - | Zcase of case_info * fconstr * fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs | Zproj of int * int * constant | Zfix of fconstr * stack @@ -569,10 +567,6 @@ let rec to_constr constr_fun lfts v = | FFlex (ConstKey op) -> mkConstU op | FInd op -> mkIndU op | FConstruct op -> mkConstructU op - | FCase (ci,p,c,ve) -> - mkCase (ci, constr_fun lfts p, - constr_fun lfts c, - CArray.Fun1.map constr_fun lfts ve) | FCaseT (ci,p,c,ve,env) -> mkCase (ci, constr_fun lfts (mk_clos env p), constr_fun lfts c, @@ -646,9 +640,6 @@ let rec zip m stk = match stk with | [] -> m | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s - | Zcase(ci,p,br)::s -> - let t = FCase(ci, p, m, br) in - zip {norm=neutr m.norm; term=t} s | ZcaseT(ci,p,br,e)::s -> let t = FCaseT(ci, p, m, br, e) in zip {norm=neutr m.norm; term=t} s @@ -731,7 +722,7 @@ let rec get_args n tys f e stk = (* Eta expansion: add a reference to implicit surrounding lambda at end of stack *) let rec eta_expand_stack = function - | (Zapp _ | Zfix _ | Zcase _ | ZcaseT _ | Zproj _ + | (Zapp _ | Zfix _ | ZcaseT _ | Zproj _ | Zshift _ | Zupdate _ as e) :: s -> e :: eta_expand_stack s | [] -> @@ -842,7 +833,6 @@ let rec knh info m stk = | FCLOS(t,e) -> knht info e t (zupdate m stk) | FLOCKED -> assert false | FApp(a,b) -> knh info a (append_stack b (zupdate m stk)) - | FCase(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::zupdate m stk) | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate m stk) | FFix(((ri,n),(_,_,_)),_) -> (match get_nth_arg m ri.(n) stk with @@ -904,10 +894,6 @@ let rec knr info m stk = | None -> (set_norm m; (m,stk))) | FConstruct((ind,c),u) when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with - (depth, args, Zcase(ci,_,br)::s) -> - assert (ci.ci_npar>=0); - let rargs = drop_parameters depth ci.ci_npar args in - kni info br.(c-1) (rargs@s) | (depth, args, ZcaseT(ci,_,br,e)::s) -> assert (ci.ci_npar>=0); let rargs = drop_parameters depth ci.ci_npar args in @@ -924,7 +910,7 @@ let rec knr info m stk = | (_,args,s) -> (m,args@s)) | FCoFix _ when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with - (_, args, (((Zcase _|ZcaseT _|Zproj _)::_) as stk')) -> + (_, args, (((ZcaseT _|Zproj _)::_) as stk')) -> let (fxe,fxbd) = contract_fix_vect m.term in knit info fxe fxbd (args@stk') | (_,args,s) -> (m,args@s)) @@ -953,9 +939,6 @@ let rec zip_term zfun m stk = | [] -> m | Zapp args :: s -> zip_term zfun (mkApp(m, Array.map zfun args)) s - | Zcase(ci,p,br)::s -> - let t = mkCase(ci, zfun p, m, Array.map zfun br) in - zip_term zfun t s | ZcaseT(ci,p,br,e)::s -> let t = mkCase(ci, zfun (mk_clos e p), m, Array.map (fun b -> zfun (mk_clos e b)) br) in diff --git a/kernel/closure.mli b/kernel/closure.mli index a3b0e0f30..c6f212aa5 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -119,7 +119,6 @@ type fterm = | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs - | FCase of case_info * fconstr * fconstr * fconstr array | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) | FLambda of int * (Name.t * constr) list * constr * fconstr subs | FProd of Name.t * fconstr * fconstr @@ -136,7 +135,6 @@ type fterm = type stack_member = | Zapp of fconstr array - | Zcase of case_info * fconstr * fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs | Zproj of int * int * constant | Zfix of fconstr * stack diff --git a/kernel/constr.ml b/kernel/constr.ml index e2b1d3fd9..753d18845 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -545,8 +545,8 @@ let equal m n = eq_constr m n (* to avoid tracing a recursive fun *) let eq_constr_univs univs m n = if m == n then true else - let eq_universes _ = Univ.Instance.check_eq univs in - let eq_sorts s1 s2 = s1 == s2 || Univ.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in + let eq_universes _ = UGraph.check_eq_instances univs in + let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let rec eq_constr' m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n in compare_head_gen eq_universes eq_sorts eq_constr' m n @@ -554,11 +554,11 @@ let eq_constr_univs univs m n = let leq_constr_univs univs m n = if m == n then true else - let eq_universes _ = Univ.Instance.check_eq univs in + let eq_universes _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = s1 == s2 || - Univ.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in + UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let leq_sorts s1 s2 = s1 == s2 || - Univ.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in + UGraph.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let rec eq_constr' m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n in @@ -571,12 +571,12 @@ let eq_constr_univs_infer univs m n = if m == n then true, Constraint.empty else let cstrs = ref Constraint.empty in - let eq_universes strict = Univ.Instance.check_eq univs in + let eq_universes strict = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true + if UGraph.check_eq univs u1 u2 then true else (cstrs := Univ.enforce_eq u1 u2 !cstrs; true) @@ -591,12 +591,12 @@ let leq_constr_univs_infer univs m n = if m == n then true, Constraint.empty else let cstrs = ref Constraint.empty in - let eq_universes strict l l' = Univ.Instance.check_eq univs l l' in + let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true + if UGraph.check_eq univs u1 u2 then true else (cstrs := Univ.enforce_eq u1 u2 !cstrs; true) in @@ -604,7 +604,7 @@ let leq_constr_univs_infer univs m n = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_leq univs u1 u2 then true + if UGraph.check_leq univs u1 u2 then true else (cstrs := Univ.enforce_leq u1 u2 !cstrs; true) diff --git a/kernel/constr.mli b/kernel/constr.mli index e6a3e71f8..5a370d31d 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -205,19 +205,19 @@ val equal : constr -> constr -> bool (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, application grouping and the universe equalities in [u]. *) -val eq_constr_univs : constr Univ.check_function +val eq_constr_univs : constr UGraph.check_function (** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo alpha, casts, application grouping and the universe inequalities in [u]. *) -val leq_constr_univs : constr Univ.check_function +val leq_constr_univs : constr UGraph.check_function (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, application grouping and the universe equalities in [u]. *) -val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.constrained +val eq_constr_univs_infer : UGraph.t -> constr -> constr -> bool Univ.constrained (** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo alpha, casts, application grouping and the universe inequalities in [u]. *) -val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.constrained +val leq_constr_univs_infer : UGraph.t -> constr -> constr -> bool Univ.constrained (** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and ignoring universe instances. *) diff --git a/kernel/context.ml b/kernel/context.ml index 796f06d37..5923048fa 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -111,6 +111,20 @@ let instance_from_named_context sign = in List.map_filter filter sign +(** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] + with n = |Δ| and with the local definitions of [Γ] skipped in + [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) + +let extended_rel_list n hyps = + let rec reln l p = function + | (_, None, _) :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps + | (_, Some _, _) :: hyps -> reln l (p+1) hyps + | [] -> l + in + reln [] 1 hyps + +let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps) + let fold_named_context f l ~init = List.fold_right f l init let fold_named_list_context f l ~init = List.fold_right f l init let fold_named_context_reverse f ~init l = List.fold_left f init l diff --git a/kernel/context.mli b/kernel/context.mli index 5279aefb6..735467747 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -82,8 +82,21 @@ val fold_named_context_reverse : ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a (** {6 Section-related auxiliary functions } *) + +(** [instance_from_named_context Ω] builds an instance [args] such + that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local + definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it + gives [Var id1, Var id3]. All [idj] are supposed distinct. *) val instance_from_named_context : named_context -> Constr.t list +(** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] + with n = |Δ| and with the local definitions of [Γ] skipped in + [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) +val extended_rel_list : int -> rel_context -> Constr.t list + +(** [extended_rel_vect n Γ] does the same, returning instead an array. *) +val extended_rel_vect : int -> rel_context -> Constr.t array + (** {6 ... } *) (** Signatures of ordered optionally named variables, intended to be accessed by de Bruijn indices *) @@ -120,3 +133,4 @@ val rel_context_length : rel_context -> int val rel_context_nhyps : rel_context -> int (** Indicates whether a LetIn or a Lambda, starting from oldest declaration *) val rel_context_tags : rel_context -> bool list + diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 28f0fa4f2..aa9ef66fe 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -206,19 +206,13 @@ and slot_for_fv env fv = assert false and eval_to_patch env (buff,pl,fv) = - (* copy code *before* patching because of nested evaluations: - the code we are patching might be called (and thus "concurrently" patched) - and results in wrong results. Side-effects... *) - let buff = Cemitcodes.copy buff in let patch = function - | Reloc_annot a, pos -> patch_int buff pos (slot_for_annot a) - | Reloc_const sc, pos -> patch_int buff pos (slot_for_str_cst sc) - | Reloc_getglobal kn, pos -> -(* Pp.msgnl (str"patching global: "++str(debug_string_of_con kn));*) - patch_int buff pos (slot_for_getglobal env kn); -(* Pp.msgnl (str"patch done: "++str(debug_string_of_con kn))*) + | Reloc_annot a, pos -> (pos, slot_for_annot a) + | Reloc_const sc, pos -> (pos, slot_for_str_cst sc) + | Reloc_getglobal kn, pos -> (pos, slot_for_getglobal env kn) in - List.iter patch pl; + let patches = List.map_left patch pl in + let buff = patch_int buff patches in let vm_env = Array.map (slot_for_fv env) fv in let tc = tcode_of_code buff (length buff) in eval_tcode tc vm_env diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 248504c1b..73cfd0122 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -308,3 +308,88 @@ let string_of_side_effect { Entries.eff } = match eff with | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.string_of_con c ^ ")" | Entries.SEscheme (cl,_) -> "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) ^ ")" + +(** Hashconsing of modules *) + +let hcons_functorize hty he hself f = match f with +| NoFunctor e -> + let e' = he e in + if e == e' then f else NoFunctor e' +| MoreFunctor (mid, ty, nf) -> + (** FIXME *) + let mid' = mid in + let ty' = hty ty in + let nf' = hself nf in + if mid == mid' && ty == ty' && nf == nf' then f + else MoreFunctor (mid, ty', nf') + +let hcons_module_alg_expr me = me + +let rec hcons_structure_field_body sb = match sb with +| SFBconst cb -> + let cb' = hcons_const_body cb in + if cb == cb' then sb else SFBconst cb' +| SFBmind mib -> + let mib' = hcons_mind mib in + if mib == mib' then sb else SFBmind mib' +| SFBmodule mb -> + let mb' = hcons_module_body mb in + if mb == mb' then sb else SFBmodule mb' +| SFBmodtype mb -> + let mb' = hcons_module_body mb in + if mb == mb' then sb else SFBmodtype mb' + +and hcons_structure_body sb = + (** FIXME *) + let map (l, sfb as fb) = + let l' = Names.Label.hcons l in + let sfb' = hcons_structure_field_body sfb in + if l == l' && sfb == sfb' then fb else (l', sfb') + in + List.smartmap map sb + +and hcons_module_signature ms = + hcons_functorize hcons_module_body hcons_structure_body hcons_module_signature ms + +and hcons_module_expression me = + hcons_functorize hcons_module_body hcons_module_alg_expr hcons_module_expression me + +and hcons_module_implementation mip = match mip with +| Abstract -> Abstract +| Algebraic me -> + let me' = hcons_module_expression me in + if me == me' then mip else Algebraic me' +| Struct ms -> + let ms' = hcons_module_signature ms in + if ms == ms' then mip else Struct ms +| FullStruct -> FullStruct + +and hcons_module_body mb = + let mp' = mb.mod_mp in + let expr' = hcons_module_implementation mb.mod_expr in + let type' = hcons_module_signature mb.mod_type in + let type_alg' = mb.mod_type_alg in + let constraints' = Univ.hcons_universe_context_set mb.mod_constraints in + let delta' = mb.mod_delta in + let retroknowledge' = mb.mod_retroknowledge in + + if + mb.mod_mp == mp' && + mb.mod_expr == expr' && + mb.mod_type == type' && + mb.mod_type_alg == type_alg' && + mb.mod_constraints == constraints' && + mb.mod_delta == delta' && + mb.mod_retroknowledge == retroknowledge' + then mb + else { + mod_mp = mp'; + mod_expr = expr'; + mod_type = type'; + mod_type_alg = type_alg'; + mod_constraints = constraints'; + mod_delta = delta'; + mod_retroknowledge = retroknowledge'; + } + +and hcons_module_type_body mtb = hcons_module_body mtb diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 1b8700958..1d0811882 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -77,3 +77,4 @@ val inductive_context : mutual_inductive_body -> universe_context val hcons_const_body : constant_body -> constant_body val hcons_mind : mutual_inductive_body -> mutual_inductive_body +val hcons_module_body : module_body -> module_body diff --git a/kernel/environ.ml b/kernel/environ.ml index 429aba4f7..09fe64d77 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -188,10 +188,10 @@ let map_universes f env = let add_constraints c env = if Univ.Constraint.is_empty c then env - else map_universes (Univ.merge_constraints c) env + else map_universes (UGraph.merge_constraints c) env let check_constraints c env = - Univ.check_constraints c env.env_stratification.env_universes + UGraph.check_constraints c env.env_stratification.env_universes let push_constraints_to_env (_,univs) env = add_constraints univs env @@ -199,19 +199,19 @@ let push_constraints_to_env (_,univs) env = let add_universes strict ctx g = let g = Array.fold_left (* Be lenient, module typing reintroduces universes and constraints due to includes *) - (fun g v -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g) + (fun g v -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) g (Univ.Instance.to_array (Univ.UContext.instance ctx)) in - Univ.merge_constraints (Univ.UContext.constraints ctx) g + UGraph.merge_constraints (Univ.UContext.constraints ctx) g let push_context ?(strict=false) ctx env = map_universes (add_universes strict ctx) env let add_universes_set strict ctx g = let g = Univ.LSet.fold - (fun v g -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g) + (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) (Univ.ContextSet.levels ctx) g - in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g + in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g let push_context_set ?(strict=false) ctx env = map_universes (add_universes_set strict ctx) env @@ -602,7 +602,10 @@ let dispatch = Array.init 31 (fun n -> mkConstruct (digit_ind, nth_digit_plus_one i (30-n))) in - mkApp(mkConstruct(ind, 1), array_of_int tag) + (* We check that no bit above 31 is set to one. This assertion used to + fail in the VM, and led to conversion tests failing at Qed. *) + assert (Int.equal (tag lsr 31) 0); + mkApp(mkConstruct(ind, 1), array_of_int tag) in (* subfunction which dispatches the compiling information of an diff --git a/kernel/environ.mli b/kernel/environ.mli index dfe6cc85b..2eab32e72 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -41,7 +41,7 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool val empty_env : env -val universes : env -> Univ.universes +val universes : env -> UGraph.t val rel_context : env -> rel_context val named_context : env -> named_context val named_context_val : env -> named_context_val diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index a46c33bf0..11df40caf 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -30,8 +30,13 @@ let indices_matter = ref false let enforce_indices_matter () = indices_matter := true let is_indices_matter () = !indices_matter -(* Same as noccur_between but may perform reductions. - Could be refined more... *) +(* [weaker_noccur_between env n nvars t] (defined above), checks that + no de Bruijn indices between [n] and [n+nvars] occur in [t]. If + some such occurrences are found, then reduction is performed + (lazily for efficiency purposes) in order to determine whether + these occurrences are occurrences in the normal form. If the + occurrences are eliminated a witness reduct [Some t'] of [t] is + returned otherwise [None] is returned. *) let weaker_noccur_between env x nvars t = if noccur_between x nvars t then Some t else @@ -284,7 +289,7 @@ let typecheck_inductive env mie = let full_polymorphic () = let defu = Term.univ_of_sort def_level in let is_natural = - type_in_type env || (check_leq (universes env') infu defu) + type_in_type env || (UGraph.check_leq (universes env') infu defu) in let _ = (** Impredicative sort, always allow *) @@ -310,7 +315,7 @@ let typecheck_inductive env mie = (* conclusions of the parameters *) (* We enforce [u >= lev] in case [lev] has a strict upper *) (* constraints over [u] *) - let b = type_in_type env || check_leq (universes env') infu u in + let b = type_in_type env || UGraph.check_leq (universes env') infu u in if not b then anomaly ~label:"check_inductive" (Pp.str"Incorrect universe " ++ @@ -451,17 +456,30 @@ let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = let array_min nmr a = if Int.equal nmr 0 then 0 else Array.fold_left (fun k (nmri,_) -> min k nmri) nmr a -(* The recursive function that checks positivity and builds the list - of recursive arguments *) +(** [check_positivity_one ienv hyps (mind,i) nargs lcnames indlc] + checks the positivity of the [i]-th member of the mutually + inductive definition [mind]. It returns an [Rtree.t] which + represents the position of the recursive calls of inductive in [i] + for use by the guard condition (terms at these positions are + considered sub-terms) as well as the number of of non-uniform + arguments (used to generate induction schemes, so a priori less + relevant to the kernel). *) let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc = let lparams = rel_context_length hyps in let nmr = rel_context_nhyps hyps in - (* Checking the (strict) positivity of a constructor argument type [c] *) + (** Positivity of one argument [c] of a constructor (i.e. the + constructor [cn] has a type of the shape [… -> c … -> P], where, + more generally, the arrows may be dependent). *) let rec check_pos (env, n, ntypes, ra_env as ienv) nmr c = let x,largs = decompose_app (whd_betadeltaiota env c) in match kind_of_term x with | Prod (na,b,d) -> let () = assert (List.is_empty largs) in + (** If one of the inductives of the mutually inductive + block occurs in the left-hand side of a product, then + such an occurrence is a non-strictly-positive + recursive call. Occurrences in the right-hand side of + the product must be strictly positive.*) (match weaker_noccur_between env n ntypes b with None -> failwith_non_pos_list n ntypes [b] | Some b -> @@ -474,21 +492,35 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname Mrec _ -> compute_rec_par ienv hyps nmr largs | _ -> nmr) in + (** The case where one of the inductives of the mutually + inductive block occurs as an argument of another is not + known to be safe. So Coq rejects it. *) if not (List.for_all (noccur_between n ntypes) largs) then failwith_non_pos_list n ntypes largs else (nmr1,rarg) with Failure _ | Invalid_argument _ -> (nmr,mk_norec)) | Ind ind_kn -> - (* If the inductive type being defined appears in a - parameter, then we have a nested indtype *) + (** If one of the inductives of the mutually inductive + block being defined appears in a parameter, then we + have a nested inductive type. The positivity is then + discharged to the [check_positive_nested] function. *) if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec) else check_positive_nested ienv nmr (ind_kn, largs) | err -> + (** If an inductive of the mutually inductive block + appears in any other way, then the positivy check gives + up. *) if noccur_between n ntypes x && List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec) else failwith_non_pos_list n ntypes (x::largs) + (** [check_positive_nested] handles the case of nested inductive + calls, that is, when an inductive types from the mutually + inductive block is called as an argument of an inductive types + (for the moment, this inductive type must be a previously + defined types, not one of the types of the mutually inductive + block being defined). *) (* accesses to the environment are not factorised, but is it worth? *) and check_positive_nested (env,n,ntypes,ra_env as ienv) nmr ((mi,u), largs) = let (mib,mip) = lookup_mind_specif env mi in @@ -497,12 +529,13 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname let (lpar,auxlargs) = try List.chop auxnpar largs with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in - (* If the inductive appears in the args (non params) then the - definition is not positive. *) + (** Inductives of the inductive block being defined are only + allowed to appear nested in the parameters of another inductive + type. Not in the proper indices. *) if not (List.for_all (noccur_between n ntypes) auxlargs) then failwith_non_pos_list n ntypes auxlargs; - (* We do not deal with imbricated mutual inductive types *) + (* Nested mutual inductive types are not supported *) let auxntyp = mib.mind_ntypes in if not (Int.equal auxntyp 1) then raise (IllFormedInd (LocalNonPos n)); (* The nested inductive type with parameters removed *) @@ -513,8 +546,11 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname (* Parameters expressed in env' *) let lpar' = List.map (lift auxntyp) lpar in let irecargs_nmr = - (* fails if the inductive type occurs non positively *) - (* with recursive parameters substituted *) + (** Checks that the "nesting" inductive type is covariant in + the relevant parameters. In other words, that the + (nested) parameters which are instantiated with + inductives of the mutually inductive block occur + positively in the types of the nested constructors. *) Array.map (function c -> let c' = hnf_prod_applist env' c lpar' in @@ -528,10 +564,14 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname in (nmr',(Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0)) - (* check the inductive types occur positively in the products of C, if - check_head=true, also check the head corresponds to a constructor of - the ith type *) - + (** [check_constructors ienv check_head nmr c] checks the positivity + condition in the type [c] of a constructor (i.e. that recursive + calls to the inductives of the mutually inductive definition + appear strictly positively in each of the arguments of the + constructor, see also [check_pos]). If [check_head] is [true], + then the type of the fully applied constructor (the "head" of + the type [c]) is checked to be the right (properly applied) + inductive type. *) and check_constructors ienv check_head nmr c = let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c = let x,largs = decompose_app (whd_betadeltaiota env c) in @@ -571,6 +611,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname and nmr' = array_min nmr irecargs_nmr in (nmr', mk_paths (Mrec ind) irecargs) +(** [check_positivity kn env_ar params] checks that the mutually + inductive block [inds] is strictly positive. *) let check_positivity kn env_ar params inds = let ntypes = Array.length inds in let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in @@ -639,6 +681,7 @@ let used_section_variables env inds = keep_hyps env ids let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) +let rel_list n m = Array.to_list (rel_vect n m) exception UndefinableExpansion @@ -653,18 +696,16 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params that typechecking projections requires just a substitution and not matching with a parameter context. *) let indty, paramsletsubst = - let _, _, subst, inst = - List.fold_right - (fun (na, b, t) (i, j, subst, inst) -> - match b with - | None -> (i-1, j-1, mkRel i :: subst, mkRel j :: inst) - | Some b -> (i, j-1, substl subst b :: subst, inst)) - paramslet (nparamargs, List.length paramslet, [], []) - in + (* [ty] = [Ind inst] is typed in context [params] *) + let inst = extended_rel_vect 0 paramslet in + let ty = mkApp (mkIndU indu, inst) in + (* [Ind inst] is typed in context [params-wo-let] *) + let inst' = rel_list 0 nparamargs in + (* {params-wo-let |- subst:params] *) + let subst = subst_of_rel_context_instance paramslet inst' in + (* {params-wo-let, x:Ind inst' |- subst':(params,x:Ind inst)] *) let subst = (* For the record parameter: *) - mkRel 1 :: List.map (lift 1) subst - in - let ty = mkApp (mkIndU indu, CArray.rev_of_list inst) in + mkRel 1 :: List.map (lift 1) subst in ty, subst in let ci = diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 1f8706652..632b4daea 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -270,18 +270,6 @@ let type_of_constructors (ind,u) (mib,mip) = (* Type of case predicates *) -let local_rels ctxt = - let (rels,_) = - Context.fold_rel_context_reverse - (fun (rels,n) (_,copt,_) -> - match copt with - None -> (mkRel n :: rels, n+1) - | Some _ -> (rels, n+1)) - ~init:([],1) - ctxt - in - rels - (* Get type of inductive, with parameters instantiated *) let inductive_sort_family mip = @@ -304,14 +292,6 @@ let is_primitive_record (mib,_) = | Some (Some _) -> true | _ -> false -let extended_rel_list n hyps = - let rec reln l p = function - | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps - | (_,Some _,_) :: hyps -> reln l (p+1) hyps - | [] -> l - in - reln [] 1 hyps - let build_dependent_inductive ind (_,mip) params = let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in applist @@ -369,22 +349,22 @@ let is_correct_arity env c pj ind specif params = let build_branches_type (ind,u) (_,mip as specif) params p = let build_one_branch i cty = let typi = full_constructor_instantiate (ind,u,specif,params) cty in - let (args,ccl) = decompose_prod_assum typi in - let nargs = rel_context_length args in + let (cstrsign,ccl) = decompose_prod_assum typi in + let nargs = rel_context_length cstrsign in let (_,allargs) = decompose_app ccl in let (lparams,vargs) = List.chop (inductive_params specif) allargs in let cargs = let cstr = ith_constructor_of_inductive ind (i+1) in - let dep_cstr = applist (mkConstructU (cstr,u),lparams@(local_rels args)) in + let dep_cstr = applist (mkConstructU (cstr,u),lparams@(extended_rel_list 0 cstrsign)) in vargs @ [dep_cstr] in - let base = betazeta_appvect mip.mind_nrealdecls (lift nargs p) (Array.of_list cargs) in - it_mkProd_or_LetIn base args in + let base = lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in + it_mkProd_or_LetIn base cstrsign in Array.mapi build_one_branch mip.mind_nf_lc (* [p] is the predicate, [c] is the match object, [realargs] is the list of real args of the inductive type *) let build_case_type env n p c realargs = - whd_betaiota env (betazeta_appvect (n+1) p (Array.of_list (realargs@[c]))) + whd_betaiota env (lambda_appvect_assum (n+1) p (Array.of_list (realargs@[c]))) let type_case_branches env (pind,largs) pj c = let specif = lookup_mind_specif env (fst pind) in diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 29fe887d7..f7220c94a 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -1,6 +1,7 @@ Names Uint31 Univ +UGraph Esubst Sorts Evar diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index bd7ee7b33..3c58e788c 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -104,7 +104,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let csti = Univ.enforce_eq_instances cus newus cst in let csta = Univ.Constraint.union csti ccst in let env' = Environ.push_context ~strict:false (Univ.UContext.make (inst, csta)) env in - let () = if not (Univ.check_constraints cst (Environ.universes env')) then + let () = if not (UGraph.check_constraints cst (Environ.universes env')) then error_incorrect_with_constraint lab in let cst = match cb.const_body with diff --git a/kernel/names.ml b/kernel/names.ml index ae2b3b638..9e4e8cd61 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -204,7 +204,7 @@ struct DirPath.to_string p ^ "." ^ s let debug_to_string (i, s, p) = - "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">" + "<"^DirPath.to_string p ^"#" ^ s ^"#"^ string_of_int i^">" let compare (x : t) (y : t) = if x == y then 0 @@ -282,6 +282,11 @@ module ModPath = struct | MPbound uid -> MBId.to_string uid | MPdot (mp,l) -> to_string mp ^ "." ^ Label.to_string l + let rec debug_to_string = function + | MPfile sl -> DirPath.to_string sl + | MPbound uid -> MBId.debug_to_string uid + | MPdot (mp,l) -> debug_to_string mp ^ "." ^ Label.to_string l + (** we compare labels first if both are MPdots *) let rec compare mp1 mp2 = if mp1 == mp2 then 0 @@ -375,12 +380,16 @@ module KerName = struct let modpath kn = kn.modpath let label kn = kn.knlabel - let to_string kn = + let to_string_gen mp_to_string kn = let dp = if DirPath.is_empty kn.dirpath then "." else "#" ^ DirPath.to_string kn.dirpath ^ "#" in - ModPath.to_string kn.modpath ^ dp ^ Label.to_string kn.knlabel + mp_to_string kn.modpath ^ dp ^ Label.to_string kn.knlabel + + let to_string kn = to_string_gen ModPath.to_string kn + + let debug_to_string kn = to_string_gen ModPath.debug_to_string kn let print kn = str (to_string kn) @@ -500,9 +509,9 @@ module KerPair = struct let print kp = str (to_string kp) let debug_to_string = function - | Same kn -> "(" ^ KerName.to_string kn ^ ")" + | Same kn -> "(" ^ KerName.debug_to_string kn ^ ")" | Dual (knu,knc) -> - "(" ^ KerName.to_string knu ^ "," ^ KerName.to_string knc ^ ")" + "(" ^ KerName.debug_to_string knu ^ "," ^ KerName.debug_to_string knc ^ ")" let debug_print kp = str (debug_to_string kp) diff --git a/kernel/names.mli b/kernel/names.mli index 7cc444375..c5a7d8f3c 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -160,6 +160,8 @@ sig module Set : Set.S with type elt = t module Map : Map.ExtS with type key = t and module Set := Set + val hcons : t -> t + end (** {6 Unique names for bound modules} *) @@ -217,6 +219,9 @@ sig val to_string : t -> string + val debug_to_string : t -> string + (** Same as [to_string], but outputs information related to debug. *) + val initial : t (** Name of the toplevel structure ([= MPfile initial_dir]) *) @@ -244,6 +249,10 @@ sig (** Display *) val to_string : t -> string + + val debug_to_string : t -> string + (** Same as [to_string], but outputs information related to debug. *) + val print : t -> Pp.std_ppcmds (** Comparisons *) diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli index 4dddb9fd3..abc9e3a3c 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.mli @@ -11,7 +11,7 @@ open Nativelambda (** This module implements the conversion test by compiling to OCaml code *) -val native_conv : conv_pb -> evars -> types conversion_function +val native_conv : conv_pb -> evars -> types kernel_conversion_function (** A conversion function parametrized by a universe comparator. Used outside of the kernel. *) diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index b2142b43c..331598d85 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -30,10 +30,6 @@ let output_dir = ".coq-native" (* Extension of genereted ml files, stored for debugging purposes *) let source_ext = ".native" -(* Global settings and utilies for interface with OCaml *) -let compiler_name = - if Dynlink.is_native then ocamlopt () else ocamlc () - let ( / ) = Filename.concat (* We have to delay evaluation of include_dirs because coqlib cannot be guessed @@ -70,14 +66,15 @@ let call_compiler ml_filename = remove link_filename; remove (f ^ ".cmi"); let args = - (if Dynlink.is_native then "-shared" else "-c") + (if Dynlink.is_native then "opt" else "ocamlc") + ::(if Dynlink.is_native then "-shared" else "-c") ::"-o"::link_filename ::"-rectypes" ::"-w"::"a" ::include_dirs @ ["-impl"; ml_filename] in - if !Flags.debug then Pp.msg_debug (Pp.str (compiler_name ^ " " ^ (String.concat " " args))); - try CUnix.sys_command compiler_name args = Unix.WEXITED 0, link_filename + if !Flags.debug then Pp.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args))); + try CUnix.sys_command (ocamlfind ()) args = Unix.WEXITED 0, link_filename with Unix.Unix_error (e,_,_) -> Pp.(msg_warning (str (Unix.error_message e))); false, link_filename diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 5f3f559a2..615b9d49b 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -45,7 +45,7 @@ type globals = { env_modtypes : module_type_body MPmap.t} type stratification = { - env_universes : universes; + env_universes : UGraph.t; env_engagement : engagement } @@ -93,7 +93,7 @@ let empty_env = { env_rel_val = []; env_nb_rel = 0; env_stratification = { - env_universes = initial_universes; + env_universes = UGraph.initial_universes; env_engagement = (PredicativeSet,StratifiedType) }; env_conv_oracle = Conv_oracle.empty; retroknowledge = Retroknowledge.initial_retroknowledge; diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 0ce0bed23..b499ac0c5 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -32,7 +32,7 @@ type globals = { env_modtypes : module_type_body MPmap.t} type stratification = { - env_universes : universes; + env_universes : UGraph.t; env_engagement : engagement } diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 939eeef5d..bf2ee2707 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -54,8 +54,7 @@ let compare_stack_shape stk1 stk2 = | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2 | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 - | ((Zcase(c1,_,_)|ZcaseT(c1,_,_,_))::s1, - (Zcase(c2,_,_)|ZcaseT(c2,_,_,_))::s2) -> + | (ZcaseT(c1,_,_,_)::s1, ZcaseT(c2,_,_,_)::s2) -> Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 @@ -89,9 +88,8 @@ let pure_stack lfts stk = let (lfx,pa) = pure_rec l a in (l, Zlfix((lfx,fx),pa)::pstk) | (ZcaseT(ci,p,br,e),(l,pstk)) -> - (l,Zlcase(ci,l,mk_clos e p,Array.map (mk_clos e) br)::pstk) - | (Zcase(ci,p,br),(l,pstk)) -> - (l,Zlcase(ci,l,p,br)::pstk)) in + (l,Zlcase(ci,l,mk_clos e p,Array.map (mk_clos e) br)::pstk)) + in snd (pure_rec lfts stk) (****************************************************************************) @@ -122,34 +120,20 @@ let whd_betadeltaiota_nolet env t = Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t | _ -> whd_val (create_clos_infos betadeltaiotanolet env) (inject t) -(* Beta *) - -let beta_appvect c v = - let rec stacklam env t stack = - match kind_of_term t, stack with - Lambda(_,_,c), arg::stacktl -> stacklam (arg::env) c stacktl - | _ -> applist (substl env t, stack) in - stacklam [] c (Array.to_list v) - -let betazeta_appvect n c v = - let rec stacklam n env t stack = - if Int.equal n 0 then applist (substl env t, stack) else - match kind_of_term t, stack with - Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl - | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack - | _ -> anomaly (Pp.str "Not enough lambda/let's") in - stacklam n [] c (Array.to_list v) - (********************************************************************) (* Conversion *) (********************************************************************) (* Conversion utility functions *) -type 'a conversion_function = env -> 'a -> 'a -> unit -type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function -type 'a universe_conversion_function = env -> Univ.universes -> 'a -> 'a -> unit -type 'a trans_universe_conversion_function = - Names.transparent_state -> 'a universe_conversion_function + +(* functions of this type are called from the kernel *) +type 'a kernel_conversion_function = env -> 'a -> 'a -> unit + +(* functions of this type can be called from outside the kernel *) +type 'a extended_conversion_function = + ?l2r:bool -> ?reds:Names.transparent_state -> env -> + ?evars:((existential->constr option) * UGraph.t) -> + 'a -> 'a -> unit exception NotConvertible exception NotConvertibleVect of int @@ -180,7 +164,7 @@ type 'a universe_state = 'a * 'a universe_compare type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b -type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints +type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints let sort_cmp_universes env pb s0 s1 (u, check) = (check.compare env pb s0 s1 u, check) @@ -235,7 +219,6 @@ let rec no_arg_available = function | Zshift _ :: stk -> no_arg_available stk | Zapp v :: stk -> Int.equal (Array.length v) 0 && no_arg_available stk | Zproj _ :: _ -> true - | Zcase _ :: _ -> true | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true @@ -248,7 +231,6 @@ let rec no_nth_arg_available n = function if n >= k then no_nth_arg_available (n-k) stk else false | Zproj _ :: _ -> true - | Zcase _ :: _ -> true | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true @@ -258,13 +240,12 @@ let rec no_case_available = function | Zshift _ :: stk -> no_case_available stk | Zapp _ :: stk -> no_case_available stk | Zproj (_,_,p) :: _ -> false - | Zcase _ :: _ -> false | ZcaseT _ :: _ -> false | Zfix _ :: _ -> true let in_whnf (t,stk) = match fterm_of t with - | (FLetIn _ | FCase _ | FCaseT _ | FApp _ + | (FLetIn _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false | FLambda _ -> no_arg_available stk | FConstruct _ -> no_case_available stk @@ -530,8 +511,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = else raise NotConvertible (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *) - | ( (FLetIn _, _) | (FCase _,_) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) - | (_, FLetIn _) | (_,FCase _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) + | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) + | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) | (FLOCKED,_) | (_,FLOCKED) ) -> assert false (* In all other cases, terms are not convertible *) @@ -556,17 +537,17 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = fold 0 cuniv else raise NotConvertible -let clos_fconv trans cv_pb l2r evars env univs t1 t2 = +let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = let reds = Closure.RedFlags.red_add_transparent betaiotazeta trans in let infos = create_clos_infos ~evars reds env in ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs let check_eq univs u u' = - if not (check_eq univs u u') then raise NotConvertible + if not (UGraph.check_eq univs u u') then raise NotConvertible let check_leq univs u u' = - if not (check_leq univs u u') then raise NotConvertible + if not (UGraph.check_leq univs u u') then raise NotConvertible let check_sort_cmp_universes env pb s0 s1 univs = match (s0,s1) with @@ -593,7 +574,7 @@ let checked_sort_cmp_universes env pb s0 s1 univs = check_sort_cmp_universes env pb s0 s1 univs; univs let check_convert_instances ~flex u u' univs = - if Univ.Instance.check_eq univs u u' then univs + if UGraph.check_eq_instances univs u u' then univs else raise NotConvertible let checked_universes = @@ -601,12 +582,12 @@ let checked_universes = compare_instances = check_convert_instances } let infer_eq (univs, cstrs as cuniv) u u' = - if Univ.check_eq univs u u' then cuniv + if UGraph.check_eq univs u u' then cuniv else univs, (Univ.enforce_eq u u' cstrs) let infer_leq (univs, cstrs as cuniv) u u' = - if Univ.check_leq univs u u' then cuniv + if UGraph.check_leq univs u u' then cuniv else let cstrs' = Univ.enforce_leq u u' cstrs in univs, cstrs' @@ -635,57 +616,35 @@ let infer_cmp_universes env pb s0 s1 univs = let infer_convert_instances ~flex u u' (univs,cstrs) = (univs, Univ.enforce_eq_instances u u' cstrs) -let inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare = +let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = { compare = infer_cmp_universes; compare_instances = infer_convert_instances } -let trans_fconv_universes reds cv_pb l2r evars env univs t1 t2 = +let gen_conv cv_pb l2r reds env evars univs t1 t2 = let b = if cv_pb = CUMUL then leq_constr_univs univs t1 t2 else eq_constr_univs univs t1 t2 in if b then () else - let _ = clos_fconv reds cv_pb l2r evars env (univs, checked_universes) t1 t2 in + let _ = clos_gen_conv reds cv_pb l2r evars env (univs, checked_universes) t1 t2 in () (* Profiling *) -let trans_fconv_universes = +let gen_conv cv_pb ?(l2r=false) ?(reds=full_transparent_state) env ?(evars=(fun _->None), universes env) = + let evars, univs = evars in if Flags.profile then - let trans_fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in - Profile.profile8 trans_fconv_universes_key trans_fconv_universes - else trans_fconv_universes - -let trans_fconv reds cv_pb l2r evars env = - trans_fconv_universes reds cv_pb l2r evars env (universes env) - -let trans_conv_cmp ?(l2r=false) conv reds = trans_fconv reds conv l2r (fun _->None) -let trans_conv ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv reds CONV l2r evars -let trans_conv_leq ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv reds CUMUL l2r evars - -let trans_conv_universes ?(l2r=false) ?(evars=fun _->None) reds = - trans_fconv_universes reds CONV l2r evars -let trans_conv_leq_universes ?(l2r=false) ?(evars=fun _->None) reds = - trans_fconv_universes reds CUMUL l2r evars + let fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in + Profile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs + else gen_conv cv_pb l2r reds env evars univs -let fconv = trans_fconv full_transparent_state +let conv = gen_conv CONV -let conv_cmp ?(l2r=false) cv_pb = fconv cv_pb l2r (fun _->None) -let conv ?(l2r=false) ?(evars=fun _->None) = fconv CONV l2r evars -let conv_leq ?(l2r=false) ?(evars=fun _->None) = fconv CUMUL l2r evars - -let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 = - Array.fold_left2_i - (fun i _ t1 t2 -> - try conv_leq ~l2r ~evars env t1 t2 - with NotConvertible -> raise (NotConvertibleVect i)) - () - v1 - v2 +let conv_leq = gen_conv CUMUL let generic_conv cv_pb ~l2r evars reds env univs t1 t2 = let (s, _) = - clos_fconv reds cv_pb l2r evars env univs t1 t2 + clos_gen_conv reds cv_pb l2r evars env univs t1 t2 in s let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = @@ -696,7 +655,7 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = if b then cstrs else let univs = ((univs, Univ.Constraint.empty), inferred_universes) in - let ((_,cstrs), _) = clos_fconv reds cv_pb l2r evars env univs t1 t2 in + let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs t1 t2 in cstrs (* Profiling *) @@ -715,18 +674,19 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta infer_conv_universes CUMUL l2r evars ts env univs t1 t2 (* This reference avoids always having to link C code with the kernel *) -let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None)) -let set_vm_conv f = vm_conv := f +let vm_conv = ref (fun cv_pb env -> + gen_conv cv_pb env ~evars:((fun _->None), universes env)) + +let set_vm_conv (f:conv_pb -> Term.types kernel_conversion_function) = vm_conv := f let vm_conv cv_pb env t1 t2 = try !vm_conv cv_pb env t1 t2 with Not_found | Invalid_argument _ -> - (Pp.msg_warning - (Pp.str "Bytecode compilation failed, falling back to default conversion"); - fconv cv_pb false (fun _->None) env t1 t2) + Pp.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion"); + gen_conv cv_pb env t1 t2 let default_conv cv_pb ?(l2r=false) env t1 t2 = - fconv cv_pb false (fun _ -> None) env t1 t2 + gen_conv cv_pb env t1 t2 let default_conv_leq = default_conv CUMUL (* @@ -739,12 +699,28 @@ let conv env t1 t2 = Profile.profile4 convleqkey conv env t1 t2;; *) +(* Application with on-the-fly reduction *) + +let beta_applist c l = + let rec app subst c l = + match kind_of_term c, l with + | Lambda(_,_,c), arg::l -> app (arg::subst) c l + | _ -> applist (substl subst c, l) in + app [] c l + +let beta_appvect c v = beta_applist c (Array.to_list v) + +let beta_app c a = beta_applist c [a] + +(* Compatibility *) +let betazeta_appvect = lambda_appvect_assum + (********************************************************************) (* Special-Purpose Reduction *) (********************************************************************) (* pseudo-reduction rule: - * [hnf_prod_app env s (Prod(_,B)) N --> B[N] + * [hnf_prod_app env (Prod(_,B)) N --> B[N] * with an HNF on the first argument to produce a product. * if this does not work, then we use the string S as part of our * error message. *) diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 0df26d627..f7a8d88c2 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -26,11 +26,11 @@ val nf_betaiota : env -> constr -> constr exception NotConvertible exception NotConvertibleVect of int -type 'a conversion_function = env -> 'a -> 'a -> unit -type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function -type 'a universe_conversion_function = env -> Univ.universes -> 'a -> 'a -> unit -type 'a trans_universe_conversion_function = - Names.transparent_state -> 'a universe_conversion_function +type 'a kernel_conversion_function = env -> 'a -> 'a -> unit +type 'a extended_conversion_function = + ?l2r:bool -> ?reds:Names.transparent_state -> env -> + ?evars:((existential->constr option) * UGraph.t) -> + 'a -> 'a -> unit type conv_pb = CONV | CUMUL @@ -45,7 +45,7 @@ type 'a universe_state = 'a * 'a universe_compare type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b -type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints +type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints val sort_cmp_universes : env -> conv_pb -> sorts -> sorts -> 'a * 'a universe_compare -> 'a * 'a universe_compare @@ -55,27 +55,12 @@ constructors. *) val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a * 'a universe_compare -> 'a * 'a universe_compare -val checked_universes : Univ.universes universe_compare -val inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare +val checked_universes : UGraph.t universe_compare +val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare -val trans_conv_cmp : ?l2r:bool -> conv_pb -> constr trans_conversion_function -val trans_conv : - ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_conversion_function -val trans_conv_leq : - ?l2r:bool -> ?evars:(existential->constr option) -> types trans_conversion_function +val conv : constr extended_conversion_function -val trans_conv_universes : - ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_universe_conversion_function -val trans_conv_leq_universes : - ?l2r:bool -> ?evars:(existential->constr option) -> types trans_universe_conversion_function - -val conv_cmp : ?l2r:bool -> conv_pb -> constr conversion_function -val conv : - ?l2r:bool -> ?evars:(existential->constr option) -> constr conversion_function -val conv_leq : - ?l2r:bool -> ?evars:(existential->constr option) -> types conversion_function -val conv_leq_vecti : - ?l2r:bool -> ?evars:(existential->constr option) -> types array conversion_function +val conv_leq : types extended_conversion_function (** These conversion functions are used by module subtyping, which needs to infer universe constraints inside the kernel *) @@ -88,23 +73,28 @@ val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> Names.transparent_state -> (constr,'a) generic_conversion_function (** option for conversion *) -val set_vm_conv : (conv_pb -> types conversion_function) -> unit -val vm_conv : conv_pb -> types conversion_function +val set_vm_conv : (conv_pb -> types kernel_conversion_function) -> unit +val vm_conv : conv_pb -> types kernel_conversion_function -val default_conv : conv_pb -> ?l2r:bool -> types conversion_function -val default_conv_leq : ?l2r:bool -> types conversion_function +val default_conv : conv_pb -> ?l2r:bool -> types kernel_conversion_function +val default_conv_leq : ?l2r:bool -> types kernel_conversion_function (************************************************************************) (** Builds an application node, reducing beta redexes it may produce. *) +val beta_applist : constr -> constr list -> constr + +(** Builds an application node, reducing beta redexes it may produce. *) val beta_appvect : constr -> constr array -> constr -(** Builds an application node, reducing the [n] first beta-zeta redexes. *) -val betazeta_appvect : int -> constr -> constr array -> constr +(** Builds an application node, reducing beta redexe it may produce. *) +val beta_app : constr -> constr -> constr (** Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) val hnf_prod_applist : env -> types -> constr list -> types +(** Compatibility alias for Term.lambda_appvect_assum *) +val betazeta_appvect : int -> constr -> constr array -> constr (*********************************************************************** s Recognizing products and arities modulo reduction *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e0a07dcc3..f86fdfa97 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -561,6 +561,7 @@ let add_mind dir l mie senv = let add_modtype l params_mte inl senv = let mp = MPdot(senv.modpath, l) in let mtb = Mod_typing.translate_modtype senv.env mp inl params_mte in + let mtb = Declareops.hcons_module_body mtb in let senv' = add_field (l,SFBmodtype mtb) MT senv in mp, senv' @@ -581,6 +582,7 @@ let full_add_module_type mp mt senv = let add_module l me inl senv = let mp = MPdot(senv.modpath, l) in let mb = Mod_typing.translate_module senv.env mp inl me in + let mb = Declareops.hcons_module_body mb in let senv' = add_field (l,SFBmodule mb) M senv in let senv'' = if Modops.is_functor mb.mod_type then senv' diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 58f3bcdf0..a00a462e1 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -317,7 +317,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = (* Check that the given definition does not add any constraint over the expected ones, so that it can be used in place of the original. *) - if Univ.check_constraints ctx1 (Environ.universes env) then + if UGraph.check_constraints ctx1 (Environ.universes env) then cstrs, env, inst2 else error (IncompatibleConstraints ctx1) with Univ.UniverseInconsistency incon -> diff --git a/kernel/term.ml b/kernel/term.ml index 33ed25fe1..455248dd5 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -471,6 +471,36 @@ let rec to_prod n lam = | Cast (c,_,_) -> to_prod n c | _ -> errorlabstrm "to_prod" (mt ()) +let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) +let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c) + +(* Application with expected on-the-fly reduction *) + +let lambda_applist c l = + let rec app subst c l = + match kind_of_term c, l with + | Lambda(_,_,c), arg::l -> app (arg::subst) c l + | _, [] -> substl subst c + | _ -> anomaly (Pp.str "Not enough lambda's") in + app [] c l + +let lambda_appvect c v = lambda_applist c (Array.to_list v) + +let lambda_app c a = lambda_applist c [a] + +let lambda_applist_assum n c l = + let rec app n subst t l = + if Int.equal n 0 then + if l == [] then substl subst t + else anomaly (Pp.str "Not enough arguments") + else match kind_of_term t, l with + | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l + | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _ -> anomaly (Pp.str "Not enough lambda/let's") in + app n [] c l + +let lambda_appvect_assum n c v = lambda_applist_assum n c (Array.to_list v) + (* pseudo-reduction rule: * [prod_app s (Prod(_,B)) N --> B[N] * with an strip_outer_cast on the first argument to produce a product *) @@ -478,19 +508,32 @@ let rec to_prod n lam = let prod_app t n = match kind_of_term (strip_outer_cast t) with | Prod (_,_,b) -> subst1 n b - | _ -> - errorlabstrm "prod_app" - (str"Needed a product, but didn't find one" ++ fnl ()) + | _ -> anomaly (str"Needed a product, but didn't find one") +(* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *) +let prod_applist c l = + let rec app subst c l = + match kind_of_term c, l with + | Prod(_,_,c), arg::l -> app (arg::subst) c l + | _, [] -> substl subst c + | _ -> anomaly (Pp.str "Not enough prod's") in + app [] c l (* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) -let prod_appvect t nL = Array.fold_left prod_app t nL +let prod_appvect c v = prod_applist c (Array.to_list v) -(* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *) -let prod_applist t nL = List.fold_left prod_app t nL +let prod_applist_assum n c l = + let rec app n subst t l = + if Int.equal n 0 then + if l == [] then substl subst t + else anomaly (Pp.str "Not enough arguments") + else match kind_of_term t, l with + | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l + | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _ -> anomaly (Pp.str "Not enough prod/let's") in + app n [] c l -let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) -let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c) +let prod_appvect_assum n c v = prod_applist_assum n c (Array.to_list v) (*********************************) (* Other term destructors *) @@ -616,25 +659,6 @@ let decompose_lam_n_decls n = in lamdec_rec empty_rel_context n -(* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction - * gives n (casts are ignored) *) -let nb_lam = - let rec nbrec n c = match kind_of_term c with - | Lambda (_,_,c) -> nbrec (n+1) c - | Cast (c,_,_) -> nbrec n c - | _ -> n - in - nbrec 0 - -(* similar to nb_lam, but gives the number of products instead *) -let nb_prod = - let rec nbrec n c = match kind_of_term c with - | Prod (_,_,c) -> nbrec (n+1) c - | Cast (c,_,_) -> nbrec n c - | _ -> n - in - nbrec 0 - let prod_assum t = fst (decompose_prod_assum t) let prod_n_assum n t = fst (decompose_prod_n_assum n t) let strip_prod_assum t = snd (decompose_prod_assum t) diff --git a/kernel/term.mli b/kernel/term.mli index d60716410..972a67ebe 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -262,14 +262,34 @@ val to_lambda : int -> constr -> constr where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *) val to_prod : int -> constr -> constr +val it_mkLambda_or_LetIn : constr -> rel_context -> constr +val it_mkProd_or_LetIn : types -> rel_context -> types + +(** In [lambda_applist c args], [c] is supposed to have the form + [λΓ.c] with [Γ] without let-in; it returns [c] with the variables + of [Γ] instantiated by [args]. *) +val lambda_applist : constr -> constr list -> constr +val lambda_appvect : constr -> constr array -> constr + +(** In [lambda_applist_assum n c args], [c] is supposed to have the + form [λΓ.c] with [Γ] of length [m] and possibly with let-ins; it + returns [c] with the assumptions of [Γ] instantiated by [args] and + the local definitions of [Γ] expanded. *) +val lambda_applist_assum : int -> constr -> constr list -> constr +val lambda_appvect_assum : int -> constr -> constr array -> constr + (** pseudo-reduction rule *) (** [prod_appvect] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *) val prod_appvect : constr -> constr array -> constr val prod_applist : constr -> constr list -> constr -val it_mkLambda_or_LetIn : constr -> rel_context -> constr -val it_mkProd_or_LetIn : types -> rel_context -> types +(** In [prod_appvect_assum n c args], [c] is supposed to have the + form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it + returns [c] with the assumptions of [Γ] instantiated by [args] and + the local definitions of [Γ] expanded. *) +val prod_appvect_assum : int -> constr -> constr array -> constr +val prod_applist_assum : int -> constr -> constr list -> constr (** {5 Other term destructors. } *) @@ -308,13 +328,6 @@ val decompose_lam_n_assum : int -> constr -> rel_context * constr (** Idem, counting let-ins *) val decompose_lam_n_decls : int -> constr -> rel_context * constr -(** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction - gives {% $ %}n{% $ %} (casts are ignored) *) -val nb_lam : constr -> int - -(** Similar to [nb_lam], but gives the number of products instead *) -val nb_prod : constr -> int - (** Return the premisses/parameters of a type/term (let-in included) *) val prod_assum : types -> rel_context val lam_assum : constr -> rel_context @@ -436,11 +449,11 @@ val eq_constr : constr -> constr -> bool (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, application grouping and the universe constraints in [u]. *) -val eq_constr_univs : constr Univ.check_function +val eq_constr_univs : constr UGraph.check_function (** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo alpha, casts, application grouping and the universe constraints in [u]. *) -val leq_constr_univs : constr Univ.check_function +val leq_constr_univs : constr UGraph.check_function (** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and ignoring universe instances. *) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml new file mode 100644 index 000000000..9e8ffbc7f --- /dev/null +++ b/kernel/uGraph.ml @@ -0,0 +1,906 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Errors +open Util +open Univ + +(* Created in Caml by Gérard Huet for CoC 4.8 [Dec 1988] *) +(* Functional code by Jean-Christophe Filliâtre for Coq V7.0 [1999] *) +(* Extension with algebraic universes by HH for Coq V7.0 [Sep 2001] *) +(* Additional support for sort-polymorphic inductive types by HH [Mar 2006] *) +(* Support for universe polymorphism by MS [2014] *) + +(* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu Sozeau, + Pierre-Marie Pédrot, Jacques-Henri Jourdan *) + +let error_inconsistency o u v (p:explanation option) = + raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p)) + +(* Universes are stratified by a partial ordering $\le$. + Let $\~{}$ be the associated equivalence. We also have a strict ordering + $<$ between equivalence classes, and we maintain that $<$ is acyclic, + and contained in $\le$ in the sense that $[U]<[V]$ implies $U\le V$. + + At every moment, we have a finite number of universes, and we + maintain the ordering in the presence of assertions $U<V$ and $U\le V$. + + The equivalence $\~{}$ is represented by a tree structure, as in the + union-find algorithm. The assertions $<$ and $\le$ are represented by + adjacency lists. + + We use the algorithm described in the paper: + + Bender, M. A., Fineman, J. T., Gilbert, S., & Tarjan, R. E. (2011). A + new approach to incremental cycle detection and related + problems. arXiv preprint arXiv:1112.0784. + + *) + +open Universe + +module UMap = LMap + +type status = NoMark | Visited | WeakVisited | ToMerge + +(* Comparison on this type is pointer equality *) +type canonical_node = + { univ: Level.t; + ltle: bool UMap.t; (* true: strict (lt) constraint. + false: weak (le) constraint. *) + gtge: LSet.t; + rank : int; + klvl: int; + ilvl: int; + mutable status: status + } + +let big_rank = 1000000 + +(* A Level.t is either an alias for another one, or a canonical one, + for which we know the universes that are above *) + +type univ_entry = + Canonical of canonical_node + | Equiv of Level.t + +type universes = + { entries : univ_entry UMap.t; + index : int; + n_nodes : int; n_edges : int } + +type t = universes + +(** Used to cleanup universes if a traversal function is interrupted before it + has the opportunity to do it itself. *) +let unsafe_cleanup_universes g = + let iter _ n = match n with + | Equiv _ -> () + | Canonical n -> n.status <- NoMark + in + UMap.iter iter g.entries + +let rec cleanup_universes g = + try unsafe_cleanup_universes g + with e -> + (** The only way unsafe_cleanup_universes may raise an exception is when + a serious error (stack overflow, out of memory) occurs, or a signal is + sent. In this unlikely event, we relaunch the cleanup until we finally + succeed. *) + cleanup_universes g; raise e + +(* Every Level.t has a unique canonical arc representative *) + +(* Low-level function : makes u an alias for v. + Does not removes edges from n_edges, but decrements n_nodes. + u should be entered as canonical before. *) +let enter_equiv g u v = + { entries = + UMap.modify u (fun _ a -> + match a with + | Canonical n -> + n.status <- NoMark; + Equiv v + | _ -> assert false) g.entries; + index = g.index; + n_nodes = g.n_nodes - 1; + n_edges = g.n_edges } + +(* Low-level function : changes data associated with a canonical node. + Resets the mutable fields in the old record, in order to avoid breaking + invariants for other users of this record. + n.univ should already been inserted as a canonical node. *) +let change_node g n = + { g with entries = + UMap.modify n.univ + (fun _ a -> + match a with + | Canonical n' -> + n'.status <- NoMark; + Canonical n + | _ -> assert false) + g.entries } + +(* repr : universes -> Level.t -> canonical_node *) +(* canonical representative : we follow the Equiv links *) +let rec repr g u = + let a = + try UMap.find u g.entries + with Not_found -> anomaly ~label:"Univ.repr" + (str"Universe " ++ Level.pr u ++ str" undefined") + in + match a with + | Equiv v -> repr g v + | Canonical arc -> arc + +let get_prop_arc g = repr g Level.prop +let get_set_arc g = repr g Level.set +let is_set_arc u = Level.is_set u.univ +let is_prop_arc u = Level.is_prop u.univ + +exception AlreadyDeclared + +(* Reindexes the given universe, using the next available index. *) +let use_index g u = + let u = repr g u in + let g = change_node g { u with ilvl = g.index } in + assert (g.index > min_int); + { g with index = g.index - 1 } + +(* [safe_repr] is like [repr] but if the graph doesn't contain the + searched universe, we add it. *) +let rec safe_repr g u = + let rec safe_repr_rec entries u = + match UMap.find u entries with + | Equiv v -> safe_repr_rec entries v + | Canonical arc -> arc + in + try g, safe_repr_rec g.entries u + with Not_found -> + let can = + { univ = u; + ltle = UMap.empty; gtge = LSet.empty; + rank = if Level.is_small u then big_rank else 0; + klvl = 0; ilvl = 0; + status = NoMark } + in + let g = { g with + entries = UMap.add u (Canonical can) g.entries; + n_nodes = g.n_nodes + 1 } + in + let g = use_index g u in + g, repr g u + +(* Returns 1 if u is higher than v in topological order. + -1 lower + 0 if u = v *) +let topo_compare u v = + if u.klvl > v.klvl then 1 + else if u.klvl < v.klvl then -1 + else if u.ilvl > v.ilvl then 1 + else if u.ilvl < v.ilvl then -1 + else (assert (u==v); 0) + +(* Checks most of the invariants of the graph. For debugging purposes. *) +let check_universes_invariants g = + let n_edges = ref 0 in + let n_nodes = ref 0 in + UMap.iter (fun l u -> + match u with + | Canonical u -> + UMap.iter (fun v strict -> + incr n_edges; + let v = repr g v in + assert (topo_compare u v = -1); + if u.klvl = v.klvl then + assert (LSet.mem u.univ v.gtge || + LSet.exists (fun l -> u == repr g l) v.gtge)) + u.ltle; + LSet.iter (fun v -> + let v = repr g v in + assert (v.klvl = u.klvl && + (UMap.mem u.univ v.ltle || + UMap.exists (fun l _ -> u == repr g l) v.ltle)) + ) u.gtge; + assert (u.status = NoMark); + assert (Level.equal l u.univ); + assert (u.ilvl > g.index); + assert (not (UMap.mem u.univ u.ltle)); + incr n_nodes + | Equiv _ -> assert (not (Level.is_small l))) + g.entries; + assert (!n_edges = g.n_edges); + assert (!n_nodes = g.n_nodes) + +let clean_ltle g ltle = + UMap.fold (fun u strict acc -> + let uu = (repr g u).univ in + if Level.equal uu u then acc + else ( + let acc = UMap.remove u (fst acc) in + if not strict && UMap.mem uu acc then (acc, true) + else (UMap.add uu strict acc, true))) + ltle (ltle, false) + +let clean_gtge g gtge = + LSet.fold (fun u acc -> + let uu = (repr g u).univ in + if Level.equal uu u then acc + else LSet.add uu (LSet.remove u (fst acc)), true) + gtge (gtge, false) + +(* [get_ltle] and [get_gtge] return ltle and gtge arcs. + Moreover, if one of these lists is dirty (e.g. points to a + non-canonical node), these functions clean this node in the + graph by removing some duplicate edges *) +let get_ltle g u = + let ltle, chgt_ltle = clean_ltle g u.ltle in + if not chgt_ltle then u.ltle, u, g + else + let sz = UMap.cardinal u.ltle in + let sz2 = UMap.cardinal ltle in + let u = { u with ltle } in + let g = change_node g u in + let g = { g with n_edges = g.n_edges + sz2 - sz } in + u.ltle, u, g + +let get_gtge g u = + let gtge, chgt_gtge = clean_gtge g u.gtge in + if not chgt_gtge then u.gtge, u, g + else + let u = { u with gtge } in + let g = change_node g u in + u.gtge, u, g + +(* [revert_graph] rollbacks the changes made to mutable fields in + nodes in the graph. + [to_revert] contains the touched nodes. *) +let revert_graph to_revert g = + List.iter (fun t -> + match UMap.find t g.entries with + | Equiv _ -> () + | Canonical t -> + t.status <- NoMark) to_revert + +exception AbortBackward of universes +exception CycleDetected + +(* Implementation of the algorithm described in § 5.1 of the following paper: + + Bender, M. A., Fineman, J. T., Gilbert, S., & Tarjan, R. E. (2011). A + new approach to incremental cycle detection and related + problems. arXiv preprint arXiv:1112.0784. *) + +(* [delta] is the timeout for backward search. It might be + usefull to tune a multiplicative constant. *) +let get_delta g = + int_of_float + (min (float_of_int g.n_edges ** 0.5) + (float_of_int g.n_nodes ** (2./.3.))) + +let rec backward_traverse to_revert b_traversed count g x = + let x = repr g x in + let count = count - 1 in + if count < 0 then begin + revert_graph to_revert g; + raise (AbortBackward g) + end; + if x.status = NoMark then begin + x.status <- Visited; + let to_revert = x.univ::to_revert in + let gtge, x, g = get_gtge g x in + let to_revert, b_traversed, count, g = + LSet.fold (fun y (to_revert, b_traversed, count, g) -> + backward_traverse to_revert b_traversed count g y) + gtge (to_revert, b_traversed, count, g) + in + to_revert, x.univ::b_traversed, count, g + end + else to_revert, b_traversed, count, g + +let rec forward_traverse f_traversed g v_klvl x y = + let y = repr g y in + if y.klvl < v_klvl then begin + let y = { y with klvl = v_klvl; + gtge = if x == y then LSet.empty + else LSet.singleton x.univ } + in + let g = change_node g y in + let ltle, y, g = get_ltle g y in + let f_traversed, g = + UMap.fold (fun z _ (f_traversed, g) -> + forward_traverse f_traversed g v_klvl y z) + ltle (f_traversed, g) + in + y.univ::f_traversed, g + end else if y.klvl = v_klvl && x != y then + let g = change_node g + { y with gtge = LSet.add x.univ y.gtge } in + f_traversed, g + else f_traversed, g + +let rec find_to_merge to_revert g x v = + let x = repr g x in + match x.status with + | Visited -> false, to_revert | ToMerge -> true, to_revert + | NoMark -> + let to_revert = x::to_revert in + if Level.equal x.univ v then + begin x.status <- ToMerge; true, to_revert end + else + begin + let merge, to_revert = LSet.fold + (fun y (merge, to_revert) -> + let merge', to_revert = find_to_merge to_revert g y v in + merge' || merge, to_revert) x.gtge (false, to_revert) + in + x.status <- if merge then ToMerge else Visited; + merge, to_revert + end + | _ -> assert false + +let get_new_edges g to_merge = + (* Computing edge sets. *) + let to_merge_lvl = + List.fold_left (fun acc u -> UMap.add u.univ u acc) + UMap.empty to_merge + in + let ltle = + UMap.fold (fun _ n acc -> + UMap.merge (fun _ strict1 strict2 -> + match strict1, strict2 with + | Some true, _ | _, Some true -> Some true + | _, _ -> Some false) + acc n.ltle) + to_merge_lvl UMap.empty + in + let ltle, _ = clean_ltle g ltle in + let ltle = + UMap.merge (fun _ a strict -> + match a, strict with + | Some _, Some true -> + (* There is a lt edge inside the new component. This is a + "bad cycle". *) + raise CycleDetected + | Some _, Some false -> None + | _, _ -> strict + ) to_merge_lvl ltle + in + let gtge = + UMap.fold (fun _ n acc -> LSet.union acc n.gtge) + to_merge_lvl LSet.empty + in + let gtge, _ = clean_gtge g gtge in + let gtge = LSet.diff gtge (UMap.domain to_merge_lvl) in + (ltle, gtge) + + +let reorder g u v = + (* STEP 1: backward search in the k-level of u. *) + let delta = get_delta g in + + (* [v_klvl] is the chosen future level for u, v and all + traversed nodes. *) + let b_traversed, v_klvl, g = + try + let to_revert, b_traversed, _, g = backward_traverse [] [] delta g u in + revert_graph to_revert g; + let v_klvl = (repr g u).klvl in + b_traversed, v_klvl, g + with AbortBackward g -> + (* Backward search was too long, use the next k-level. *) + let v_klvl = (repr g u).klvl + 1 in + [], v_klvl, g + in + let f_traversed, g = + (* STEP 2: forward search. Contrary to what is described in + the paper, we do not test whether v_klvl = u.klvl nor we assign + v_klvl to v.klvl. Indeed, the first call to forward_traverse + will do all that. *) + forward_traverse [] g v_klvl (repr g v) v + in + + (* STEP 3: merge nodes if needed. *) + let to_merge, b_reindex, f_reindex = + if (repr g u).klvl = v_klvl then + begin + let merge, to_revert = find_to_merge [] g u v in + let r = + if merge then + List.filter (fun u -> u.status = ToMerge) to_revert, + List.filter (fun u -> (repr g u).status <> ToMerge) b_traversed, + List.filter (fun u -> (repr g u).status <> ToMerge) f_traversed + else [], b_traversed, f_traversed + in + List.iter (fun u -> u.status <- NoMark) to_revert; + r + end + else [], b_traversed, f_traversed + in + let to_reindex, g = + match to_merge with + | [] -> List.rev_append f_reindex b_reindex, g + | n0::q0 -> + (* Computing new root. *) + let root, rank_rest = + List.fold_left (fun ((best, rank_rest) as acc) n -> + if n.rank >= best.rank then n, best.rank else acc) + (n0, min_int) q0 + in + let ltle, gtge = get_new_edges g to_merge in + (* Inserting the new root. *) + let g = change_node g + { root with ltle; gtge; + rank = max root.rank (rank_rest + 1); } + in + + (* Inserting shortcuts for old nodes. *) + let g = List.fold_left (fun g n -> + if Level.equal n.univ root.univ then g else enter_equiv g n.univ root.univ) + g to_merge + in + + (* Updating g.n_edges *) + let oldsz = + List.fold_left (fun sz u -> sz+UMap.cardinal u.ltle) + 0 to_merge + in + let sz = UMap.cardinal ltle in + let g = { g with n_edges = g.n_edges + sz - oldsz } in + + (* Not clear in the paper: we have to put the newly + created component just between B and F. *) + List.rev_append f_reindex (root.univ::b_reindex), g + + in + + (* STEP 4: reindex traversed nodes. *) + List.fold_left use_index g to_reindex + +(* Assumes [u] and [v] are already in the graph. *) +(* Does NOT assume that ucan != vcan. *) +let insert_edge strict ucan vcan g = + try + let u = ucan.univ and v = vcan.univ in + (* do we need to reorder nodes ? *) + let g = if topo_compare ucan vcan <= 0 then g else reorder g u v in + + (* insert the new edge in the graph. *) + let u = repr g u in + let v = repr g v in + if u == v then + if strict then raise CycleDetected else g + else + let g = + try let oldstrict = UMap.find v.univ u.ltle in + if strict && not oldstrict then + change_node g { u with ltle = UMap.add v.univ true u.ltle } + else g + with Not_found -> + { (change_node g { u with ltle = UMap.add v.univ strict u.ltle }) + with n_edges = g.n_edges + 1 } + in + if u.klvl <> v.klvl || LSet.mem u.univ v.gtge then g + else + let v = { v with gtge = LSet.add u.univ v.gtge } in + change_node g v + with + | CycleDetected as e -> raise e + | e -> + (** Unlikely event: fatal error or signal *) + let () = cleanup_universes g in + raise e + +let add_universe vlev strict g = + try + let _arcv = UMap.find vlev g.entries in + raise AlreadyDeclared + with Not_found -> + assert (g.index > min_int); + let v = { + univ = vlev; + ltle = LMap.empty; + gtge = LSet.empty; + rank = 0; + klvl = 0; + ilvl = g.index; + status = NoMark; + } + in + let entries = UMap.add vlev (Canonical v) g.entries in + let g = { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges } in + insert_edge strict (get_set_arc g) v g + +exception Found_explanation of explanation + +let get_explanation strict u v g = + let v = repr g v in + let visited_strict = ref UMap.empty in + let rec traverse strict u = + if u == v then + if strict then None else Some [] + else if topo_compare u v = 1 then None + else + let visited = + try not (UMap.find u.univ !visited_strict) || strict + with Not_found -> false + in + if visited then None + else begin + visited_strict := UMap.add u.univ strict !visited_strict; + try + UMap.iter (fun u' strictu' -> + match traverse (strict && not strictu') (repr g u') with + | None -> () + | Some exp -> + let typ = if strictu' then Lt else Le in + raise (Found_explanation ((typ, make u') :: exp))) + u.ltle; + None + with Found_explanation exp -> Some exp + end + in + let u = repr g u in + if u == v then [(Eq, make v.univ)] + else match traverse strict u with Some exp -> exp | None -> assert false + +let get_explanation strict u v g = + if !Flags.univ_print then Some (get_explanation strict u v g) + else None + +(* To compare two nodes, we simply do a forward search. + We implement two improvements: + - we ignore nodes that are higher than the destination; + - we do a BFS rather than a DFS because we expect to have a short + path (typically, the shortest path has length 1) +*) +exception Found of canonical_node list +let search_path strict u v g = + let rec loop to_revert todo next_todo = + match todo, next_todo with + | [], [] -> to_revert (* No path found *) + | [], _ -> loop to_revert next_todo [] + | (u, strict)::todo, _ -> + if u.status = Visited || (u.status = WeakVisited && strict) + then loop to_revert todo next_todo + else + let to_revert = + if u.status = NoMark then u::to_revert else to_revert + in + u.status <- if strict then WeakVisited else Visited; + if try UMap.find v.univ u.ltle || not strict + with Not_found -> false + then raise (Found to_revert) + else + begin + let next_todo = + UMap.fold (fun u strictu next_todo -> + let strict = not strictu && strict in + let u = repr g u in + if u == v && not strict then raise (Found to_revert) + else if topo_compare u v = 1 then next_todo + else (u, strict)::next_todo) + u.ltle next_todo + in + loop to_revert todo next_todo + end + in + if u == v then not strict + else + try + let res, to_revert = + try false, loop [] [u, strict] [] + with Found to_revert -> true, to_revert + in + List.iter (fun u -> u.status <- NoMark) to_revert; + res + with e -> + (** Unlikely event: fatal error or signal *) + let () = cleanup_universes g in + raise e + +(** Uncomment to debug the cycle detection algorithm. *) +(*let insert_edge strict ucan vcan g = + check_universes_invariants g; + let g = insert_edge strict ucan vcan g in + check_universes_invariants g; + let ucan = repr g ucan.univ in + let vcan = repr g vcan.univ in + assert (search_path strict ucan vcan g); + g*) + +(** First, checks on universe levels *) + +let check_equal g u v = + let arcu = repr g u and arcv = repr g v in + arcu == arcv + +let check_eq_level g u v = u == v || check_equal g u v + +let check_smaller g strict u v = + let arcu = repr g u and arcv = repr g v in + if strict then + search_path true arcu arcv g + else + is_prop_arc arcu + || (is_set_arc arcu && not (is_prop_arc arcv)) + || search_path false arcu arcv g + +(** Then, checks on universes *) + +type 'a check_function = universes -> 'a -> 'a -> bool + +let check_equal_expr g x y = + x == y || (let (u, n) = x and (v, m) = y in + Int.equal n m && check_equal g u v) + +let check_eq_univs g l1 l2 = + let f x1 x2 = check_equal_expr g x1 x2 in + let exists x1 l = Universe.exists (fun x2 -> f x1 x2) l in + Universe.for_all (fun x1 -> exists x1 l2) l1 + && Universe.for_all (fun x2 -> exists x2 l1) l2 + +let check_eq g u v = + Universe.equal u v || check_eq_univs g u v + +let check_smaller_expr g (u,n) (v,m) = + let diff = n - m in + match diff with + | 0 -> check_smaller g false u v + | 1 -> check_smaller g true u v + | x when x < 0 -> check_smaller g false u v + | _ -> false + +let exists_bigger g ul l = + Universe.exists (fun ul' -> + check_smaller_expr g ul ul') l + +let real_check_leq g u v = + Universe.for_all (fun ul -> exists_bigger g ul v) u + +let check_leq g u v = + Universe.equal u v || + is_type0m_univ u || + check_eq_univs g u v || real_check_leq g u v + +(* enforc_univ_eq g u v will force u=v if possible, will fail otherwise *) + +let rec enforce_univ_eq u v g = + let ucan = repr g u in + let vcan = repr g v in + if topo_compare ucan vcan = 1 then enforce_univ_eq v u g + else + let g = insert_edge false ucan vcan g in (* Cannot fail *) + try insert_edge false vcan ucan g + with CycleDetected -> + error_inconsistency Eq v u (get_explanation true u v g) + +(* enforce_univ_leq g u v will force u<=v if possible, will fail otherwise *) +let enforce_univ_leq u v g = + let ucan = repr g u in + let vcan = repr g v in + try insert_edge false ucan vcan g + with CycleDetected -> + error_inconsistency Le u v (get_explanation true v u g) + +(* enforce_univ_lt u v will force u<v if possible, will fail otherwise *) +let enforce_univ_lt u v g = + let ucan = repr g u in + let vcan = repr g v in + try insert_edge true ucan vcan g + with CycleDetected -> + error_inconsistency Lt u v (get_explanation false v u g) + +let empty_universes = + let set_arc = Canonical { + univ = Level.set; + ltle = LMap.empty; + gtge = LSet.empty; + rank = big_rank; + klvl = 0; + ilvl = (-1); + status = NoMark; + } in + let prop_arc = Canonical { + univ = Level.prop; + ltle = LMap.empty; + gtge = LSet.empty; + rank = big_rank; + klvl = 0; + ilvl = 0; + status = NoMark; + } in + let entries = UMap.add Level.set set_arc (UMap.singleton Level.prop prop_arc) in + let empty = { entries; index = (-2); n_nodes = 2; n_edges = 0 } in + enforce_univ_lt Level.prop Level.set empty + +(* Prop = Set is forbidden here. *) +let initial_universes = empty_universes + +let is_initial_universes g = UMap.equal (==) g.entries initial_universes.entries + +let enforce_constraint cst g = + match cst with + | (u,Lt,v) -> enforce_univ_lt u v g + | (u,Le,v) -> enforce_univ_leq u v g + | (u,Eq,v) -> enforce_univ_eq u v g + +let merge_constraints c g = + Constraint.fold enforce_constraint c g + +let check_constraint g (l,d,r) = + match d with + | Eq -> check_equal g l r + | Le -> check_smaller g false l r + | Lt -> check_smaller g true l r + +let check_constraints c g = + Constraint.for_all (check_constraint g) c + +(* Normalization *) + +let lookup_level u g = + try Some (UMap.find u g) with Not_found -> None + +(** [normalize_universes g] returns a graph where all edges point + directly to the canonical representent of their target. The output + graph should be equivalent to the input graph from a logical point + of view, but optimized. We maintain the invariant that the key of + a [Canonical] element is its own name, by keeping [Equiv] edges. *) +let normalize_universes g = + let g = + { g with + entries = UMap.map (fun entry -> + match entry with + | Equiv u -> Equiv ((repr g u).univ) + | Canonical ucan -> Canonical { ucan with rank = 1 }) + g.entries } + in + UMap.fold (fun _ u g -> + match u with + | Equiv u -> g + | Canonical u -> + let _, u, g = get_ltle g u in + let _, _, g = get_gtge g u in + g) + g.entries g + +let constraints_of_universes g = + let constraints_of u v acc = + match v with + | Canonical {univ=u; ltle} -> + UMap.fold (fun v strict acc-> + let typ = if strict then Lt else Le in + Constraint.add (u,typ,v) acc) ltle acc + | Equiv v -> Constraint.add (u,Eq,v) acc + in + UMap.fold constraints_of g.entries Constraint.empty + +let constraints_of_universes g = + constraints_of_universes (normalize_universes g) + +(** [sort_universes g] builds a totally ordered universe graph. The + output graph should imply the input graph (and the implication + will be strict most of the time), but is not necessarily minimal. + Moreover, it adds levels [Type.n] to identify universes at level + n. An artificial constraint Set < Type.2 is added to ensure that + Type.n and small universes are not merged. Note: the result is + unspecified if the input graph already contains [Type.n] nodes + (calling a module Type is probably a bad idea anyway). *) +let sort_universes g = + let cans = + UMap.fold (fun _ u l -> + match u with + | Equiv _ -> l + | Canonical can -> can :: l + ) g.entries [] + in + let cans = List.sort topo_compare cans in + let lowest_levels = + UMap.mapi (fun u _ -> if Level.is_small u then 0 else 2) + (UMap.filter + (fun _ u -> match u with Equiv _ -> false | Canonical _ -> true) + g.entries) + in + let lowest_levels = + List.fold_left (fun lowest_levels can -> + let lvl = UMap.find can.univ lowest_levels in + UMap.fold (fun u' strict lowest_levels -> + let cost = if strict then 1 else 0 in + let u' = (repr g u').univ in + UMap.modify u' (fun _ lvl0 -> max lvl0 (lvl+cost)) lowest_levels) + can.ltle lowest_levels) + lowest_levels cans + in + let max_lvl = UMap.fold (fun _ a b -> max a b) lowest_levels 0 in + let mp = Names.DirPath.make [Names.Id.of_string "Type"] in + let types = Array.init (max_lvl + 1) (function + | 0 -> Level.prop + | 1 -> Level.set + | n -> Level.make mp (n-2)) + in + let g = Array.fold_left (fun g u -> + let g, u = safe_repr g u in + change_node g { u with rank = big_rank }) g types + in + let g = if max_lvl >= 2 then enforce_univ_lt Level.set types.(2) g else g in + let g = + UMap.fold (fun u lvl g -> enforce_univ_eq u (types.(lvl)) g) + lowest_levels g + in + normalize_universes g + +(** Instances *) + +let check_eq_instances g t1 t2 = + let t1 = Instance.to_array t1 in + let t2 = Instance.to_array t2 in + t1 == t2 || + (Int.equal (Array.length t1) (Array.length t2) && + let rec aux i = + (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1)) + in aux 0) + +(** Pretty-printing *) + +let pr_arc prl = function + | _, Canonical {univ=u; ltle} -> + if UMap.is_empty ltle then mt () + else + prl u ++ str " " ++ + v 0 + (pr_sequence (fun (v, strict) -> + (if strict then str "< " else str "<= ") ++ prl v) + (UMap.bindings ltle)) ++ + fnl () + | u, Equiv v -> + prl u ++ str " = " ++ prl v ++ fnl () + +let pr_universes prl g = + let graph = UMap.fold (fun u a l -> (u,a)::l) g.entries [] in + prlist (pr_arc prl) graph + +(* Dumping constraints to a file *) + +let dump_universes output g = + let dump_arc u = function + | Canonical {univ=u; ltle} -> + let u_str = Level.to_string u in + UMap.iter (fun v strict -> + let typ = if strict then Lt else Le in + output typ u_str (Level.to_string v)) ltle; + | Equiv v -> + output Eq (Level.to_string u) (Level.to_string v) + in + UMap.iter dump_arc g.entries + +(** Profiling *) + +let merge_constraints = + if Flags.profile then + let key = Profile.declare_profile "merge_constraints" in + Profile.profile2 key merge_constraints + else merge_constraints +let check_constraints = + if Flags.profile then + let key = Profile.declare_profile "check_constraints" in + Profile.profile2 key check_constraints + else check_constraints + +let check_eq = + if Flags.profile then + let check_eq_key = Profile.declare_profile "check_eq" in + Profile.profile3 check_eq_key check_eq + else check_eq + +let check_leq = + if Flags.profile then + let check_leq_key = Profile.declare_profile "check_leq" in + Profile.profile3 check_leq_key check_leq + else check_leq diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli new file mode 100644 index 000000000..e95cf4d1c --- /dev/null +++ b/kernel/uGraph.mli @@ -0,0 +1,63 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Univ + +(** {6 Graphs of universes. } *) + +type t + +type universes = t + +type 'a check_function = universes -> 'a -> 'a -> bool +val check_leq : universe check_function +val check_eq : universe check_function + +(** The empty graph of universes *) +val empty_universes : universes + +(** The initial graph of universes: Prop < Set *) +val initial_universes : universes + +val is_initial_universes : universes -> bool + +val sort_universes : 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 ... } *) +(** Merge of constraints in a universes graph. + The function [merge_constraints] merges a set of constraints in a given + universes graph. It raises the exception [UniverseInconsistency] if the + constraints are not satisfiable. *) + +val enforce_constraint : univ_constraint -> universes -> universes +val merge_constraints : constraints -> universes -> universes + +val constraints_of_universes : universes -> constraints + +val check_constraint : universes -> univ_constraint -> bool +val check_constraints : constraints -> universes -> bool + +val check_eq_instances : Instance.t check_function +(** Check equality of instances w.r.t. a universe graph *) + +(** {6 Pretty-printing of universes. } *) + +val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds + +(** {6 Dumping to a file } *) + +val dump_universes : + (constraint_type -> string -> string -> unit) -> + universes -> unit diff --git a/kernel/univ.ml b/kernel/univ.ml index 2b3a2bdb1..fab0e6fb8 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -653,170 +653,6 @@ open Universe let universe_level = Universe.level -type status = Unset | SetLe | SetLt - -(* Comparison on this type is pointer equality *) -type canonical_arc = - { univ: Level.t; - lt: Level.t list; - le: Level.t list; - rank : int; - mutable status : status; - (** Guaranteed to be unset out of the [compare_neq] functions. It is used - to do an imperative traversal of the graph, ensuring a O(1) check that - a node has already been visited. Quite performance critical indeed. *) - } - -let arc_is_le arc = match arc.status with -| Unset -> false -| SetLe | SetLt -> true - -let arc_is_lt arc = match arc.status with -| Unset | SetLe -> false -| SetLt -> true - -let terminal u = {univ=u; lt=[]; le=[]; rank=0; status = Unset} - -module UMap : -sig - type key = Level.t - type +'a t - val empty : 'a t - val add : key -> 'a -> 'a t -> 'a t - val find : key -> 'a t -> 'a - val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool - val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b - val iter : (key -> 'a -> unit) -> 'a t -> unit - val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t -end = HMap.Make(Level) - -(* A Level.t is either an alias for another one, or a canonical one, - for which we know the universes that are above *) - -type univ_entry = - Canonical of canonical_arc - | Equiv of Level.t - -type universes = univ_entry UMap.t - -(** Used to cleanup universes if a traversal function is interrupted before it - has the opportunity to do it itself. *) -let unsafe_cleanup_universes g = - let iter _ arc = match arc with - | Equiv _ -> () - | Canonical arc -> arc.status <- Unset - in - UMap.iter iter g - -let rec cleanup_universes g = - try unsafe_cleanup_universes g - with e -> - (** The only way unsafe_cleanup_universes may raise an exception is when - a serious error (stack overflow, out of memory) occurs, or a signal is - sent. In this unlikely event, we relaunch the cleanup until we finally - succeed. *) - cleanup_universes g; raise e - -let enter_equiv_arc u v g = - UMap.add u (Equiv v) g - -let enter_arc ca g = - UMap.add ca.univ (Canonical ca) g - -(* Every Level.t has a unique canonical arc representative *) - -(** The graph always contains nodes for Prop and Set. *) - -let terminal_lt u v = - {(terminal u) with lt=[v]} - -let empty_universes = - let g = enter_arc (terminal Level.set) UMap.empty in - let g = enter_arc (terminal_lt Level.prop Level.set) g in - g - -(* repr : universes -> Level.t -> canonical_arc *) -(* canonical representative : we follow the Equiv links *) - -let rec repr g u = - let a = - try UMap.find u g - with Not_found -> anomaly ~label:"Univ.repr" - (str"Universe " ++ Level.pr u ++ str" undefined") - in - match a with - | Equiv v -> repr g v - | Canonical arc -> arc - -let get_prop_arc g = repr g Level.prop -let get_set_arc g = repr g Level.set -let is_set_arc u = Level.is_set u.univ -let is_prop_arc u = Level.is_prop u.univ - -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 = - let rec searchrec w = function - | [] -> w - | v :: vl -> - let arcv = repr g v in - if List.memq arcv w || arcu==arcv then - searchrec w vl - else - searchrec (arcv :: w) vl - in - searchrec [] arcu.le - - -(* between : Level.t -> canonical_arc -> canonical_arc list *) -(* between u v = { w | u<=w<=v, w canonical } *) -(* between is the most costly operation *) - -let between g arcu arcv = - (* good are all w | u <= w <= v *) - (* bad are all w | u <= w ~<= v *) - (* find good and bad nodes in {w | u <= w} *) - (* explore b u = (b or "u is good") *) - let rec explore ((good, bad, b) as input) arcu = - if List.memq arcu good then - (good, bad, true) (* b or true *) - else if List.memq arcu bad then - input (* (good, bad, b or false) *) - else - let leq = reprleq g arcu in - (* is some universe >= u good ? *) - let good, bad, b_leq = - List.fold_left explore (good, bad, false) leq - in - if b_leq then - arcu::good, bad, true (* b or true *) - else - good, arcu::bad, b (* b or false *) - in - let good,_,_ = explore ([arcv],[],false) arcu in - good -(* We assume compare(u,v) = LE with v canonical (see compare below). - In this case List.hd(between g u v) = repr u - Otherwise, between g u v = [] - *) type constraint_type = Lt | Le | Eq @@ -831,343 +667,6 @@ let constraint_type_ord c1 c2 = match c1, c2 with | Eq, Eq -> 0 | Eq, _ -> 1 -(** [fast_compare_neq] : is [arcv] in the transitive upward closure of [arcu] ? - - 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. - - We do the traversal imperatively, setting the [status] flag on visited nodes. - This ensures O(1) check, but it also requires unsetting the flag when leaving - the function. Some special care has to be taken in order to ensure we do not - recover a messed up graph at the end. This occurs in particular when the - traversal raises an exception. Even though the code below is exception-free, - OCaml may still raise random exceptions, essentially fatal exceptions or - signal handlers. Therefore we ensure the cleanup by a catch-all clause. Note - also that the use of an imperative solution does make this function - thread-unsafe. For now we do not check universes in different threads, but if - ever this is to be done, we would need some lock somewhere. - -*) - -let get_explanation strict g arcu arcv = - (* [c] characterizes whether (and how) arcv has already been related - to arcu among the lt_done,le_done universe *) - let rec cmp c to_revert lt_todo le_todo = match lt_todo, le_todo with - | [],[] -> (to_revert, c) - | (arc,p)::lt_todo, le_todo -> - if arc_is_lt arc then - cmp c to_revert lt_todo le_todo - else - let rec find lt_todo lt le = match le with - | [] -> - begin match lt with - | [] -> - let () = arc.status <- SetLt in - cmp c (arc :: to_revert) lt_todo le_todo - | u :: lt -> - let arc = repr g u in - let p = (Lt, make u) :: p in - if arc == arcv then - if strict then (to_revert, p) else (to_revert, p) - else find ((arc, p) :: lt_todo) lt le - end - | u :: le -> - let arc = repr g u in - let p = (Le, make u) :: p in - if arc == arcv then - if strict then (to_revert, p) else (to_revert, p) - else find ((arc, p) :: lt_todo) lt le - in - find lt_todo arc.lt arc.le - | [], (arc,p)::le_todo -> - 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 p to_revert [] le_todo else (to_revert, p) - else - if arc_is_le arc then - cmp c to_revert [] le_todo - else - let rec find lt_todo lt = match lt with - | [] -> - let fold accu u = - let p = (Le, make u) :: p in - let node = (repr g u, p) in - node :: accu - in - let le_new = List.fold_left fold le_todo arc.le in - let () = arc.status <- SetLe in - cmp c (arc :: to_revert) lt_todo le_new - | u :: lt -> - let arc = repr g u in - let p = (Lt, make u) :: p in - if arc == arcv then - if strict then (to_revert, p) else (to_revert, p) - else find ((arc, p) :: lt_todo) lt - in - find [] arc.lt - in - let start = (* if is_prop_arc arcu then [Le, make arcv.univ] else *) [] in - try - let (to_revert, c) = cmp start [] [] [(arcu, [])] in - (** Reset all the touched arcs. *) - let () = List.iter (fun arc -> arc.status <- Unset) to_revert in - List.rev c - with e -> - (** Unlikely event: fatal error or signal *) - let () = cleanup_universes g in - raise e - -let get_explanation strict g arcu arcv = - if !Flags.univ_print then Some (get_explanation strict g arcu arcv) - else None - -type fast_order = FastEQ | FastLT | FastLE | FastNLE - -let fast_compare_neq strict g arcu arcv = - (* [c] characterizes whether arcv has already been related - to arcu among the lt_done,le_done universe *) - let rec cmp c to_revert lt_todo le_todo = match lt_todo, le_todo with - | [],[] -> (to_revert, c) - | arc::lt_todo, le_todo -> - if arc_is_lt arc then - cmp c to_revert lt_todo le_todo - else - let () = arc.status <- SetLt in - process_lt c (arc :: to_revert) lt_todo le_todo arc.lt arc.le - | [], arc::le_todo -> - 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 FastLE to_revert [] le_todo else (to_revert, FastLE) - else - if arc_is_le arc then - cmp c to_revert [] le_todo - else - let () = arc.status <- SetLe in - process_le c (arc :: to_revert) [] le_todo arc.lt arc.le - - and process_lt c to_revert lt_todo le_todo lt le = match le with - | [] -> - begin match lt with - | [] -> cmp c to_revert lt_todo le_todo - | u :: lt -> - let arc = repr g u in - if arc == arcv then - if strict then (to_revert, FastLT) else (to_revert, FastLE) - else process_lt c to_revert (arc :: lt_todo) le_todo lt le - end - | u :: le -> - let arc = repr g u in - if arc == arcv then - if strict then (to_revert, FastLT) else (to_revert, FastLE) - else process_lt c to_revert (arc :: lt_todo) le_todo lt le - - and process_le c to_revert lt_todo le_todo lt le = match lt with - | [] -> - let fold accu u = - let node = repr g u in - node :: accu - in - let le_new = List.fold_left fold le_todo le in - cmp c to_revert lt_todo le_new - | u :: lt -> - let arc = repr g u in - if arc == arcv then - if strict then (to_revert, FastLT) else (to_revert, FastLE) - else process_le c to_revert (arc :: lt_todo) le_todo lt le - - in - try - let (to_revert, c) = cmp FastNLE [] [] [arcu] in - (** Reset all the touched arcs. *) - let () = List.iter (fun arc -> arc.status <- Unset) to_revert in - c - with e -> - (** Unlikely event: fatal error or signal *) - let () = cleanup_universes g in - raise e - -let get_explanation_strict g arcu arcv = get_explanation true g arcu arcv - -let fast_compare g arcu arcv = - if arcu == arcv then FastEQ else fast_compare_neq true g arcu arcv - -let is_leq g arcu arcv = - arcu == arcv || - (match fast_compare_neq false g arcu arcv with - | FastNLE -> false - | (FastEQ|FastLE|FastLT) -> true) - -let is_lt g arcu arcv = - if arcu == arcv then false - else - match fast_compare_neq true g arcu arcv with - | FastLT -> true - | (FastEQ|FastLE|FastNLE) -> false - -(* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ - compare(u,v) = LT or LE => compare(v,u) = NLE - compare(u,v) = NLE => compare(v,u) = NLE or LE or LT - - Adding u>=v is consistent iff compare(v,u) # LT - and then it is redundant iff compare(u,v) # NLE - Adding u>v is consistent iff compare(v,u) = NLE - and then it is redundant iff compare(u,v) = LT *) - -(** * Universe checks [check_eq] and [check_leq], used in coqchk *) - -(** First, checks on universe levels *) - -let check_equal g u v = - let arcu = repr g u and arcv = repr g v in - arcu == arcv - -let check_eq_level g u v = u == v || check_equal g u v - -let check_smaller g strict u v = - let arcu = repr g u and arcv = repr g v in - if strict then - is_lt g arcu arcv - else - is_prop_arc arcu - || (is_set_arc arcu && not (is_prop_arc arcv)) - || is_leq g arcu arcv - -(** Then, checks on universes *) - -type 'a check_function = universes -> 'a -> 'a -> bool - -let check_equal_expr g x y = - x == y || (let (u, n) = x and (v, m) = y in - Int.equal n m && check_equal g u v) - -let check_eq_univs g l1 l2 = - let f x1 x2 = check_equal_expr g x1 x2 in - let exists x1 l = Huniv.exists (fun x2 -> f x1 x2) l in - Huniv.for_all (fun x1 -> exists x1 l2) l1 - && Huniv.for_all (fun x2 -> exists x2 l1) l2 - -let check_eq g u v = - Universe.equal u v || check_eq_univs g u v - -let check_smaller_expr g (u,n) (v,m) = - let diff = n - m in - match diff with - | 0 -> check_smaller g false u v - | 1 -> check_smaller g true u v - | x when x < 0 -> check_smaller g false u v - | _ -> false - -let exists_bigger g ul l = - Huniv.exists (fun ul' -> - check_smaller_expr g ul ul') l - -let real_check_leq g u v = - Huniv.for_all (fun ul -> exists_bigger g ul v) u - -let check_leq g u v = - Universe.equal u v || - Universe.is_type0m u || - check_eq_univs g u v || real_check_leq g u v - -(** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *) - -(* setlt : Level.t -> Level.t -> reason -> unit *) -(* forces u > v *) -(* this is normally an update of u in g rather than a creation. *) -let setlt g arcu arcv = - let arcu' = {arcu with lt=arcv.univ::arcu.lt} in - enter_arc arcu' g, arcu' - -(* checks that non-redundant *) -let setlt_if (g,arcu) v = - let arcv = repr g v in - if is_lt g arcu arcv then g, arcu - else setlt g arcu arcv - -(* setleq : Level.t -> Level.t -> unit *) -(* forces u >= v *) -(* this is normally an update of u in g rather than a creation. *) -let setleq g arcu arcv = - let arcu' = {arcu with le=arcv.univ::arcu.le} in - enter_arc arcu' g, arcu' - -(* checks that non-redundant *) -let setleq_if (g,arcu) v = - let arcv = repr g v in - if is_leq g arcu arcv then g, arcu - else setleq g arcu arcv - -(* merge : Level.t -> Level.t -> unit *) -(* we assume compare(u,v) = LE *) -(* merge u v forces u ~ v with repr u as canonical repr *) -let merge g arcu arcv = - (* we find the arc with the biggest rank, and we redirect all others to it *) - let arcu, g, v = - let best_ranked (max_rank, old_max_rank, best_arc, rest) arc = - if Level.is_small arc.univ || - (arc.rank >= max_rank && not (Level.is_small best_arc.univ)) - then (arc.rank, max_rank, arc, best_arc::rest) - else (max_rank, old_max_rank, best_arc, arc::rest) - in - match between g arcu arcv with - | [] -> anomaly (str "Univ.between") - | arc::rest -> - let (max_rank, old_max_rank, best_arc, rest) = - List.fold_left best_ranked (arc.rank, min_int, arc, []) rest in - if max_rank > old_max_rank then best_arc, g, rest - else begin - (* one redirected node also has max_rank *) - let arcu = {best_arc with rank = max_rank + 1} in - arcu, enter_arc arcu g, rest - end - in - let redirect (g,w,w') arcv = - let g' = enter_equiv_arc arcv.univ arcu.univ g in - (g',List.unionq arcv.lt w,arcv.le@w') - in - let (g',w,w') = List.fold_left redirect (g,[],[]) v in - let g_arcu = (g',arcu) in - let g_arcu = List.fold_left setlt_if g_arcu w in - let g_arcu = List.fold_left setleq_if g_arcu w' in - fst g_arcu - -(* merge_disc : Level.t -> Level.t -> unit *) -(* we assume compare(u,v) = compare(v,u) = NLE *) -(* merge_disc u v forces u ~ v with repr u as canonical repr *) -let merge_disc g arc1 arc2 = - let arcu, arcv = if Level.is_small arc2.univ || arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in - let arcu, g = - if not (Int.equal arc1.rank arc2.rank) then arcu, g - else - let arcu = {arcu with rank = succ arcu.rank} in - arcu, enter_arc arcu g - in - let g' = enter_equiv_arc arcv.univ arcu.univ g in - let g_arcu = (g',arcu) in - let g_arcu = List.fold_left setlt_if g_arcu arcv.lt in - let g_arcu = List.fold_left setleq_if g_arcu arcv.le in - fst g_arcu - (* Universe inconsistency: error raised when trying to enforce a relation that would create a cycle in the graph of universes. *) @@ -1178,70 +677,10 @@ exception UniverseInconsistency of univ_inconsistency let error_inconsistency o u v (p:explanation option) = raise (UniverseInconsistency (o,make u,make v,p)) -(* enforce_univ_eq : Level.t -> Level.t -> unit *) -(* enforce_univ_eq u v will force u=v if possible, will fail otherwise *) - -let enforce_univ_eq u v g = - let arcu = repr g u and arcv = repr g v in - match fast_compare g arcu arcv with - | FastEQ -> g - | FastLT -> - let p = get_explanation_strict g arcu arcv in - error_inconsistency Eq v u p - | FastLE -> merge g arcu arcv - | FastNLE -> - (match fast_compare g arcv arcu with - | FastLT -> - let p = get_explanation_strict g arcv arcu in - error_inconsistency Eq u v p - | FastLE -> merge g arcv arcu - | FastNLE -> merge_disc g arcu arcv - | FastEQ -> anomaly (Pp.str "Univ.compare")) - -(* enforce_univ_leq : Level.t -> Level.t -> unit *) -(* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *) -let enforce_univ_leq u v g = - let arcu = repr g u and arcv = repr g v in - if is_leq g arcu arcv then g - else - match fast_compare g arcv arcu with - | FastLT -> - let p = get_explanation_strict g arcv arcu in - error_inconsistency Le u v p - | FastLE -> merge g arcv arcu - | FastNLE -> fst (setleq g arcu arcv) - | FastEQ -> anomaly (Pp.str "Univ.compare") - -(* enforce_univ_lt u v will force u<v if possible, will fail otherwise *) -let enforce_univ_lt u v g = - let arcu = repr g u and arcv = repr g v in - match fast_compare g arcu arcv with - | FastLT -> g - | FastLE -> fst (setlt g arcu arcv) - | FastEQ -> error_inconsistency Lt u v (Some [(Eq,make v)]) - | FastNLE -> - match fast_compare_neq false g arcv arcu with - FastNLE -> fst (setlt g arcu arcv) - | FastEQ -> anomaly (Pp.str "Univ.compare") - | (FastLE|FastLT) -> - let p = get_explanation false g arcv arcu in - error_inconsistency Lt u v p - -(* Prop = Set is forbidden here. *) -let initial_universes = empty_universes - -let is_initial_universes g = UMap.equal (==) g initial_universes - (* Constraints and sets of constraints. *) type univ_constraint = Level.t * constraint_type * Level.t -let enforce_constraint cst g = - match cst with - | (u,Lt,v) -> enforce_univ_lt u v g - | (u,Le,v) -> enforce_univ_leq u v g - | (u,Eq,v) -> enforce_univ_eq u v g - let pr_constraint_type op = let op_str = match op with | Lt -> " < " @@ -1276,8 +715,6 @@ end let empty_constraint = Constraint.empty let union_constraint = Constraint.union let eq_constraint = Constraint.equal -let merge_constraints c g = - Constraint.fold enforce_constraint c g type constraints = Constraint.t @@ -1378,218 +815,12 @@ let enforce_leq u v c = let enforce_leq_level u v c = if Level.equal u v then c else Constraint.add (u,Le,v) c -let check_constraint g (l,d,r) = - match d with - | Eq -> check_equal g l r - | Le -> check_smaller g false l r - | Lt -> check_smaller g true l r - -let check_constraints c g = - Constraint.for_all (check_constraint g) c - let enforce_univ_constraint (u,d,v) = match d with | Eq -> enforce_eq u v | Le -> enforce_leq u v | Lt -> enforce_leq (super u) v -(* Normalization *) - -let lookup_level u g = - try Some (UMap.find u g) with Not_found -> None - -(** [normalize_universes g] returns a graph where all edges point - directly to the canonical representent of their target. The output - graph should be equivalent to the input graph from a logical point - of view, but optimized. We maintain the invariant that the key of - a [Canonical] element is its own name, by keeping [Equiv] edges - (see the assertion)... I (Stéphane Glondu) am not sure if this - plays a role in the rest of the module. *) -let normalize_universes g = - let rec visit u arc cache = match lookup_level u cache with - | Some x -> x, cache - | None -> match Lazy.force arc with - | None -> - u, UMap.add u u cache - | Some (Canonical {univ=v; lt=_; le=_}) -> - v, UMap.add u v cache - | Some (Equiv v) -> - let v, cache = visit v (lazy (lookup_level v g)) cache in - v, UMap.add u v cache - in - let cache = UMap.fold - (fun u arc cache -> snd (visit u (Lazy.lazy_from_val (Some arc)) cache)) - g UMap.empty - in - let repr x = UMap.find x cache in - let lrepr us = List.fold_left - (fun e x -> LSet.add (repr x) e) LSet.empty us - in - let canonicalize u = function - | Equiv _ -> Equiv (repr u) - | Canonical {univ=v; lt=lt; le=le; rank=rank} -> - assert (u == v); - (* avoid duplicates and self-loops *) - let lt = lrepr lt and le = lrepr le in - let le = LSet.filter - (fun x -> x != u && not (LSet.mem x lt)) le - in - LSet.iter (fun x -> assert (x != u)) lt; - Canonical { - univ = v; - lt = LSet.elements lt; - le = LSet.elements le; - rank = rank; - status = Unset; - } - in - UMap.mapi canonicalize g - -let constraints_of_universes g = - let constraints_of u v acc = - match v with - | Canonical {univ=u; lt=lt; le=le} -> - let acc = List.fold_left (fun acc v -> Constraint.add (u,Lt,v) acc) acc lt in - let acc = List.fold_left (fun acc v -> Constraint.add (u,Le,v) acc) acc le in - acc - | Equiv v -> Constraint.add (u,Eq,v) acc - in - UMap.fold constraints_of g Constraint.empty - -let constraints_of_universes g = - constraints_of_universes (normalize_universes g) - -(** Longest path algorithm. This is used to compute the minimal number of - universes required if the only strict edge would be the Lt one. This - algorithm assumes that the given universes constraints are a almost DAG, in - the sense that there may be {Eq, Le}-cycles. This is OK for consistent - universes, which is the only case where we use this algorithm. *) - -(** Adjacency graph *) -type graph = constraint_type LMap.t LMap.t - -exception Connected - -(** Check connectedness *) -let connected x y (g : graph) = - let rec connected x target seen g = - if Level.equal x target then raise Connected - else if not (LSet.mem x seen) then - let seen = LSet.add x seen in - let fold z _ seen = connected z target seen g in - let neighbours = try LMap.find x g with Not_found -> LMap.empty in - LMap.fold fold neighbours seen - else seen - in - try ignore(connected x y LSet.empty g); false with Connected -> true - -let add_edge x y v (g : graph) = - try - let neighbours = LMap.find x g in - let neighbours = LMap.add y v neighbours in - LMap.add x neighbours g - with Not_found -> - LMap.add x (LMap.singleton y v) g - -(** We want to keep the graph DAG. If adding an edge would cause a cycle, that - would necessarily be an {Eq, Le}-cycle, otherwise there would have been a - universe inconsistency. Therefore we may omit adding such a cycling edge - without changing the compacted graph. *) -let add_eq_edge x y v g = if connected y x g then g else add_edge x y v g - -(** Construct the DAG and its inverse at the same time. *) -let make_graph g : (graph * graph) = - let fold u arc accu = match arc with - | Equiv v -> - let (dir, rev) = accu in - (add_eq_edge u v Eq dir, add_eq_edge v u Eq rev) - | Canonical { univ; lt; le; } -> - let () = assert (u == univ) in - let fold_lt (dir, rev) v = (add_edge u v Lt dir, add_edge v u Lt rev) in - let fold_le (dir, rev) v = (add_eq_edge u v Le dir, add_eq_edge v u Le rev) in - (** Order is important : lt after le, because of the possible redundancy - between [le] and [lt] in a canonical arc. This way, the [lt] constraint - is the last one set, which is correct because it implies [le]. *) - let accu = List.fold_left fold_le accu le in - let accu = List.fold_left fold_lt accu lt in - accu - in - UMap.fold fold g (LMap.empty, LMap.empty) - -(** Construct a topological order out of a DAG. *) -let rec topological_fold u g rem seen accu = - let is_seen = - try - let status = LMap.find u seen in - assert status; (** If false, not a DAG! *) - true - with Not_found -> false - in - if not is_seen then - let rem = LMap.remove u rem in - let seen = LMap.add u false seen in - let neighbours = try LMap.find u g with Not_found -> LMap.empty in - let fold v _ (rem, seen, accu) = topological_fold v g rem seen accu in - let (rem, seen, accu) = LMap.fold fold neighbours (rem, seen, accu) in - (rem, LMap.add u true seen, u :: accu) - else (rem, seen, accu) - -let rec topological g rem seen accu = - let node = try Some (LMap.choose rem) with Not_found -> None in - match node with - | None -> accu - | Some (u, _) -> - let rem, seen, accu = topological_fold u g rem seen accu in - topological g rem seen accu - -(** Compute the longest path from any vertex. *) -let constraint_cost = function -| Eq | Le -> 0 -| Lt -> 1 - -(** This algorithm browses the graph in topological order, computing for each - encountered node the length of the longest path leading to it. Should be - O(|V|) or so (modulo map representation). *) -let rec flatten_graph rem (rev : graph) map mx = match rem with -| [] -> map, mx -| u :: rem -> - let prev = try LMap.find u rev with Not_found -> LMap.empty in - let fold v cstr accu = - let v_cost = LMap.find v map in - max (v_cost + constraint_cost cstr) accu - in - let u_cost = LMap.fold fold prev 0 in - let map = LMap.add u u_cost map in - flatten_graph rem rev map (max mx u_cost) - -(** [sort_universes g] builds a map from universes in [g] to natural - numbers. It outputs a graph containing equivalence edges from each - level appearing in [g] to [Type.n], and [lt] edges between the - [Type.n]s. The output graph should imply the input graph (and the - [Type.n]s. The output graph should imply the input graph (and the - implication will be strict most of the time), but is not - necessarily minimal. Note: the result is unspecified if the input - graph already contains [Type.n] nodes (calling a module Type is - probably a bad idea anyway). *) -let sort_universes orig = - let (dir, rev) = make_graph orig in - let order = topological dir dir LMap.empty [] in - let compact, max = flatten_graph order rev LMap.empty 0 in - let mp = Names.DirPath.make [Names.Id.of_string "Type"] in - let types = Array.init (max + 1) (fun n -> Level.make mp n) in - (** Old universes are made equal to [Type.n] *) - let fold u level accu = UMap.add u (Equiv types.(level)) accu in - let sorted = LMap.fold fold compact UMap.empty in - (** Add all [Type.n] nodes *) - let fold i accu u = - if i < max then - let pred = types.(i + 1) in - let arc = {univ = u; lt = [pred]; le = []; rank = 0; status = Unset; } in - UMap.add u (Canonical arc) accu - else accu - in - Array.fold_left_i fold sorted types - (* Miscellaneous functions to remove or test local univ assumed to occur in a universe *) @@ -1645,7 +876,6 @@ module Instance : sig val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds val levels : t -> LSet.t - val check_eq : t check_function end = struct type t = Level.t array @@ -1731,13 +961,6 @@ struct (* Necessary as universe instances might come from different modules and unmarshalling doesn't preserve sharing *)) - let check_eq g t1 t2 = - t1 == t2 || - (Int.equal (Array.length t1) (Array.length t2) && - let rec aux i = - (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1)) - in aux 0) - end let enforce_eq_instances x y = @@ -1993,27 +1216,6 @@ let abstract_universes poly ctx = (** Pretty-printing *) -let pr_arc prl = function - | _, Canonical {univ=u; lt=[]; le=[]} -> - mt () - | _, Canonical {univ=u; lt=lt; le=le} -> - let opt_sep = match lt, le with - | [], _ | _, [] -> mt () - | _ -> spc () - in - prl u ++ str " " ++ - v 0 - (pr_sequence (fun v -> str "< " ++ prl v) lt ++ - opt_sep ++ - pr_sequence (fun v -> str "<= " ++ prl v) le) ++ - fnl () - | u, Equiv v -> - prl u ++ str " = " ++ prl v ++ fnl () - -let pr_universes prl g = - let graph = UMap.fold (fun u a l -> (u,a)::l) g [] in - prlist (pr_arc prl) graph - let pr_constraints prl = Constraint.pr prl let pr_universe_context = UContext.pr @@ -2026,19 +1228,6 @@ let pr_universe_subst = let pr_universe_level_subst = LMap.pr (fun u -> str" := " ++ Level.pr u ++ spc ()) -(* Dumping constraints to a file *) - -let dump_universes output g = - let dump_arc u = function - | Canonical {univ=u; lt=lt; le=le} -> - let u_str = Level.to_string u in - List.iter (fun v -> output Lt u_str (Level.to_string v)) lt; - List.iter (fun v -> output Le u_str (Level.to_string v)) le - | Equiv v -> - output Eq (Level.to_string u) (Level.to_string v) - in - UMap.iter dump_arc g - module Huniverse_set = Hashcons.Make( struct @@ -2086,26 +1275,3 @@ let subst_instance_constraints = let key = Profile.declare_profile "subst_instance_constraints" in Profile.profile2 key subst_instance_constraints else subst_instance_constraints - -let merge_constraints = - if Flags.profile then - let key = Profile.declare_profile "merge_constraints" in - Profile.profile2 key merge_constraints - else merge_constraints -let check_constraints = - if Flags.profile then - let key = Profile.declare_profile "check_constraints" in - Profile.profile2 key check_constraints - else check_constraints - -let check_eq = - if Flags.profile then - let check_eq_key = Profile.declare_profile "check_eq" in - Profile.profile3 check_eq_key check_eq - else check_eq - -let check_leq = - if Flags.profile then - let check_leq_key = Profile.declare_profile "check_leq" in - Profile.profile3 check_leq_key check_leq - else check_leq diff --git a/kernel/univ.mli b/kernel/univ.mli index c926c57bd..5682940a0 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -40,6 +40,9 @@ sig val pr : t -> Pp.std_ppcmds (** Pretty-printing *) + val to_string : t -> string + (** Debug printing *) + val var : int -> t val var_index : t -> int option @@ -115,6 +118,9 @@ sig val type1 : t (** the universe of the type of Prop/Set *) + + val exists : (Level.t * int -> bool) -> t -> bool + val for_all : (Level.t * int -> bool) -> t -> bool end type universe = Universe.t @@ -148,31 +154,6 @@ val univ_level_mem : universe_level -> universe -> bool val univ_level_rem : universe_level -> universe -> universe -> universe -(** {6 Graphs of universes. } *) - -type universes - -type 'a check_function = universes -> 'a -> 'a -> bool -val check_leq : universe check_function -val check_eq : universe check_function - -(** The empty graph of universes *) -val empty_universes : universes - -(** The initial graph of universes: Prop < Set *) -val initial_universes : universes - -val is_initial_universes : universes -> bool - -val sort_universes : 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 @@ -203,12 +184,6 @@ val enforce_leq : universe constraint_function val enforce_eq_level : universe_level constraint_function val enforce_leq_level : universe_level constraint_function -(** {6 ... } *) -(** Merge of constraints in a universes graph. - The function [merge_constraints] merges a set of constraints in a given - universes graph. It raises the exception [UniverseInconsistency] if the - constraints are not satisfiable. *) - (** Type explanation is used to decorate error messages to provide useful explanation why a given constraint is rejected. It is composed of a path of universes and relation kinds [(r1,u1);..;(rn,un)] means @@ -226,14 +201,6 @@ type univ_inconsistency = constraint_type * universe * universe * explanation op exception UniverseInconsistency of univ_inconsistency -val enforce_constraint : univ_constraint -> universes -> universes -val merge_constraints : constraints -> universes -> universes - -val constraints_of_universes : universes -> constraints - -val check_constraint : universes -> univ_constraint -> bool -val check_constraints : constraints -> universes -> bool - (** {6 Support for universe polymorphism } *) (** Polymorphic maps from universe levels to 'a *) @@ -309,8 +276,6 @@ sig val levels : t -> LSet.t (** The set of levels in the instance *) - val check_eq : t check_function - (** Check equality of instances w.r.t. a universe graph *) end type universe_instance = Instance.t @@ -428,7 +393,6 @@ val instantiate_univ_constraints : universe_instance -> universe_context -> cons (** {6 Pretty-printing of universes. } *) -val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds val pr_constraint_type : constraint_type -> Pp.std_ppcmds val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds @@ -439,12 +403,6 @@ val explain_universe_inconsistency : (Level.t -> Pp.std_ppcmds) -> val pr_universe_level_subst : universe_level_subst -> Pp.std_ppcmds val pr_universe_subst : universe_subst -> Pp.std_ppcmds -(** {6 Dumping to a file } *) - -val dump_universes : - (constraint_type -> string -> string -> unit) -> - universes -> unit - (** {6 Hash-consing } *) val hcons_univ : universe -> universe diff --git a/kernel/vars.ml b/kernel/vars.ml index a800e2531..a00c7036f 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -151,6 +151,11 @@ let make_subst = function done; subst +(* The type of substitutions, with term substituting most recent + binder at the head *) + +type substl = Constr.t list + let substnl laml n c = substn_many (make_subst laml) n c let substl laml c = substn_many (make_subst laml) 0 c let subst1 lam c = substn_many [|make_substituend lam|] 0 c @@ -159,12 +164,20 @@ let substnl_decl laml k r = map_rel_declaration (fun c -> substnl laml k c) r let substl_decl laml r = map_rel_declaration (fun c -> substnl laml 0 c) r let subst1_decl lam r = map_rel_declaration (fun c -> subst1 lam c) r -let substnl_named_decl laml k d = - map_named_declaration (fun c -> substnl laml k c) d -let substl_named_decl laml d = - map_named_declaration (fun c -> substnl laml 0 c) d -let subst1_named_decl lam d = - map_named_declaration (fun c -> subst1 lam c) d +(* Build a substitution from an instance, inserting missing let-ins *) + +let subst_of_rel_context_instance sign l = + let rec aux subst sign l = + match sign, l with + | (_,None,_)::sign', a::args' -> aux (a::subst) sign' args' + | (_,Some c,_)::sign', args' -> + aux (substl subst c :: subst) sign' args' + | [], [] -> subst + | _ -> Errors.anomaly (Pp.str "Instance and signature do not match") + in aux [] (List.rev sign) l + +let adjust_subst_to_rel_context sign l = + List.rev (subst_of_rel_context_instance sign l) (* (thin_val sigma) removes identity substitutions from sigma *) @@ -197,15 +210,10 @@ let replace_vars var_alist x = in substrec 0 x -(* -let repvarkey = Profile.declare_profile "replace_vars";; -let replace_vars vl c = Profile.profile2 repvarkey replace_vars vl c ;; -*) - -(* (subst_var str t) substitute (VAR str) by (Rel 1) in t *) +(* (subst_var str t) substitute (Var str) by (Rel 1) in t *) let subst_var str t = replace_vars [(str, Constr.mkRel 1)] t -(* (subst_vars [id1;...;idn] t) substitute (VAR idj) by (Rel j) in t *) +(* (subst_vars [id1;...;idn] t) substitute (Var idj) by (Rel j) in t *) let substn_vars p vars c = let _,subst = List.fold_left (fun (n,l) var -> ((n+1),(var,Constr.mkRel n)::l)) (p,[]) vars diff --git a/kernel/vars.mli b/kernel/vars.mli index c0fbeeb6e..a84cf0114 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -42,33 +42,87 @@ val liftn : int -> int -> constr -> constr (** [lift n c] lifts by [n] the positive indexes in [c] *) val lift : int -> constr -> constr -(** [substnl [a1;...;an] k c] substitutes in parallel [a1],...,[an] +(** The type [substl] is the type of substitutions [u₁..un] of type + some context Δ and defined in some environment Γ. Typing of + substitutions is defined by: + - Γ ⊢ ∅ : ∅, + - Γ ⊢ u₁..u{_n-1} : Δ and Γ ⊢ u{_n} : An\[u₁..u{_n-1}\] implies + Γ ⊢ u₁..u{_n} : Δ,x{_n}:A{_n} + - Γ ⊢ u₁..u{_n-1} : Δ and Γ ⊢ un : A{_n}\[u₁..u{_n-1}\] implies + Γ ⊢ u₁..u{_n} : Δ,x{_n}:=c{_n}:A{_n} when Γ ⊢ u{_n} ≡ c{_n}\[u₁..u{_n-1}\] + + Note that [u₁..un] is represented as a list with [un] at the head of + the list, i.e. as [[un;...;u₁]]. *) + +type substl = constr list + +(** Let [Γ] be a context interleaving declarations [x₁:T₁..xn:Tn] + and definitions [y₁:=c₁..yp:=cp] in some context [Γ₀]. Let + [u₁..un] be an {e instance} of [Γ], i.e. an instance in [Γ₀] + of the [xi]. Then, [subst_of_rel_context_instance Γ u₁..un] + returns the corresponding {e substitution} of [Γ], i.e. the + appropriate interleaving [σ] of the [u₁..un] with the [c₁..cp], + all of them in [Γ₀], so that a derivation [Γ₀, Γ, Γ₁|- t:T] + can be instantiated into a derivation [Γ₀, Γ₁ |- t[σ]:T[σ]] using + [substnl σ |Γ₁| t]. + Note that the instance [u₁..un] is represented starting with [u₁], + as if usable in [applist] while the substitution is + represented the other way round, i.e. ending with either [u₁] or + [c₁], as if usable for [substl]. *) +val subst_of_rel_context_instance : rel_context -> constr list -> substl + +(** For compatibility: returns the substitution reversed *) +val adjust_subst_to_rel_context : rel_context -> constr list -> constr list + +(** [substnl [a₁;...;an] k c] substitutes in parallel [a₁],...,[an] for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates - accordingly indexes in [a1],...,[an] and [c] *) -val substnl : constr list -> int -> constr -> constr -val substl : constr list -> constr -> constr + accordingly indexes in [an],...,[a1] and [c]. In terms of typing, if + Γ ⊢ a{_n}..a₁ : Δ and Γ, Δ, Γ' ⊢ c : T with |Γ'|=k, then + Γ, Γ' ⊢ [substnl [a₁;...;an] k c] : [substnl [a₁;...;an] k T]. *) +val substnl : substl -> int -> constr -> constr + +(** [substl σ c] is a short-hand for [substnl σ 0 c] *) +val substl : substl -> constr -> constr + +(** [substl a c] is a short-hand for [substnl [a] 0 c] *) val subst1 : constr -> constr -> constr -val substnl_decl : constr list -> int -> rel_declaration -> rel_declaration -val substl_decl : constr list -> rel_declaration -> rel_declaration -val subst1_decl : constr -> rel_declaration -> rel_declaration +(** [substnl_decl [a₁;...;an] k Ω] substitutes in parallel [a₁], ..., [an] + for respectively [Rel(k+1)], ..., [Rel(k+n)] in [Ω]; it relocates + accordingly indexes in [a₁],...,[an] and [c]. In terms of typing, if + Γ ⊢ a{_n}..a₁ : Δ and Γ, Δ, Γ', Ω ⊢ with |Γ'|=[k], then + Γ, Γ', [substnl_decl [a₁;...;an]] k Ω ⊢. *) +val substnl_decl : substl -> int -> rel_declaration -> rel_declaration -val substnl_named_decl : constr list -> int -> named_declaration -> named_declaration -val subst1_named_decl : constr -> named_declaration -> named_declaration -val substl_named_decl : constr list -> named_declaration -> named_declaration +(** [substl_decl σ Ω] is a short-hand for [substnl_decl σ 0 Ω] *) +val substl_decl : substl -> rel_declaration -> rel_declaration +(** [subst1_decl a Ω] is a short-hand for [substnl_decl [a] 0 Ω] *) +val subst1_decl : constr -> rel_declaration -> rel_declaration + +(** [replace_vars k [(id₁,c₁);...;(idn,cn)] t] substitutes [Var idj] by + [cj] in [t]. *) val replace_vars : (Id.t * constr) list -> constr -> constr -(** (subst_var str t) substitute (VAR str) by (Rel 1) in t *) -val subst_var : Id.t -> constr -> constr -(** [subst_vars [id1;...;idn] t] substitute [VAR idj] by [Rel j] in [t] - if two names are identical, the one of least indice is kept *) -val subst_vars : Id.t list -> constr -> constr +(** [substn_vars k [id₁;...;idn] t] substitutes [Var idj] by [Rel j+k-1] in [t]. + If two names are identical, the one of least index is kept. In terms of + typing, if Γ,x{_n}:U{_n},...,x₁:U₁,Γ' ⊢ t:T, together with id{_j}:T{_j} and + Γ,x{_n}:U{_n},...,x₁:U₁,Γ' ⊢ T{_j}\[id{_j+1}..id{_n}:=x{_j+1}..x{_n}\] ≡ Uj, + then Γ\\{id₁,...,id{_n}\},x{_n}:U{_n},...,x₁:U₁,Γ' ⊢ [substn_vars + (|Γ'|+1) [id₁;...;idn] t] : [substn_vars (|Γ'|+1) [id₁;...;idn] + T]. *) -(** [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t] - if two names are identical, the one of least indice is kept *) val substn_vars : int -> Id.t list -> constr -> constr +(** [subst_vars [id1;...;idn] t] is a short-hand for [substn_vars + [id1;...;idn] 1 t]: it substitutes [Var idj] by [Rel j] in [t]. If + two names are identical, the one of least index is kept. *) +val subst_vars : Id.t list -> constr -> constr + +(** [subst_var id t] is a short-hand for [substn_vars [id] 1 t]: it + substitutes [Var id] by [Rel 1] in [t]. *) +val subst_var : Id.t -> constr -> constr + (** {3 Substitution of universes} *) open Univ diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 49e5d23e6..acf4c408f 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -12,7 +12,7 @@ open Reduction (********************************************************************** s conversion functions *) -val vm_conv : conv_pb -> types conversion_function +val vm_conv : conv_pb -> types kernel_conversion_function (** A conversion function parametrized by a universe comparator. Used outside of the kernel. *) |