diff options
-rw-r--r-- | dev/top_printers.ml | 5 | ||||
-rw-r--r-- | pretyping/cases.ml | 6 | ||||
-rw-r--r-- | pretyping/evarsolve.ml | 2 | ||||
-rw-r--r-- | pretyping/evarutil.ml | 4 | ||||
-rw-r--r-- | pretyping/evd.ml | 179 | ||||
-rw-r--r-- | pretyping/evd.mli | 24 | ||||
-rw-r--r-- | printing/printer.ml | 6 | ||||
-rw-r--r-- | proofs/goal.ml | 7 |
8 files changed, 113 insertions, 120 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index c0ef89a71..6f2c24176 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -135,8 +135,9 @@ let pr_existentialset evars = prlist_with_sep spc pr_evar (Evar.Set.elements evars) let ppexistentialset evars = pp (pr_existentialset evars) -let ppexistentialfilter filter = - pp (prlist_with_sep spc bool (Evd.Filter.repr filter)) +let ppexistentialfilter filter = match Evd.Filter.repr filter with +| None -> pp (Pp.str "ΓΈ") +| Some f -> pp (prlist_with_sep spc bool f) let ppclenv clenv = pp(pr_clenv clenv) let ppgoalgoal gl = pp(Goal.pr_goal gl) let ppgoal g = pp(Printer.pr_goal g) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index a7957ebe8..d71499eda 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1573,12 +1573,12 @@ let abstract_tycon loc env evdref subst _tycon extenv t = (fun i _ -> if Int.List.mem i vl then u else mkRel i) 1 (rel_context extenv) in let rel_filter = - Filter.init_list (fun a -> not (isRel a) || dependent a u + List.map (fun a -> not (isRel a) || dependent a u || Int.Set.mem (destRel a) depvl) inst in let named_filter = - Filter.init_list (fun (id,_,_) -> dependent (mkVar id) u) + List.map (fun (id,_,_) -> dependent (mkVar id) u) (named_context extenv) in - let filter = Filter.append rel_filter named_filter in + let filter = Filter.make (rel_filter @ named_filter) in let candidates = u :: List.map mkRel vl in let ev = e_new_evar evdref extenv ~src:(loc, Evar_kinds.CasesType) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 89a63a13c..4f982114a 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -494,7 +494,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let evd,b = define_evar_from_virtual_equation define_fun env evd b sign filter inst_in_env in evd,Some b in - (push_named_context_val (id,b_in_sign,t_in_sign) sign, Filter.cons true filter, + (push_named_context_val (id,b_in_sign,t_in_sign) sign, Filter.extend 1 filter, (mkRel 1)::(List.map (lift 1) inst_in_env), (mkRel 1)::(List.map (lift 1) inst_in_sign), push_rel d env,evd,id::avoid)) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 21a418943..1605ef7cf 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -643,7 +643,7 @@ let define_pure_evar_as_product evd evk = let evd2,rng = let newenv = push_named (id, None, dom) evenv in let src = evar_source evk evd1 in - let filter = Filter.cons true (evar_filter evi) in + let filter = Filter.extend 1 (evar_filter evi) in new_type_evar evd1 newenv ~src ~filter in let prod = mkProd (Name id, dom, subst_var id rng) in let evd3 = Evd.define evk prod evd2 in @@ -681,7 +681,7 @@ let define_pure_evar_as_lambda env evd evk = let id = next_name_away_with_default_using_types "x" na avoid (whd_evar evd dom) in let newenv = push_named (id, None, dom) evenv in - let filter = Filter.cons true (evar_filter evi) in + let filter = Filter.extend 1 (evar_filter evi) in let src = evar_source evk evd1 in let evd2,body = new_evar evd1 newenv ~src (subst1 (mkVar id) rng) ~filter in let lam = mkLambda (Name id, dom, subst_var id body) in diff --git a/pretyping/evd.ml b/pretyping/evd.ml index d6c9a2097..8fc6b8ab2 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -23,45 +23,22 @@ module Filter : sig type t val equal : t -> t -> bool - val length : t -> int - val identity : int -> t - val is_identity : t -> bool - val init : int -> (int -> bool) -> t + val identity : t val filter_list : t -> 'a list -> 'a list val filter_array : t -> 'a array -> 'a array - val cons : bool -> t -> t + val extend : int -> t -> t val compose : t -> t -> t val restrict_upon : t -> int -> (int -> bool) -> t option val map_along : (bool -> 'a -> bool) -> t -> 'a list -> t - val init_list : ('a -> bool) -> 'a list -> t - val append : t -> t -> t - val repr : t -> bool list + val make : bool list -> t + val repr : t -> bool list option end = struct - type t = bool list + type t = bool list option + (** We guarantee through the interface that if a filter is [Some _] then it + contains at least one [false] somewhere. *) - (** Most of filters we use are identities, so we share their use. *) - let identity_pool = Array.make 128 [] - - let () = - (** Fill the filter pool *) - for i = 1 to 127 do - let pred = Array.unsafe_get identity_pool (pred i) in - let curr = true :: pred in - Array.unsafe_set identity_pool i curr - done - - let rec identity_gen n accu = - if n = 0 then accu - else identity_gen (pred n) (true :: accu) - - let identity n = - if n < 128 then Array.unsafe_get identity_pool n - else - let accu = Array.unsafe_get identity_pool 127 in - identity_gen (n - 127) accu - - let length = List.length + let identity = None let rec equal l1 l2 = match l1, l2 with | [], [] -> true @@ -69,25 +46,40 @@ struct (if h1 then h2 else not h2) && equal l1 l2 | _ -> false + let equal l1 l2 = match l1, l2 with + | None, None -> true + | Some _, None | None, Some _ -> false + | Some l1, Some l2 -> equal l1 l2 + let rec is_identity = function | [] -> true | true :: l -> is_identity l | false :: _ -> false - let rec init_aux f i accu = - if i = 0 then accu - else init_aux f (pred i) (f (pred i) :: accu) + let normalize f = if is_identity f then None else Some f - let init len f = - init_aux f len [] + let filter_list f l = match f with + | None -> l + | Some f -> CList.filter_with f l - let filter_list = CList.filter_with + let filter_array f v = match f with + | None -> v + | Some f -> CArray.filter_with f v - let filter_array = CArray.filter_with + let rec extend n l = + if n = 0 then l + else extend (pred n) (true :: l) - let cons b l = b :: l + let extend n = function + | None -> None + | Some f -> Some (extend n f) - let compose = CList.filter_with + let compose f1 f2 = match f1 with + | None -> f2 + | Some f1 -> + match f2 with + | None -> None + | Some f2 -> normalize (CList.filter_with f1 f2) let apply_subfilter filter subfilter = let len = Array.length subfilter in @@ -102,16 +94,24 @@ struct let restrict_upon f len p = let newfilter = Array.init len p in - if Array.for_all (fun id -> id) newfilter then - None + if Array.for_all (fun id -> id) newfilter then None else - Some (apply_subfilter f newfilter) - - let map_along = List.map2 + (** In both cases we statically know that the argument will contain at + least one [false] *) + let nf = match f with + | None -> Some (Array.to_list newfilter) + | Some f -> Some (apply_subfilter f newfilter) + in + Some nf - let init_list = List.map + let map_along f flt l = + let ans = match flt with + | None -> List.map (fun x -> f true x) l + | Some flt -> List.map2 f flt l + in + normalize ans - let append = (@) + let make l = normalize l let repr f = f @@ -145,7 +145,7 @@ let make_evar hyps ccl = { evar_concl = ccl; evar_hyps = hyps; evar_body = Evar_empty; - evar_filter = Filter.identity (List.length (named_context_of_val hyps)); + evar_filter = Filter.identity; evar_source = (Loc.ghost,Evar_kinds.InternalHole); evar_candidates = None; evar_extra = Store.empty @@ -163,41 +163,37 @@ let evar_body evi = evi.evar_body let evar_context evi = named_context_of_val evi.evar_hyps let evar_filtered_context evi = - let filter = evar_filter evi in - if Filter.is_identity filter then evar_context evi - else Filter.filter_list (evar_filter evi) (evar_context evi) + Filter.filter_list (evar_filter evi) (evar_context evi) let evar_hyps evi = evi.evar_hyps -let evar_filtered_hyps evi = - let filter = evar_filter evi in - if Filter.is_identity filter then evar_hyps evi - else - let rec make_hyps filter ctxt = match filter, ctxt with - | [], [] -> empty_named_context_val - | false :: filter, _ :: ctxt -> make_hyps filter ctxt - | true :: filter, decl :: ctxt -> - let hyps = make_hyps filter ctxt in - push_named_context_val decl hyps - | _ -> instance_mismatch () - in - make_hyps (Filter.repr filter) (evar_context evi) +let evar_filtered_hyps evi = match Filter.repr (evar_filter evi) with +| None -> evar_hyps evi +| Some filter -> + let rec make_hyps filter ctxt = match filter, ctxt with + | [], [] -> empty_named_context_val + | false :: filter, _ :: ctxt -> make_hyps filter ctxt + | true :: filter, decl :: ctxt -> + let hyps = make_hyps filter ctxt in + push_named_context_val decl hyps + | _ -> instance_mismatch () + in + make_hyps filter (evar_context evi) let evar_env evi = Global.env_of_context evi.evar_hyps -let evar_filtered_env evi = - let filter = evar_filter evi in - if Filter.is_identity filter then evar_env evi - else - let rec make_env filter ctxt = match filter, ctxt with - | [], [] -> reset_context (Global.env ()) - | false :: filter, _ :: ctxt -> make_env filter ctxt - | true :: filter, decl :: ctxt -> - let env = make_env filter ctxt in - push_named decl env - | _ -> instance_mismatch () - in - make_env (Filter.repr filter) (evar_context evi) +let evar_filtered_env evi = match Filter.repr (evar_filter evi) with +| None -> evar_env evi +| Some filter -> + let rec make_env filter ctxt = match filter, ctxt with + | [], [] -> reset_context (Global.env ()) + | false :: filter, _ :: ctxt -> make_env filter ctxt + | true :: filter, decl :: ctxt -> + let env = make_env filter ctxt in + push_named decl env + | _ -> instance_mismatch () + in + make_env filter (evar_context evi) let eq_evar_body b1 b2 = match b1, b2 with | Evar_empty, Evar_empty -> true @@ -234,13 +230,19 @@ let make_evar_instance_array info args = | true :: filter, (id, _, _) :: ctxt -> if i < len then let c = Array.unsafe_get args i in - if isVarId id c then instrec filter ctxt (succ i) - else (id, c) :: instrec filter ctxt (succ i) + (id, c) :: instrec filter ctxt (succ i) else instance_mismatch () | _ -> instance_mismatch () in - let filter = Filter.repr (evar_filter info) in - instrec filter (evar_context info) 0 + match Filter.repr (evar_filter info) with + | None -> + let map i (id, _, _) = + if (i < len) then (id, Array.unsafe_get args i) + else instance_mismatch () + in + List.map_i map 0 (evar_context info) + | Some filter -> + instrec filter (evar_context info) 0 let instantiate_evar_array info c args = let inst = make_evar_instance_array info args in @@ -533,13 +535,11 @@ let define evk body evd = in { evd with defn_evars; undf_evars; last_mods; } -let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter ?candidates evd = - let filter = match filter with - | None -> - Filter.identity (List.length (named_context_of_val hyps)) +let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?(filter = Filter.identity) ?candidates evd = + let () = match Filter.repr filter with + | None -> () | Some filter -> - assert (Int.equal (Filter.length filter) (List.length (named_context_of_val hyps))); - filter + assert (Int.equal (List.length filter) (List.length (named_context_of_val hyps))) in let evar_info = { evar_hyps = hyps; @@ -918,7 +918,10 @@ let pr_evar_source = function let pr_evar_info evi = let phyps = try - let decls = List.combine (evar_context evi) (Filter.repr (evar_filter evi)) in + let decls = match Filter.repr (evar_filter evi) with + | None -> List.map (fun c -> (c, true)) (evar_context evi) + | Some filter -> List.combine (evar_context evi) filter + in prlist_with_sep spc pr_decl (List.rev decls) with Invalid_argument _ -> str "Ill-formed filtered context" in let pty = print_constr evi.evar_concl in diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 8f423c788..55bce05de 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -42,17 +42,8 @@ sig val equal : t -> t -> bool (** Equality over filters *) - val length : t -> int - (** Length of a filter. *) - - val identity : int -> t - (** The identity filter of the given length. *) - - val is_identity : t -> bool - (** Check whether the whole bitmask is set. *) - - val init : int -> (int -> bool) -> t - (** Create a filter with the given length and constructing function. *) + val identity : t + (** The identity filter. *) val filter_list : t -> 'a list -> 'a list (** Filter a list. Sizes must coincide. *) @@ -60,8 +51,8 @@ sig val filter_array : t -> 'a array -> 'a array (** Filter an array. Sizes must coincide. *) - val cons : bool -> t -> t - (** Extend a bitmask on the left. *) + val extend : int -> t -> t + (** [extend n f] extends [f] on the left with [n]-th times [true]. *) val compose : t -> t -> t (** Horizontal composition : [compose f1 f2] only keeps parts of [f2] where @@ -73,13 +64,10 @@ sig val map_along : (bool -> 'a -> bool) -> t -> 'a list -> t (** Apply the function on the filter and the list. Sizes must coincide. *) - val init_list : ('a -> bool) -> 'a list -> t + val make : bool list -> t (** Create out of a list *) - val append : t -> t -> t - (** Append, seen as lists *) - - val repr : t -> bool list + val repr : t -> bool list option (** Observe as a bool list. *) end diff --git a/printing/printer.ml b/printing/printer.ml index 4bab893d7..935153bff 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -356,8 +356,10 @@ let pr_concl n sigma g = (* display evar type: a context and a type *) let pr_evgl_sign gl = let ps = pr_named_context_of (evar_env gl) in - let f = Filter.repr (evar_filter gl) in - let _, l = List.filter2 (fun b c -> not b) f (evar_context gl) in + let _, l = match Filter.repr (evar_filter gl) with + | None -> [], [] + | Some f -> List.filter2 (fun b c -> not b) f (evar_context gl) + in let ids = List.rev_map pi1 l in let warn = if List.is_empty ids then mt () else diff --git a/proofs/goal.ml b/proofs/goal.ml index 64eeb69d9..ac3e593da 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -501,8 +501,7 @@ module V82 = struct let mk_goal evars hyps concl extra = let evi = { Evd.evar_hyps = hyps; Evd.evar_concl = concl; - Evd.evar_filter = Evd.Filter.identity - (List.length (Environ.named_context_of_val hyps)); + Evd.evar_filter = Evd.Filter.identity; Evd.evar_body = Evd.Evar_empty; Evd.evar_source = (Loc.ghost,Evar_kinds.GoalEvar); Evd.evar_candidates = None; @@ -558,8 +557,8 @@ module V82 = struct let hyps = evi.Evd.evar_hyps in let new_hyps = List.fold_right Environ.push_named_context_val extra_hyps hyps in - let extra_filter = Evd.Filter.identity (List.length extra_hyps) in - let new_filter = Evd.Filter.append extra_filter evi.Evd.evar_filter in + let filter = evi.Evd.evar_filter in + let new_filter = Evd.Filter.extend (List.length extra_hyps) filter in let new_evi = { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in let new_evi = Typeclasses.mark_unresolvable new_evi in |