diff options
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 77 |
1 files changed, 44 insertions, 33 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index cfc9aa6351..2142cee374 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -8,10 +8,11 @@ open Pp open CErrors +open Sorts open Util open Names open Nameops -open Term +open Constr open Vars open Environ @@ -124,10 +125,9 @@ end (* The type of mappings for existential variables *) -module Dummy = struct end -module Store = Store.Make(Dummy) +module Store = Store.Make () -type evar = Term.existential_key +type evar = Evar.t let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk) @@ -281,9 +281,9 @@ type 'a freelisted = { (* Collects all metavars appearing in a constr *) let metavars_of c = let rec collrec acc c = - match kind_of_term c with + match kind c with | Meta mv -> Int.Set.add mv acc - | _ -> Term.fold_constr collrec acc c + | _ -> Constr.fold collrec acc c in collrec Int.Set.empty c @@ -371,17 +371,17 @@ val key : Id.t -> t -> Evar.t end = struct -type t = Id.t EvMap.t * existential_key Idmap.t +type t = Id.t EvMap.t * Evar.t Id.Map.t -let empty = (EvMap.empty, Idmap.empty) +let empty = (EvMap.empty, Id.Map.empty) let add_name_newly_undefined id evk evi (evtoid, idtoev as names) = match id with | None -> names | Some id -> - if Idmap.mem id idtoev then - user_err (str "Already an existential evar of name " ++ pr_id id); - (EvMap.add evk id evtoid, Idmap.add id evk idtoev) + if Id.Map.mem id idtoev then + user_err (str "Already an existential evar of name " ++ Id.print id); + (EvMap.add evk id evtoid, Id.Map.add id evk idtoev) let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) = if EvMap.mem evk evtoid then @@ -393,15 +393,15 @@ let remove_name_defined evk (evtoid, idtoev as names) = let id = try Some (EvMap.find evk evtoid) with Not_found -> None in match id with | None -> names - | Some id -> (EvMap.remove evk evtoid, Idmap.remove id idtoev) + | Some id -> (EvMap.remove evk evtoid, Id.Map.remove id idtoev) let rename evk id (evtoid, idtoev) = let id' = try Some (EvMap.find evk evtoid) with Not_found -> None in match id' with - | None -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev) + | None -> (EvMap.add evk id evtoid, Id.Map.add id evk idtoev) | Some id' -> - if Idmap.mem id idtoev then anomaly (str "Evar name already in use."); - (EvMap.update evk id evtoid (* overwrite old name *), Idmap.add id evk (Idmap.remove id' idtoev)) + if Id.Map.mem id idtoev then anomaly (str "Evar name already in use."); + (EvMap.set evk id evtoid (* overwrite old name *), Id.Map.add id evk (Id.Map.remove id' idtoev)) let reassign_name_defined evk evk' (evtoid, idtoev as names) = let id = try Some (EvMap.find evk evtoid) with Not_found -> None in @@ -409,13 +409,13 @@ let reassign_name_defined evk evk' (evtoid, idtoev as names) = | None -> names (** evk' must not be defined *) | Some id -> (EvMap.add evk' id (EvMap.remove evk evtoid), - Idmap.add id evk' (Idmap.remove id idtoev)) + Id.Map.add id evk' (Id.Map.remove id idtoev)) let ident evk (evtoid, _) = try Some (EvMap.find evk evtoid) with Not_found -> None let key id (_, idtoev) = - Idmap.find id idtoev + Id.Map.find id idtoev end @@ -466,9 +466,8 @@ let add d e i = add_with_name d e i let evar_counter_summary_name = "evar counter" (* Generator of existential names *) -let new_untyped_evar = - let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in - fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr +let evar_ctr, evar_counter_summary_tag = Summary.ref_tag 0 ~name:evar_counter_summary_name +let new_untyped_evar () = incr evar_ctr; Evar.unsafe_of_int !evar_ctr let new_evar evd ?name evi = let evk = new_untyped_evar () in @@ -630,7 +629,9 @@ let evar_source evk d = (find d evk).evar_source let evar_ident evk evd = EvNames.ident evk evd.evar_names let evar_key id evd = EvNames.key id evd.evar_names -let define_aux def undef evk body = +let restricted = Store.field () + +let define_aux ?dorestrict def undef evk body = let oldinfo = try EvMap.find evk undef with Not_found -> @@ -640,7 +641,10 @@ let define_aux def undef evk body = anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.") in let () = assert (oldinfo.evar_body == Evar_empty) in - let newinfo = { oldinfo with evar_body = Evar_defined body } in + let evar_extra = match dorestrict with + | Some evk' -> Store.set oldinfo.evar_extra restricted evk' + | None -> oldinfo.evar_extra in + let newinfo = { oldinfo with evar_body = Evar_defined body; evar_extra } in EvMap.add evk newinfo def, EvMap.remove evk undef (* define the existential of section path sp as the constr body *) @@ -653,6 +657,9 @@ let define evk body evd = let evar_names = EvNames.remove_name_defined evk evd.evar_names in { evd with defn_evars; undf_evars; last_mods; evar_names } +let is_restricted_evar evi = + Store.get evi.evar_extra restricted + let restrict evk filter ?candidates ?src evd = let evk' = new_untyped_evar () in let evar_info = EvMap.find evk evd.undf_evars in @@ -667,7 +674,7 @@ let restrict evk filter ?candidates ?src evd = let ctxt = Filter.filter_list filter (evar_context evar_info) in let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in let body = mkEvar(evk',id_inst) in - let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in + let (defn_evars, undf_evars) = define_aux ~dorestrict:evk' evd.defn_evars evd.undf_evars evk body in { evd with undf_evars = EvMap.add evk' evar_info' undf_evars; defn_evars; last_mods; evar_names }, evk' @@ -699,10 +706,10 @@ let extract_all_conv_pbs evd = extract_conv_pbs evd (fun _ -> true) let loc_of_conv_pb evd (pbty,env,t1,t2) = - match kind_of_term (fst (decompose_app t1)) with + match kind (fst (decompose_app t1)) with | Evar (evk1,_) -> fst (evar_source evk1 evd) | _ -> - match kind_of_term (fst (decompose_app t2)) with + match kind (fst (decompose_app t2)) with | Evar (evk2,_) -> fst (evar_source evk2 evd) | _ -> None @@ -713,9 +720,9 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) = let evars_of_term c = let rec evrec acc c = - match kind_of_term c with + match kind c with | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) - | _ -> Term.fold_constr evrec acc c + | _ -> Constr.fold evrec acc c in evrec Evar.Set.empty c @@ -748,7 +755,12 @@ let evar_universe_context d = d.universes let universe_context_set d = UState.context_set d.universes -let universe_context ?names evd = UState.universe_context ?names evd.universes +let to_universe_context evd = UState.context evd.universes + +let const_univ_entry ~poly evd = UState.const_univ_entry ~poly evd.universes +let ind_univ_entry ~poly evd = UState.ind_univ_entry ~poly evd.universes + +let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl let restrict_universe_context evd vars = { evd with universes = UState.restrict evd.universes vars } @@ -790,8 +802,8 @@ let make_evar_universe_context e l = | None -> uctx | Some us -> List.fold_left - (fun uctx (loc,id) -> - fst (UState.new_univ_variable ?loc univ_rigid (Some (Id.to_string id)) uctx)) + (fun uctx { CAst.loc; v = id } -> + fst (UState.new_univ_variable ?loc univ_rigid (Some id) uctx)) uctx us (****************************************) @@ -843,7 +855,7 @@ let normalize_universe evd = let normalize_universe_instance evd l = let vars = ref (UState.subst evd.universes) in - let normalize = Univ.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in + let normalize = Universes.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in Univ.Instance.subst_fn normalize l let normalize_sort evars s = @@ -922,8 +934,7 @@ let nf_constraints evd = let universe_of_name evd s = UState.universe_of_name evd.universes s -let add_universe_name evd s l = - { evd with universes = UState.add_universe_name evd.universes s l } +let universe_binders evd = UState.universe_binders evd.universes let universes evd = UState.ugraph evd.universes |