diff options
| -rw-r--r-- | lib/cMap.ml | 14 | ||||
| -rw-r--r-- | lib/cMap.mli | 4 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 52 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 4 |
4 files changed, 42 insertions, 32 deletions
diff --git a/lib/cMap.ml b/lib/cMap.ml index bf0a33768..4c94f122a 100644 --- a/lib/cMap.ml +++ b/lib/cMap.ml @@ -19,11 +19,13 @@ sig include Map.S module Set : Set.S with type elt = key val domain : 'a t -> Set.t + val bind : (key -> 'a) -> Set.t -> 'a t end -module Domain (M : Map.OrderedType) : +module MapExt (M : Map.OrderedType) : sig val domain : 'a Map.Make(M).t -> Set.Make(M).t + val bind : (M.t -> 'a) -> Set.Make(M).t -> 'a Map.Make(M).t end = struct (** This unsafe module is a way to access to the actual implementations of @@ -50,11 +52,17 @@ struct (** This function is essentially identity, but OCaml current stdlib does not take advantage of the similarity of the two structures, so we introduce this unsafe loophole. *) - + + let rec bind f (s : set) : 'a map = match Obj.magic s with + | SEmpty -> Obj.magic MEmpty + | SNode (l, k, r, h) -> + Obj.magic (MNode (bind f l, k, f k, bind f r, h)) + (** Dual operation of [domain]. *) + end module Make(M : Map.OrderedType) = struct include Map.Make(M) - include Domain(M) + include MapExt(M) end diff --git a/lib/cMap.mli b/lib/cMap.mli index 9b7043d9e..222138828 100644 --- a/lib/cMap.mli +++ b/lib/cMap.mli @@ -27,6 +27,10 @@ sig val domain : 'a t -> Set.t (** Recover the set of keys defined in the map. *) + val bind : (key -> 'a) -> Set.t -> 'a t + (** [bind f s] transform the set [x1; ...; xn] into [x1 := f x1; ...; + xn := f xn]. *) + end module Make(M : Map.OrderedType) : ExtS with diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e86732658..ad5f5a7ae 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -782,7 +782,7 @@ let whd_meta sigma c = match kind_of_term c with * Differs from (strong whd_meta). *) let plain_instance s c = let rec irec n u = match kind_of_term u with - | Meta p -> (try lift n (List.assoc p s) with Not_found -> u) + | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u) | App (f,l) when isCast f -> let (f,_,t) = destCast f in let l' = Array.map (irec n) l in @@ -791,7 +791,7 @@ let plain_instance s c = (* Don't flatten application nodes: this is used to extract a proof-term from a proof-tree and we want to keep the structure of the proof-tree *) - (try let g = List.assoc p s in + (try let g = Metamap.find p s in match kind_of_term g with | App _ -> let h = Id.of_string "H" in @@ -800,13 +800,12 @@ let plain_instance s c = with Not_found -> mkApp (f,l')) | _ -> mkApp (irec n f,l')) | Cast (m,_,_) when isMeta m -> - (try lift n (List.assoc (destMeta m) s) with Not_found -> u) + (try lift n (Metamap.find (destMeta m) s) with Not_found -> u) | _ -> map_constr_with_binders succ irec n u in - match s with - | [] -> c - | _ -> irec 0 c + if Metamap.is_empty s then c + else irec 0 c (* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota] has (unfortunately) different subtle side effects: @@ -1041,32 +1040,32 @@ let meta_value evd mv = let rec valrec mv = match meta_opt_fvalue evd mv with | Some (b,_) -> - instance evd - (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas)) - b.rebus + let metas = Metamap.bind valrec b.freemetas in + instance evd metas b.rebus | None -> mkMeta mv in valrec mv let meta_instance sigma b = - let c_sigma = - List.map - (fun mv -> (mv,meta_value sigma mv)) (Metaset.elements b.freemetas) - in - match c_sigma with - | [] -> b.rebus - | _ -> instance sigma c_sigma b.rebus + let fm = b.freemetas in + if Metaset.is_empty fm then b.rebus + else + let c_sigma = Metamap.bind (fun mv -> meta_value sigma mv) fm in + instance sigma c_sigma b.rebus let nf_meta sigma c = meta_instance sigma (mk_freelisted c) (* Instantiate metas that create beta/iota redexes *) let meta_reducible_instance evd b = - let fm = Metaset.elements b.freemetas in - let metas = List.fold_left (fun l mv -> - match (try meta_opt_fvalue evd mv with Not_found -> None) with - | Some (g,(_,s)) -> (mv,(g.rebus,s))::l - | None -> l) [] fm in + let fm = b.freemetas in + let fold mv accu = + let fvalue = try meta_opt_fvalue evd mv with Not_found -> None in + match fvalue with + | None -> accu + | Some (g, (_, s)) -> Metamap.add mv (g.rebus, s) accu + in + let metas = Metaset.fold fold fm Metamap.empty in let rec irec u = let u = whd_betaiota Evd.empty u in match kind_of_term u with @@ -1074,7 +1073,7 @@ let meta_reducible_instance evd b = let m = destMeta (strip_outer_cast c) in (match try - let g, s = List.assoc m metas in + let g, s = Metamap.find m metas in let is_coerce = match s with CoerceToType -> true | _ -> false in if isConstruct g || not is_coerce then Some g else None with Not_found -> None @@ -1085,7 +1084,7 @@ let meta_reducible_instance evd b = let m = destMeta (strip_outer_cast f) in (match try - let g, s = List.assoc m metas in + let g, s = Metamap.find m metas in let is_coerce = match s with CoerceToType -> true | _ -> false in if isLambda g || not is_coerce then Some g else None with Not_found -> None @@ -1093,15 +1092,14 @@ let meta_reducible_instance evd b = | Some g -> irec (mkApp (g,l)) | None -> mkApp (f,Array.map irec l)) | Meta m -> - (try let g, s = List.assoc m metas in + (try let g, s = Metamap.find m metas in let is_coerce = match s with CoerceToType -> true | _ -> false in if not is_coerce then irec g else u with Not_found -> u) | _ -> map_constr irec u in - match fm with - | [] -> (* nf_betaiota? *) b.rebus - | _ -> irec b.rebus + if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus + else irec b.rebus let head_unfold_under_prod ts env _ c = diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 588914c58..b98a7d309 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -225,8 +225,8 @@ val is_trans_fconv : conv_pb -> transparent_state -> env -> evar_map -> constr (** {6 Special-Purpose Reduction Functions } *) val whd_meta : evar_map -> constr -> constr -val plain_instance : (metavariable * constr) list -> constr -> constr -val instance :evar_map -> (metavariable * constr) list -> constr -> constr +val plain_instance : constr Metamap.t -> constr -> constr +val instance : evar_map -> constr Metamap.t -> constr -> constr val head_unfold_under_prod : transparent_state -> reduction_function (** {6 Heuristic for Conversion with Evar } *) |