diff options
Diffstat (limited to 'pretyping/evd.ml')
-rw-r--r-- | pretyping/evd.ml | 74 |
1 files changed, 74 insertions, 0 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml new file mode 100644 index 00000000..7a3e7c02 --- /dev/null +++ b/pretyping/evd.ml @@ -0,0 +1,74 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: evd.ml,v 1.3.2.1 2004/07/16 19:30:44 herbelin Exp $ *) + +open Util +open Names +open Term +open Sign + +(* The type of mappings for existential variables *) + +type evar = existential_key + +type evar_body = + | Evar_empty + | Evar_defined of constr + +type evar_info = { + evar_concl : constr; + evar_hyps : named_context; + evar_body : evar_body} + +module Evarmap = Intmap + +type evar_map = evar_info Evarmap.t + +let empty = Evarmap.empty + +let to_list evc = Evarmap.fold (fun ev x acc -> (ev,x)::acc) evc [] +let dom evc = Evarmap.fold (fun ev _ acc -> ev::acc) evc [] +let map evc k = Evarmap.find k evc +let rmv evc k = Evarmap.remove k evc +let remap evc k i = Evarmap.add k i evc +let in_dom evc k = Evarmap.mem k evc + +let add evd ev newinfo = Evarmap.add ev newinfo evd + +let define evd ev body = + let oldinfo = map evd ev in + let newinfo = + { evar_concl = oldinfo.evar_concl; + evar_hyps = oldinfo.evar_hyps; + evar_body = Evar_defined body} + in + match oldinfo.evar_body with + | Evar_empty -> Evarmap.add ev newinfo evd + | _ -> anomaly "cannot define an isevar twice" + +(* The list of non-instantiated existential declarations *) + +let non_instantiated sigma = + let listev = to_list sigma in + List.fold_left + (fun l ((ev,evd) as d) -> + if evd.evar_body = Evar_empty then (d::l) else l) + [] listev + +let is_evar sigma ev = in_dom sigma ev + +let is_defined sigma ev = + let info = map sigma ev in + not (info.evar_body = Evar_empty) + +let evar_body ev = ev.evar_body + +let string_of_existential ev = "?" ^ string_of_int ev + +let existential_of_int ev = ev |