summaryrefslogtreecommitdiff
path: root/pretyping/evd.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
commita4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch)
tree26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /pretyping/evd.ml
parent164c6861860e6b52818c031f901ffeff91fca16a (diff)
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'pretyping/evd.ml')
-rw-r--r--pretyping/evd.ml1908
1 files changed, 0 insertions, 1908 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
deleted file mode 100644
index 01083142..00000000
--- a/pretyping/evd.ml
+++ /dev/null
@@ -1,1908 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \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 Names
-open Nameops
-open Term
-open Vars
-open Termops
-open Environ
-open Globnames
-
-(** Generic filters *)
-module Filter :
-sig
- type t
- val equal : t -> t -> bool
- val identity : t
- val filter_list : t -> 'a list -> 'a list
- val filter_array : t -> 'a array -> 'a array
- val extend : int -> t -> t
- val compose : t -> t -> t
- val apply_subfilter : t -> bool list -> t
- val restrict_upon : t -> int -> (int -> bool) -> t option
- val map_along : (bool -> 'a -> bool) -> t -> 'a list -> t
- val make : bool list -> t
- val repr : t -> bool list option
-end =
-struct
- type t = bool list option
- (** We guarantee through the interface that if a filter is [Some _] then it
- contains at least one [false] somewhere. *)
-
- let identity = None
-
- let rec equal l1 l2 = match l1, l2 with
- | [], [] -> true
- | h1 :: l1, h2 :: l2 ->
- (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 normalize f = if is_identity f then None else Some f
-
- let filter_list f l = match f with
- | None -> l
- | Some f -> CList.filter_with f l
-
- let filter_array f v = match f with
- | None -> v
- | Some f -> CArray.filter_with f v
-
- let rec extend n l =
- if n = 0 then l
- else extend (pred n) (true :: l)
-
- let extend n = function
- | None -> None
- | Some f -> Some (extend n f)
-
- 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_array filter subfilter =
- (** In both cases we statically know that the argument will contain at
- least one [false] *)
- match filter with
- | None -> Some (Array.to_list subfilter)
- | Some f ->
- let len = Array.length subfilter in
- let fold b (i, ans) =
- if b then
- let () = assert (0 <= i) in
- (pred i, Array.unsafe_get subfilter i :: ans)
- else
- (i, false :: ans)
- in
- Some (snd (List.fold_right fold f (pred len, [])))
-
- let apply_subfilter filter subfilter =
- apply_subfilter_array filter (Array.of_list subfilter)
-
- let restrict_upon f len p =
- let newfilter = Array.init len p in
- if Array.for_all (fun id -> id) newfilter then None
- else
- Some (apply_subfilter_array f newfilter)
-
- 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 make l = normalize l
-
- let repr f = f
-
-end
-
-(* The kinds of existential variables are now defined in [Evar_kinds] *)
-
-(* The type of mappings for existential variables *)
-
-module Dummy = struct end
-module Store = Store.Make(Dummy)
-
-type evar = Term.existential_key
-
-let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk)
-
-type evar_body =
- | Evar_empty
- | Evar_defined of constr
-
-type evar_info = {
- evar_concl : constr;
- evar_hyps : named_context_val;
- evar_body : evar_body;
- evar_filter : Filter.t;
- evar_source : Evar_kinds.t Loc.located;
- evar_candidates : constr list option; (* if not None, list of allowed instances *)
- evar_extra : Store.t }
-
-let make_evar hyps ccl = {
- evar_concl = ccl;
- evar_hyps = hyps;
- evar_body = Evar_empty;
- evar_filter = Filter.identity;
- evar_source = (Loc.ghost,Evar_kinds.InternalHole);
- evar_candidates = None;
- evar_extra = Store.empty
-}
-
-let instance_mismatch () =
- anomaly (Pp.str "Signature and its instance do not match")
-
-let evar_concl evi = evi.evar_concl
-
-let evar_filter evi = evi.evar_filter
-
-let evar_body evi = evi.evar_body
-
-let evar_context evi = named_context_of_val evi.evar_hyps
-
-let evar_filtered_context evi =
- Filter.filter_list (evar_filter evi) (evar_context evi)
-
-let evar_hyps evi = evi.evar_hyps
-
-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 = 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 map_evar_body f = function
- | Evar_empty -> Evar_empty
- | Evar_defined d -> Evar_defined (f d)
-
-let map_evar_info f evi =
- {evi with
- evar_body = map_evar_body f evi.evar_body;
- evar_hyps = map_named_val f evi.evar_hyps;
- evar_concl = f evi.evar_concl;
- evar_candidates = Option.map (List.map f) evi.evar_candidates }
-
-let evar_ident_info evi =
- match evi.evar_source with
- | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
- | _,Evar_kinds.VarInstance id -> id
- | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
- | _ ->
- let env = reset_with_named_context evi.evar_hyps (Global.env()) in
- Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous
-
-(* This exception is raised by *.existential_value *)
-exception NotInstantiatedEvar
-
-(* Note: let-in contributes to the instance *)
-
-let evar_instance_array test_id info args =
- let len = Array.length args in
- let rec instrec filter ctxt i = match filter, ctxt with
- | [], [] ->
- if Int.equal i len then []
- else instance_mismatch ()
- | false :: filter, _ :: ctxt ->
- instrec filter ctxt i
- | true :: filter, (id,_,_ as d) :: ctxt ->
- if i < len then
- let c = Array.unsafe_get args i in
- if test_id d c then instrec filter ctxt (succ i)
- else (id, c) :: instrec filter ctxt (succ i)
- else instance_mismatch ()
- | _ -> instance_mismatch ()
- in
- match Filter.repr (evar_filter info) with
- | None ->
- let map i (id,_,_ as d) =
- if (i < len) then
- let c = Array.unsafe_get args i in
- if test_id d c then None else Some (id,c)
- else instance_mismatch ()
- in
- List.map_filter_i map (evar_context info)
- | Some filter ->
- instrec filter (evar_context info) 0
-
-let make_evar_instance_array info args =
- evar_instance_array (fun (id,_,_) -> isVarId id) info args
-
-let instantiate_evar_array info c args =
- let inst = make_evar_instance_array info args in
- match inst with
- | [] -> c
- | _ -> replace_vars inst c
-
-module StringOrd = struct type t = string let compare = String.compare end
-module UNameMap = struct
-
- include Map.Make(StringOrd)
-
- let union s t =
- if s == t then s
- else
- merge (fun k l r ->
- match l, r with
- | Some _, _ -> l
- | _, _ -> r) s t
-end
-
-(* 2nd part used to check consistency on the fly. *)
-type evar_universe_context =
- { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t;
- uctx_local : Univ.universe_context_set; (** The local context of variables *)
- uctx_univ_variables : Universes.universe_opt_subst;
- (** The local universes that are unification variables *)
- uctx_univ_algebraic : Univ.universe_set;
- (** The subset of unification variables that can be instantiated with
- algebraic universes as they appear in inferred types only. *)
- uctx_universes : Univ.universes; (** The current graph extended with the local constraints *)
- uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *)
- }
-
-let empty_evar_universe_context =
- { uctx_names = UNameMap.empty, Univ.LMap.empty;
- uctx_local = Univ.ContextSet.empty;
- uctx_univ_variables = Univ.LMap.empty;
- uctx_univ_algebraic = Univ.LSet.empty;
- uctx_universes = Univ.initial_universes;
- uctx_initial_universes = Univ.initial_universes }
-
-let evar_universe_context_from e =
- let u = universes e in
- {empty_evar_universe_context with
- uctx_universes = u; uctx_initial_universes = u}
-
-let is_empty_evar_universe_context ctx =
- Univ.ContextSet.is_empty ctx.uctx_local &&
- Univ.LMap.is_empty ctx.uctx_univ_variables
-
-let union_evar_universe_context ctx ctx' =
- if ctx == ctx' then ctx
- else if is_empty_evar_universe_context ctx' then ctx
- else
- let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in
- let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in
- let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local)
- (Univ.ContextSet.levels ctx.uctx_local) in
- let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in
- let declarenew g =
- Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g
- in
- let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
- { uctx_names = (names, names_rev);
- uctx_local = local;
- uctx_univ_variables =
- Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
- uctx_univ_algebraic =
- Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic;
- uctx_initial_universes = declarenew ctx.uctx_initial_universes;
- uctx_universes =
- if local == ctx.uctx_local then ctx.uctx_universes
- else
- let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
- Univ.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
-
-(* let union_evar_universe_context_key = Profile.declare_profile "union_evar_universe_context";; *)
-(* let union_evar_universe_context = *)
-(* Profile.profile2 union_evar_universe_context_key union_evar_universe_context;; *)
-
-type 'a in_evar_universe_context = 'a * evar_universe_context
-
-let evar_universe_context_set diff ctx =
- let initctx = ctx.uctx_local in
- let cstrs =
- Univ.LSet.fold
- (fun l cstrs ->
- try
- match Univ.LMap.find l ctx.uctx_univ_variables with
- | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs
- | None -> cstrs
- with Not_found | Option.IsNone -> cstrs)
- (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty
- in
- Univ.ContextSet.add_constraints cstrs initctx
-
-let evar_universe_context_constraints ctx = snd ctx.uctx_local
-let evar_context_universe_context ctx = Univ.ContextSet.to_context ctx.uctx_local
-
-let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local = ctx }
-let evar_universe_context_subst ctx = ctx.uctx_univ_variables
-
-let add_uctx_names s l (names, names_rev) =
- (UNameMap.add s l names, Univ.LMap.add l s names_rev)
-
-let evar_universe_context_of_binders b =
- let ctx = empty_evar_universe_context in
- let names =
- List.fold_left (fun acc (id, l) -> add_uctx_names (Id.to_string id) l acc)
- ctx.uctx_names b
- in { ctx with uctx_names = names }
-
-let instantiate_variable l b v =
- v := Univ.LMap.add l (Some b) !v
-
-exception UniversesDiffer
-
-let process_universe_constraints univs vars alg cstrs =
- let vars = ref vars in
- let normalize = Universes.normalize_universe_opt_subst vars in
- let rec unify_universes fo l d r local =
- let l = normalize l and r = normalize r in
- if Univ.Universe.equal l r then local
- else
- let varinfo x =
- match Univ.Universe.level x with
- | None -> Inl x
- | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l alg)
- in
- if d == Universes.ULe then
- if Univ.check_leq univs l r then
- (** Keep Prop/Set <= var around if var might be instantiated by prop or set
- later. *)
- if Univ.Universe.is_level l then
- match Univ.Universe.level r with
- | Some r ->
- Univ.Constraint.add (Option.get (Univ.Universe.level l),Univ.Le,r) local
- | _ -> local
- else local
- else
- match Univ.Universe.level r with
- | None -> error ("Algebraic universe on the right")
- | Some rl ->
- if Univ.Level.is_small rl then
- let levels = Univ.Universe.levels l in
- Univ.LSet.fold (fun l local ->
- if Univ.Level.is_small l || Univ.LMap.mem l !vars then
- unify_universes fo (Univ.Universe.make l) Universes.UEq r local
- else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None)))
- levels local
- else
- Univ.enforce_leq l r local
- else if d == Universes.ULub then
- match varinfo l, varinfo r with
- | (Inr (l, true, _), Inr (r, _, _))
- | (Inr (r, _, _), Inr (l, true, _)) ->
- instantiate_variable l (Univ.Universe.make r) vars;
- Univ.enforce_eq_level l r local
- | Inr (_, _, _), Inr (_, _, _) ->
- unify_universes true l Universes.UEq r local
- | _, _ -> assert false
- else (* d = Universes.UEq *)
- match varinfo l, varinfo r with
- | Inr (l', lloc, _), Inr (r', rloc, _) ->
- let () =
- if lloc then
- instantiate_variable l' r vars
- else if rloc then
- instantiate_variable r' l vars
- else if not (Univ.check_eq univs l r) then
- (* Two rigid/global levels, none of them being local,
- one of them being Prop/Set, disallow *)
- if Univ.Level.is_small l' || Univ.Level.is_small r' then
- raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
- else
- if fo then
- raise UniversesDiffer
- in
- Univ.enforce_eq_level l' r' local
- | Inr (l, loc, alg), Inl r
- | Inl r, Inr (l, loc, alg) ->
- let inst = Univ.univ_level_rem l r r in
- if alg then (instantiate_variable l inst vars; local)
- else
- let lu = Univ.Universe.make l in
- if Univ.univ_level_mem l r then
- Univ.enforce_leq inst lu local
- else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
- | _, _ (* One of the two is algebraic or global *) ->
- if Univ.check_eq univs l r then local
- else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
- in
- let local =
- Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local)
- cstrs Univ.Constraint.empty
- in
- !vars, local
-
-let add_constraints_context ctx cstrs =
- let univs, local = ctx.uctx_local in
- let cstrs' = Univ.Constraint.fold (fun (l,d,r) acc ->
- let l = Univ.Universe.make l and r = Univ.Universe.make r in
- let cstr' =
- if d == Univ.Lt then (Univ.Universe.super l, Universes.ULe, r)
- else (l, (if d == Univ.Le then Universes.ULe else Universes.UEq), r)
- in Universes.Constraints.add cstr' acc)
- cstrs Universes.Constraints.empty
- in
- let vars, local' =
- process_universe_constraints ctx.uctx_universes
- ctx.uctx_univ_variables ctx.uctx_univ_algebraic
- cstrs'
- in
- { ctx with uctx_local = (univs, Univ.Constraint.union local local');
- uctx_univ_variables = vars;
- uctx_universes = Univ.merge_constraints local' ctx.uctx_universes }
-
-(* let addconstrkey = Profile.declare_profile "add_constraints_context";; *)
-(* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *)
-
-let add_universe_constraints_context ctx cstrs =
- let univs, local = ctx.uctx_local in
- let vars, local' =
- process_universe_constraints ctx.uctx_universes
- ctx.uctx_univ_variables ctx.uctx_univ_algebraic
- cstrs
- in
- { ctx with uctx_local = (univs, Univ.Constraint.union local local');
- uctx_univ_variables = vars;
- uctx_universes = Univ.merge_constraints local' ctx.uctx_universes }
-
-(* let addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *)
-(* let add_universe_constraints_context = *)
-(* Profile.profile2 addunivconstrkey add_universe_constraints_context;; *)
-(*******************************************************************)
-(* Metamaps *)
-
-(*******************************************************************)
-(* Constraints for existential variables *)
-(*******************************************************************)
-
-type 'a freelisted = {
- rebus : 'a;
- freemetas : Int.Set.t }
-
-(* Collects all metavars appearing in a constr *)
-let metavars_of c =
- let rec collrec acc c =
- match kind_of_term c with
- | Meta mv -> Int.Set.add mv acc
- | _ -> fold_constr collrec acc c
- in
- collrec Int.Set.empty c
-
-let mk_freelisted c =
- { rebus = c; freemetas = metavars_of c }
-
-let map_fl f cfl = { cfl with rebus=f cfl.rebus }
-
-(* Status of an instance found by unification wrt to the meta it solves:
- - a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X)
- - a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X)
- - a term that can be eta-expanded n times while still being a solution
- (e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice)
-*)
-
-type instance_constraint = IsSuperType | IsSubType | Conv
-
-let eq_instance_constraint c1 c2 = c1 == c2
-
-(* Status of the unification of the type of an instance against the type of
- the meta it instantiates:
- - CoerceToType means that the unification of types has not been done
- and that a coercion can still be inserted: the meta should not be
- substituted freely (this happens for instance given via the
- "with" binding clause).
- - TypeProcessed means that the information obtainable from the
- unification of types has been extracted.
- - TypeNotProcessed means that the unification of types has not been
- done but it is known that no coercion may be inserted: the meta
- can be substituted freely.
-*)
-
-type instance_typing_status =
- CoerceToType | TypeNotProcessed | TypeProcessed
-
-(* Status of an instance together with the status of its type unification *)
-
-type instance_status = instance_constraint * instance_typing_status
-
-(* Clausal environments *)
-
-type clbinding =
- | Cltyp of Name.t * constr freelisted
- | Clval of Name.t * (constr freelisted * instance_status) * constr freelisted
-
-let map_clb f = function
- | Cltyp (na,cfl) -> Cltyp (na,map_fl f cfl)
- | Clval (na,(cfl1,pb),cfl2) -> Clval (na,(map_fl f cfl1,pb),map_fl f cfl2)
-
-(* name of defined is erased (but it is pretty-printed) *)
-let clb_name = function
- Cltyp(na,_) -> (na,false)
- | Clval (na,_,_) -> (na,true)
-
-(***********************)
-
-module Metaset = Int.Set
-
-module Metamap = Int.Map
-
-let metamap_to_list m =
- Metamap.fold (fun n v l -> (n,v)::l) m []
-
-(*************************)
-(* Unification state *)
-
-type conv_pb = Reduction.conv_pb
-type evar_constraint = conv_pb * Environ.env * constr * constr
-
-module EvMap = Evar.Map
-
-type evar_map = {
- (** Existential variables *)
- defn_evars : evar_info EvMap.t;
- undf_evars : evar_info EvMap.t;
- evar_names : Id.t EvMap.t * existential_key Idmap.t;
- (** Universes *)
- universes : evar_universe_context;
- (** Conversion problems *)
- conv_pbs : evar_constraint list;
- last_mods : Evar.Set.t;
- (** Metas *)
- metas : clbinding Metamap.t;
- (** Interactive proofs *)
- effects : Safe_typing.private_constants;
- future_goals : Evar.t list; (** list of newly created evars, to be
- eventually turned into goals if not solved.*)
- principal_future_goal : Evar.t option; (** if [Some e], [e] must be
- contained
- [future_goals]. The evar
- [e] will inherit
- properties (now: the
- name) of the evar which
- will be instantiated with
- a term containing [e]. *)
- extras : Store.t;
-}
-
-(*** Lifting primitive from Evar.Map. ***)
-
-let add_name_newly_undefined naming evk evi (evtoid,idtoev) =
- let id = match naming with
- | Misctypes.IntroAnonymous ->
- let id = evar_ident_info evi in
- Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev)
- | Misctypes.IntroIdentifier id ->
- let id' =
- Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
- if not (Names.Id.equal id id') then
- user_err_loc
- (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id);
- id'
- | Misctypes.IntroFresh id ->
- Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
- (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
-
-let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) =
- if EvMap.mem evk evtoid then
- evar_names
- else
- add_name_newly_undefined naming evk evi evar_names
-
-let remove_name_defined evk (evtoid,idtoev) =
- let id = EvMap.find evk evtoid in
- (EvMap.remove evk evtoid, Idmap.remove id idtoev)
-
-let remove_name_possibly_already_defined evk evar_names =
- try remove_name_defined evk evar_names
- with Not_found -> evar_names
-
-let rename evk id evd =
- let (evtoid,idtoev) = evd.evar_names in
- let id' = EvMap.find evk evtoid in
- if Idmap.mem id idtoev then anomaly (str "Evar name already in use");
- { evd with evar_names =
- (EvMap.add evk id evtoid (* overwrite old name *),
- Idmap.add id evk (Idmap.remove id' idtoev)) }
-
-let reassign_name_defined evk evk' (evtoid,idtoev) =
- let id = EvMap.find evk evtoid in
- (EvMap.add evk' id (EvMap.remove evk evtoid),
- Idmap.add id evk' (Idmap.remove id idtoev))
-
-let add d e i = match i.evar_body with
-| Evar_empty ->
- let evar_names = add_name_undefined Misctypes.IntroAnonymous e i d.evar_names in
- { d with undf_evars = EvMap.add e i d.undf_evars; evar_names }
-| Evar_defined _ ->
- let evar_names = remove_name_possibly_already_defined e d.evar_names in
- { d with defn_evars = EvMap.add e i d.defn_evars; evar_names }
-
-let remove d e =
- let undf_evars = EvMap.remove e d.undf_evars in
- let defn_evars = EvMap.remove e d.defn_evars in
- let principal_future_goal = match d.principal_future_goal with
- | None -> None
- | Some e' -> if Evar.equal e e' then None else d.principal_future_goal
- in
- let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in
- { d with undf_evars; defn_evars; principal_future_goal; future_goals }
-
-let find d e =
- try EvMap.find e d.undf_evars
- with Not_found -> EvMap.find e d.defn_evars
-
-let find_undefined d e = EvMap.find e d.undf_evars
-
-let mem d e = EvMap.mem e d.undf_evars || EvMap.mem e d.defn_evars
-
-(* spiwack: this function loses information from the original evar_map
- it might be an idea not to export it. *)
-let to_list d =
- (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *)
- let l = ref [] in
- EvMap.iter (fun evk x -> l := (evk,x)::!l) d.defn_evars;
- EvMap.iter (fun evk x -> l := (evk,x)::!l) d.undf_evars;
- !l
-
-let undefined_map d = d.undf_evars
-
-let drop_all_defined d = { d with defn_evars = EvMap.empty }
-
-(* spiwack: not clear what folding over an evar_map, for now we shall
- simply fold over the inner evar_map. *)
-let fold f d a =
- EvMap.fold f d.defn_evars (EvMap.fold f d.undf_evars a)
-
-let fold_undefined f d a = EvMap.fold f d.undf_evars a
-
-let raw_map f d =
- let f evk info =
- let ans = f evk info in
- let () = match info.evar_body, ans.evar_body with
- | Evar_defined _, Evar_empty
- | Evar_empty, Evar_defined _ ->
- anomaly (str "Unrespectful mapping function.")
- | _ -> ()
- in
- ans
- in
- let defn_evars = EvMap.smartmapi f d.defn_evars in
- let undf_evars = EvMap.smartmapi f d.undf_evars in
- { d with defn_evars; undf_evars; }
-
-let raw_map_undefined f d =
- let f evk info =
- let ans = f evk info in
- let () = match ans.evar_body with
- | Evar_defined _ ->
- anomaly (str "Unrespectful mapping function.")
- | _ -> ()
- in
- ans
- in
- { d with undf_evars = EvMap.smartmapi f d.undf_evars; }
-
-let is_evar = mem
-
-let is_defined d e = EvMap.mem e d.defn_evars
-
-let is_undefined d e = EvMap.mem e d.undf_evars
-
-let existential_value d (n, args) =
- let info = find d n in
- match evar_body info with
- | Evar_defined c ->
- instantiate_evar_array info c args
- | Evar_empty ->
- raise NotInstantiatedEvar
-
-let existential_opt_value d ev =
- try Some (existential_value d ev)
- with NotInstantiatedEvar -> None
-
-let existential_type d (n, args) =
- let info =
- try find d n
- with Not_found ->
- anomaly (str "Evar " ++ str (string_of_existential n) ++ str " was not declared") in
- instantiate_evar_array info info.evar_concl args
-
-let add_constraints d c =
- { d with universes = add_constraints_context d.universes c }
-
-let add_universe_constraints d c =
- { d with universes = add_universe_constraints_context d.universes c }
-
-(*** /Lifting... ***)
-
-(* evar_map are considered empty disregarding histories *)
-let is_empty d =
- EvMap.is_empty d.defn_evars &&
- EvMap.is_empty d.undf_evars &&
- List.is_empty d.conv_pbs &&
- Metamap.is_empty d.metas
-
-let cmap f evd =
- { evd with
- metas = Metamap.map (map_clb f) evd.metas;
- defn_evars = EvMap.map (map_evar_info f) evd.defn_evars;
- undf_evars = EvMap.map (map_evar_info f) evd.undf_evars
- }
-
-(* spiwack: deprecated *)
-let create_evar_defs sigma = { sigma with
- conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty }
-(* spiwack: tentatively deprecated *)
-let create_goal_evar_defs sigma = { sigma with
- (* conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty } *)
- metas=Metamap.empty }
-
-let empty = {
- defn_evars = EvMap.empty;
- undf_evars = EvMap.empty;
- universes = empty_evar_universe_context;
- conv_pbs = [];
- last_mods = Evar.Set.empty;
- metas = Metamap.empty;
- effects = Safe_typing.empty_private_constants;
- evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *)
- future_goals = [];
- principal_future_goal = None;
- extras = Store.empty;
-}
-
-let from_env e =
- { empty with universes = evar_universe_context_from e }
-
-let from_ctx ctx = { empty with universes = ctx }
-
-let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
-
-let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d =
- let conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs in
- let last_mods = if with_conv_pbs then evd.last_mods else d.last_mods in
- let universes =
- if not with_univs then evd.universes
- else union_evar_universe_context evd.universes d.universes
- in
- { evd with
- metas = d.metas;
- last_mods; conv_pbs; universes }
-
-let merge_universe_context evd uctx' =
- { evd with universes = union_evar_universe_context evd.universes uctx' }
-
-let set_universe_context evd uctx' =
- { evd with universes = uctx' }
-
-let add_conv_pb ?(tail=false) pb d =
- if tail then {d with conv_pbs = d.conv_pbs @ [pb]}
- else {d with conv_pbs = pb::d.conv_pbs}
-
-let evar_source evk d = (find d evk).evar_source
-
-let evar_ident evk evd =
- try EvMap.find evk (fst evd.evar_names)
- with Not_found ->
- (* Unnamed (non-dependent) evar *)
- add_suffix (Id.of_string "X") (string_of_int (Evar.repr evk))
-
-let evar_key id evd =
- Idmap.find id (snd evd.evar_names)
-
-let define_aux def undef evk body =
- let oldinfo =
- try EvMap.find evk undef
- with Not_found ->
- if EvMap.mem evk def then
- anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice")
- else
- 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
- EvMap.add evk newinfo def, EvMap.remove evk undef
-
-(* define the existential of section path sp as the constr body *)
-let define evk body evd =
- let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
- let last_mods = match evd.conv_pbs with
- | [] -> evd.last_mods
- | _ -> Evar.Set.add evk evd.last_mods
- in
- let evar_names = remove_name_defined evk evd.evar_names in
- { evd with defn_evars; undf_evars; last_mods; evar_names }
-
-let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole))
- ?(filter=Filter.identity) ?candidates ?(store=Store.empty)
- ?(naming=Misctypes.IntroAnonymous) evd =
- let () = match Filter.repr filter with
- | None -> ()
- | Some filter ->
- assert (Int.equal (List.length filter) (List.length (named_context_of_val hyps)))
- in
- let evar_info = {
- evar_hyps = hyps;
- evar_concl = ty;
- evar_body = Evar_empty;
- evar_filter = filter;
- evar_source = src;
- evar_candidates = candidates;
- evar_extra = store; }
- in
- let evar_names = add_name_newly_undefined naming evk evar_info evd.evar_names in
- { evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; evar_names }
-
-let restrict evk evk' filter ?candidates evd =
- let evar_info = EvMap.find evk evd.undf_evars in
- let evar_info' =
- { evar_info with evar_filter = filter;
- evar_candidates = candidates;
- evar_extra = Store.empty } in
- let evar_names = reassign_name_defined evk evk' evd.evar_names in
- let ctxt = Filter.filter_list filter (evar_context evar_info) in
- let id_inst = Array.map_of_list (fun (id,_,_) -> mkVar id) 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
- { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
- defn_evars; evar_names }
-
-let downcast evk ccl evd =
- let evar_info = EvMap.find evk evd.undf_evars in
- let evar_info' = { evar_info with evar_concl = ccl } in
- { evd with undf_evars = EvMap.add evk evar_info' evd.undf_evars }
-
-(* extracts conversion problems that satisfy predicate p *)
-(* Note: conv_pbs not satisying p are stored back in reverse order *)
-let extract_conv_pbs evd p =
- let (pbs,pbs1) =
- List.fold_left
- (fun (pbs,pbs1) pb ->
- if p pb then
- (pb::pbs,pbs1)
- else
- (pbs,pb::pbs1))
- ([],[])
- evd.conv_pbs
- in
- {evd with conv_pbs = pbs1; last_mods = Evar.Set.empty},
- pbs
-
-let extract_changed_conv_pbs evd p =
- extract_conv_pbs evd (fun pb -> p evd.last_mods pb)
-
-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
- | Evar (evk1,_) -> fst (evar_source evk1 evd)
- | _ ->
- match kind_of_term (fst (decompose_app t2)) with
- | Evar (evk2,_) -> fst (evar_source evk2 evd)
- | _ -> Loc.ghost
-
-(** The following functions return the set of evars immediately
- contained in the object *)
-
-(* excluding defined evars *)
-
-let evar_list c =
- let rec evrec acc c =
- match kind_of_term c with
- | Evar (evk, _ as ev) -> ev :: acc
- | _ -> fold_constr evrec acc c in
- evrec [] c
-
-let evars_of_term c =
- let rec evrec acc c =
- match kind_of_term c with
- | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
- | _ -> fold_constr evrec acc c
- in
- evrec Evar.Set.empty c
-
-let evars_of_named_context nc =
- List.fold_right (fun (_, b, t) s ->
- Option.fold_left (fun s t ->
- Evar.Set.union s (evars_of_term t))
- (Evar.Set.union s (evars_of_term t)) b)
- nc Evar.Set.empty
-
-let evars_of_filtered_evar_info evi =
- Evar.Set.union (evars_of_term evi.evar_concl)
- (Evar.Set.union
- (match evi.evar_body with
- | Evar_empty -> Evar.Set.empty
- | Evar_defined b -> evars_of_term b)
- (evars_of_named_context (evar_filtered_context evi)))
-
-(**********************************************************)
-(* Sort variables *)
-
-type rigid =
- | UnivRigid
- | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
-
-let univ_rigid = UnivRigid
-let univ_flexible = UnivFlexible false
-let univ_flexible_alg = UnivFlexible true
-
-let evar_universe_context d = d.universes
-
-let universe_context_set d = d.universes.uctx_local
-
-let pr_uctx_level uctx =
- let map, map_rev = uctx.uctx_names in
- fun l ->
- try str(Univ.LMap.find l map_rev)
- with Not_found ->
- Universes.pr_with_global_universes l
-
-let universe_context ?names evd =
- match names with
- | None -> [], Univ.ContextSet.to_context evd.universes.uctx_local
- | Some pl ->
- let levels = Univ.ContextSet.levels evd.universes.uctx_local in
- let newinst, map, left =
- List.fold_right
- (fun (loc,id) (newinst, map, acc) ->
- let l =
- try UNameMap.find (Id.to_string id) (fst evd.universes.uctx_names)
- with Not_found ->
- user_err_loc (loc, "universe_context",
- str"Universe " ++ pr_id id ++ str" is not bound anymore.")
- in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc))
- pl ([], [], levels)
- in
- if not (Univ.LSet.is_empty left) then
- let n = Univ.LSet.cardinal left in
- errorlabstrm "universe_context"
- (str(CString.plural n "Universe") ++ spc () ++
- Univ.LSet.pr (pr_uctx_level evd.universes) left ++
- spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.")
- else
- let inst = Univ.Instance.of_array (Array.of_list newinst) in
- let ctx = Univ.UContext.make (inst,
- Univ.ContextSet.constraints evd.universes.uctx_local)
- in map, ctx
-
-let restrict_universe_context evd vars =
- let uctx = evd.universes in
- let uctx' = Universes.restrict_universe_context uctx.uctx_local vars in
- { evd with universes = { uctx with uctx_local = uctx' } }
-
-let universe_subst evd =
- evd.universes.uctx_univ_variables
-
-let merge_uctx sideff rigid uctx ctx' =
- let open Univ in
- let levels = ContextSet.levels ctx' in
- let uctx = if sideff then uctx else
- match rigid with
- | UnivRigid -> uctx
- | UnivFlexible b ->
- let fold u accu =
- if LMap.mem u accu then accu
- else LMap.add u None accu
- in
- let uvars' = LSet.fold fold levels uctx.uctx_univ_variables in
- if b then
- { uctx with uctx_univ_variables = uvars';
- uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels }
- else { uctx with uctx_univ_variables = uvars' }
- in
- let uctx_local =
- if sideff then uctx.uctx_local
- else ContextSet.append ctx' uctx.uctx_local
- in
- let declare g =
- LSet.fold (fun u g ->
- try Univ.add_universe u false g
- with Univ.AlreadyDeclared when sideff -> g)
- levels g
- in
- let initial = declare uctx.uctx_initial_universes in
- let univs = declare uctx.uctx_universes in
- let uctx_universes = merge_constraints (ContextSet.constraints ctx') univs in
- { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial }
-
-let merge_context_set ?(sideff=false) rigid evd ctx' =
- {evd with universes = merge_uctx sideff rigid evd.universes ctx'}
-
-let merge_uctx_subst uctx s =
- { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s }
-
-let merge_universe_subst evd subst =
- {evd with universes = merge_uctx_subst evd.universes subst }
-
-let with_context_set rigid d (a, ctx) =
- (merge_context_set rigid d ctx, a)
-
-let emit_universe_side_effects eff u =
- let uctxs = Safe_typing.universes_of_private eff in
- List.fold_left (merge_uctx true univ_rigid) u uctxs
-
-let uctx_new_univ_variable rigid name predicative
- ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
- let u = Universes.new_univ_level (Global.current_dirpath ()) in
- let ctx' = Univ.ContextSet.add_universe u ctx in
- let uctx', pred =
- match rigid with
- | UnivRigid -> uctx, true
- | UnivFlexible b ->
- let uvars' = Univ.LMap.add u None uvars in
- if b then {uctx with uctx_univ_variables = uvars';
- uctx_univ_algebraic = Univ.LSet.add u avars}, false
- else {uctx with uctx_univ_variables = uvars'}, false
- in
- let names =
- match name with
- | Some n -> add_uctx_names n u uctx.uctx_names
- | None -> uctx.uctx_names
- in
- let initial =
- Univ.add_universe u false uctx.uctx_initial_universes
- in
- let uctx' =
- {uctx' with uctx_names = names; uctx_local = ctx';
- uctx_universes = Univ.add_universe u false uctx.uctx_universes;
- uctx_initial_universes = initial}
- in uctx', u
-
-let new_univ_level_variable ?name ?(predicative=true) rigid evd =
- let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in
- ({evd with universes = uctx'}, u)
-
-let new_univ_variable ?name ?(predicative=true) rigid evd =
- let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in
- ({evd with universes = uctx'}, Univ.Universe.make u)
-
-let new_sort_variable ?name ?(predicative=true) rigid d =
- let (d', u) = new_univ_variable rigid ?name ~predicative d in
- (d', Type u)
-
-let add_global_univ d u =
- let uctx = d.universes in
- let initial =
- Univ.add_universe u true uctx.uctx_initial_universes
- in
- let univs =
- Univ.add_universe u true uctx.uctx_universes
- in
- { d with universes = { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local;
- uctx_initial_universes = initial;
- uctx_universes = univs } }
-
-let make_flexible_variable evd b u =
- let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as ctx = evd.universes in
- let uvars' = Univ.LMap.add u None uvars in
- let avars' =
- if b then
- let uu = Univ.Universe.make u in
- let substu_not_alg u' v =
- Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v
- in
- if not (Univ.LMap.exists substu_not_alg uvars)
- then Univ.LSet.add u avars else avars
- else avars
- in
- {evd with universes = {ctx with uctx_univ_variables = uvars';
- uctx_univ_algebraic = avars'}}
-
-let make_evar_universe_context e l =
- let uctx = evar_universe_context_from e in
- match l with
- | None -> uctx
- | Some us ->
- List.fold_left
- (fun uctx (loc,id) ->
- fst (uctx_new_univ_variable univ_rigid (Some (Id.to_string id)) true uctx))
- uctx us
-
-(****************************************)
-(* Operations on constants *)
-(****************************************)
-
-let fresh_sort_in_family ?(rigid=univ_flexible) env evd s =
- with_context_set rigid evd (Universes.fresh_sort_in_family env s)
-
-let fresh_constant_instance env evd c =
- with_context_set univ_flexible evd (Universes.fresh_constant_instance env c)
-
-let fresh_inductive_instance env evd i =
- with_context_set univ_flexible evd (Universes.fresh_inductive_instance env i)
-
-let fresh_constructor_instance env evd c =
- with_context_set univ_flexible evd (Universes.fresh_constructor_instance env c)
-
-let fresh_global ?(rigid=univ_flexible) ?names env evd gr =
- with_context_set rigid evd (Universes.fresh_global_instance ?names env gr)
-
-let whd_sort_variable evd t = t
-
-let is_sort_variable evd s =
- match s with
- | Type u ->
- (match Univ.universe_level u with
- | Some l as x ->
- let uctx = evd.universes in
- if Univ.LSet.mem l (Univ.ContextSet.levels uctx.uctx_local) then x
- else None
- | None -> None)
- | _ -> None
-
-let is_flexible_level evd l =
- let uctx = evd.universes in
- Univ.LMap.mem l uctx.uctx_univ_variables
-
-let is_eq_sort s1 s2 =
- if Sorts.equal s1 s2 then None
- else
- let u1 = univ_of_sort s1
- and u2 = univ_of_sort s2 in
- if Univ.Universe.equal u1 u2 then None
- else Some (u1, u2)
-
-let normalize_universe evd =
- let vars = ref evd.universes.uctx_univ_variables in
- let normalize = Universes.normalize_universe_opt_subst vars in
- normalize
-
-let normalize_universe_instance evd l =
- let vars = ref evd.universes.uctx_univ_variables in
- let normalize = Univ.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in
- Univ.Instance.subst_fn normalize l
-
-let normalize_sort evars s =
- match s with
- | Prop _ -> s
- | Type u ->
- let u' = normalize_universe evars u in
- if u' == u then s else Type u'
-
-(* FIXME inefficient *)
-let set_eq_sort env d s1 s2 =
- let s1 = normalize_sort d s1 and s2 = normalize_sort d s2 in
- match is_eq_sort s1 s2 with
- | None -> d
- | Some (u1, u2) ->
- if not (type_in_type env) then
- add_universe_constraints d
- (Universes.Constraints.singleton (u1,Universes.UEq,u2))
- else
- d
-
-let has_lub evd u1 u2 =
- (* let normalize = Universes.normalize_universe_opt_subst (ref univs.uctx_univ_variables) in *)
- (* (\* let dref, norm = memo_normalize_universe d in *\) *)
- (* let u1 = normalize u1 and u2 = normalize u2 in *)
- if Univ.Universe.equal u1 u2 then evd
- else add_universe_constraints evd
- (Universes.Constraints.singleton (u1,Universes.ULub,u2))
-
-let set_eq_level d u1 u2 =
- add_constraints d (Univ.enforce_eq_level u1 u2 Univ.Constraint.empty)
-
-let set_leq_level d u1 u2 =
- add_constraints d (Univ.enforce_leq_level u1 u2 Univ.Constraint.empty)
-
-let set_eq_instances ?(flex=false) d u1 u2 =
- add_universe_constraints d
- (Universes.enforce_eq_instances_univs flex u1 u2 Universes.Constraints.empty)
-
-let set_leq_sort env evd s1 s2 =
- let s1 = normalize_sort evd s1
- and s2 = normalize_sort evd s2 in
- match is_eq_sort s1 s2 with
- | None -> evd
- | Some (u1, u2) ->
- (* if Univ.is_type0_univ u2 then *)
- (* if Univ.is_small_univ u1 then evd *)
- (* else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *)
- (* else if Univ.is_type0m_univ u2 then *)
- (* raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *)
- (* else *)
- if not (type_in_type env) then
- add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2))
- else evd
-
-let check_eq evd s s' =
- Univ.check_eq evd.universes.uctx_universes s s'
-
-let check_leq evd s s' =
- Univ.check_leq evd.universes.uctx_universes s s'
-
-let subst_univs_context_with_def def usubst (ctx, cst) =
- (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst)
-
-let normalize_evar_universe_context_variables uctx =
- let normalized_variables, undef, def, subst =
- Universes.normalize_univ_variables uctx.uctx_univ_variables
- in
- let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in
- let ctx_local', univs = Universes.refresh_constraints uctx.uctx_initial_universes ctx_local in
- subst, { uctx with uctx_local = ctx_local';
- uctx_univ_variables = normalized_variables;
- uctx_universes = univs }
-
-(* let normvarsconstrkey = Profile.declare_profile "normalize_evar_universe_context_variables";; *)
-(* let normalize_evar_universe_context_variables = *)
-(* Profile.profile1 normvarsconstrkey normalize_evar_universe_context_variables;; *)
-
-let abstract_undefined_variables uctx =
- let vars' =
- Univ.LMap.fold (fun u v acc ->
- if v == None then Univ.LSet.remove u acc
- else acc)
- uctx.uctx_univ_variables uctx.uctx_univ_algebraic
- in { uctx with uctx_local = Univ.ContextSet.empty;
- uctx_univ_algebraic = vars' }
-
-let fix_undefined_variables ({ universes = uctx } as evm) =
- let algs', vars' =
- Univ.LMap.fold (fun u v (algs, vars as acc) ->
- if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars)
- else acc)
- uctx.uctx_univ_variables
- (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables)
- in
- {evm with universes =
- { uctx with uctx_univ_variables = vars';
- uctx_univ_algebraic = algs' } }
-
-
-let refresh_undefined_univ_variables uctx =
- let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in
- let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (Univ.subst_univs_level_level subst u) acc)
- uctx.uctx_univ_algebraic Univ.LSet.empty
- in
- let vars =
- Univ.LMap.fold
- (fun u v acc ->
- Univ.LMap.add (Univ.subst_univs_level_level subst u)
- (Option.map (Univ.subst_univs_level_universe subst) v) acc)
- uctx.uctx_univ_variables Univ.LMap.empty
- in
- let declare g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g)
- (Univ.ContextSet.levels ctx') g in
- let initial = declare uctx.uctx_initial_universes in
- let univs = declare Univ.initial_universes in
- let uctx' = {uctx_names = uctx.uctx_names;
- uctx_local = ctx';
- uctx_univ_variables = vars; uctx_univ_algebraic = alg;
- uctx_universes = univs;
- uctx_initial_universes = initial } in
- uctx', subst
-
-let refresh_undefined_universes evd =
- let uctx', subst = refresh_undefined_univ_variables evd.universes in
- let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in
- evd', subst
-
-let normalize_evar_universe_context uctx =
- let rec fixpoint uctx =
- let ((vars',algs'), us') =
- Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables
- uctx.uctx_univ_algebraic
- in
- if Univ.ContextSet.equal us' uctx.uctx_local then uctx
- else
- let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in
- let uctx' =
- { uctx_names = uctx.uctx_names;
- uctx_local = us';
- uctx_univ_variables = vars';
- uctx_univ_algebraic = algs';
- uctx_universes = universes;
- uctx_initial_universes = uctx.uctx_initial_universes }
- in fixpoint uctx'
- in fixpoint uctx
-
-let nf_univ_variables evd =
- let subst, uctx' = normalize_evar_universe_context_variables evd.universes in
- let evd' = {evd with universes = uctx'} in
- evd', subst
-
-let nf_constraints evd =
- let subst, uctx' = normalize_evar_universe_context_variables evd.universes in
- let uctx' = normalize_evar_universe_context uctx' in
- {evd with universes = uctx'}
-
-let nf_constraints =
- if Flags.profile then
- let nfconstrkey = Profile.declare_profile "nf_constraints" in
- Profile.profile1 nfconstrkey nf_constraints
- else nf_constraints
-
-let universe_of_name evd s =
- UNameMap.find s (fst evd.universes.uctx_names)
-
-let add_universe_name evd s l =
- let names' = add_uctx_names s l evd.universes.uctx_names in
- {evd with universes = {evd.universes with uctx_names = names'}}
-
-let universes evd = evd.universes.uctx_universes
-
-let update_sigma_env evd env =
- let univs = Environ.universes env in
- let eunivs =
- { evd.universes with uctx_initial_universes = univs;
- uctx_universes = univs }
- in
- let eunivs = merge_uctx true univ_rigid eunivs eunivs.uctx_local in
- { evd with universes = eunivs }
-
-(* Conversion w.r.t. an evar map and its local universes. *)
-
-let test_conversion_gen env evd pb t u =
- match pb with
- | Reduction.CONV ->
- Reduction.trans_conv_universes
- full_transparent_state ~evars:(existential_opt_value evd) env
- evd.universes.uctx_universes t u
- | Reduction.CUMUL -> Reduction.trans_conv_leq_universes
- full_transparent_state ~evars:(existential_opt_value evd) env
- evd.universes.uctx_universes t u
-
-let test_conversion env d pb t u =
- try test_conversion_gen env d pb t u; true
- with _ -> false
-
-let eq_constr_univs evd t u =
- let b, c = Universes.eq_constr_univs_infer evd.universes.uctx_universes t u in
- if b then
- try let evd' = add_universe_constraints evd c in evd', b
- with Univ.UniverseInconsistency _ | UniversesDiffer -> evd, false
- else evd, b
-
-let e_eq_constr_univs evdref t u =
- let evd, b = eq_constr_univs !evdref t u in
- evdref := evd; b
-
-(**********************************************************)
-(* Side effects *)
-
-let emit_side_effects eff evd =
- { evd with effects = Safe_typing.concat_private eff evd.effects;
- universes = emit_universe_side_effects eff evd.universes }
-
-let drop_side_effects evd =
- { evd with effects = Safe_typing.empty_private_constants; }
-
-let eval_side_effects evd = evd.effects
-
-(* Future goals *)
-let declare_future_goal evk evd =
- { evd with future_goals = evk::evd.future_goals }
-
-let declare_principal_goal evk evd =
- match evd.principal_future_goal with
- | None -> { evd with
- future_goals = evk::evd.future_goals;
- principal_future_goal=Some evk; }
- | Some _ -> Errors.error "Only one main subgoal per instantiation."
-
-let future_goals evd = evd.future_goals
-
-let principal_future_goal evd = evd.principal_future_goal
-
-let reset_future_goals evd =
- { evd with future_goals = [] ; principal_future_goal=None }
-
-let restore_future_goals evd gls pgl =
- { evd with future_goals = gls ; principal_future_goal = pgl }
-
-(**********************************************************)
-(* Accessing metas *)
-
-(** We use this function to overcome OCaml compiler limitations and to prevent
- the use of costly in-place modifications. *)
-let set_metas evd metas = {
- defn_evars = evd.defn_evars;
- undf_evars = evd.undf_evars;
- universes = evd.universes;
- conv_pbs = evd.conv_pbs;
- last_mods = evd.last_mods;
- metas;
- effects = evd.effects;
- evar_names = evd.evar_names;
- future_goals = evd.future_goals;
- principal_future_goal = evd.principal_future_goal;
- extras = evd.extras;
-}
-
-let meta_list evd = metamap_to_list evd.metas
-
-let undefined_metas evd =
- let filter = function
- | (n,Clval(_,_,typ)) -> None
- | (n,Cltyp (_,typ)) -> Some n
- in
- let m = List.map_filter filter (meta_list evd) in
- List.sort Int.compare m
-
-let map_metas_fvalue f evd =
- let map = function
- | Clval(id,(c,s),typ) -> Clval(id,(mk_freelisted (f c.rebus),s),typ)
- | x -> x
- in
- set_metas evd (Metamap.smartmap map evd.metas)
-
-let meta_opt_fvalue evd mv =
- match Metamap.find mv evd.metas with
- | Clval(_,b,_) -> Some b
- | Cltyp _ -> None
-
-let meta_defined evd mv =
- match Metamap.find mv evd.metas with
- | Clval _ -> true
- | Cltyp _ -> false
-
-let try_meta_fvalue evd mv =
- match Metamap.find mv evd.metas with
- | Clval(_,b,_) -> b
- | Cltyp _ -> raise Not_found
-
-let meta_fvalue evd mv =
- try try_meta_fvalue evd mv
- with Not_found -> anomaly ~label:"meta_fvalue" (Pp.str "meta has no value")
-
-let meta_value evd mv =
- (fst (try_meta_fvalue evd mv)).rebus
-
-let meta_ftype evd mv =
- match Metamap.find mv evd.metas with
- | Cltyp (_,b) -> b
- | Clval(_,_,b) -> b
-
-let meta_type evd mv = (meta_ftype evd mv).rebus
-
-let meta_declare mv v ?(name=Anonymous) evd =
- let metas = Metamap.add mv (Cltyp(name,mk_freelisted v)) evd.metas in
- set_metas evd metas
-
-let meta_assign mv (v, pb) evd =
- let modify _ = function
- | Cltyp (na, ty) -> Clval (na, (mk_freelisted v, pb), ty)
- | _ -> anomaly ~label:"meta_assign" (Pp.str "already defined")
- in
- let metas = Metamap.modify mv modify evd.metas in
- set_metas evd metas
-
-let meta_reassign mv (v, pb) evd =
- let modify _ = function
- | Clval(na, _, ty) -> Clval (na, (mk_freelisted v, pb), ty)
- | _ -> anomaly ~label:"meta_reassign" (Pp.str "not yet defined")
- in
- let metas = Metamap.modify mv modify evd.metas in
- set_metas evd metas
-
-(* If the meta is defined then forget its name *)
-let meta_name evd mv =
- try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous
-
-let explain_no_such_bound_variable evd id =
- let mvl =
- List.rev (Metamap.fold (fun n clb l ->
- let na = fst (clb_name clb) in
- if na != Anonymous then out_name na :: l else l)
- evd.metas []) in
- errorlabstrm "Evd.meta_with_name"
- (str"No such bound variable " ++ pr_id id ++
- (if mvl == [] then str " (no bound variables at all in the expression)."
- else
- (str" (possible name" ++
- str (if List.length mvl == 1 then " is: " else "s are: ") ++
- pr_enum pr_id mvl ++ str").")))
-
-let meta_with_name evd id =
- let na = Name id in
- let (mvl,mvnodef) =
- Metamap.fold
- (fun n clb (l1,l2 as l) ->
- let (na',def) = clb_name clb in
- if Name.equal na na' then if def then (n::l1,l2) else (n::l1,n::l2)
- else l)
- evd.metas ([],[]) in
- match mvnodef, mvl with
- | _,[] ->
- explain_no_such_bound_variable evd id
- | ([n],_|_,[n]) ->
- n
- | _ ->
- errorlabstrm "Evd.meta_with_name"
- (str "Binder name \"" ++ pr_id id ++
- strbrk "\" occurs more than once in clause.")
-
-let clear_metas evd = {evd with metas = Metamap.empty}
-
-let meta_merge ?(with_univs = true) evd1 evd2 =
- let metas = Metamap.fold Metamap.add evd1.metas evd2.metas in
- let universes =
- if with_univs then union_evar_universe_context evd2.universes evd1.universes
- else evd2.universes
- in
- {evd2 with universes; metas; }
-
-type metabinding = metavariable * constr * instance_status
-
-let retract_coercible_metas evd =
- let mc = ref [] in
- let map n v = match v with
- | Clval (na, (b, (Conv, CoerceToType as s)), typ) ->
- let () = mc := (n, b.rebus, s) :: !mc in
- Cltyp (na, typ)
- | v -> v
- in
- let metas = Metamap.smartmapi map evd.metas in
- !mc, set_metas evd metas
-
-let subst_defined_metas_evars (bl,el) c =
- let rec substrec c = match kind_of_term c with
- | Meta i ->
- let select (j,_,_) = Int.equal i j in
- substrec (pi2 (List.find select bl))
- | Evar (evk,args) ->
- let select (_,(evk',args'),_) = Evar.equal evk evk' && Array.equal Constr.equal args args' in
- (try substrec (pi3 (List.find select el))
- with Not_found -> map_constr substrec c)
- | _ -> map_constr substrec c
- in try Some (substrec c) with Not_found -> None
-
-let evar_source_of_meta mv evd =
- match meta_name evd mv with
- | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar)
- | Name id -> (Loc.ghost,Evar_kinds.VarInstance id)
-
-let dependent_evar_ident ev evd =
- let evi = find evd ev in
- match evi.evar_source with
- | (_,Evar_kinds.VarInstance id) -> id
- | _ -> anomaly (str "Not an evar resulting of a dependent binding")
-
-(**********************************************************)
-(* Extra data *)
-
-let get_extra_data evd = evd.extras
-let set_extra_data extras evd = { evd with extras }
-
-(*******************************************************************)
-
-type pending = (* before: *) evar_map * (* after: *) evar_map
-
-type pending_constr = pending * constr
-
-type open_constr = evar_map * constr
-
-(*******************************************************************)
-(* The type constructor ['a sigma] adds an evar map to an object of
- type ['a] *)
-type 'a sigma = {
- it : 'a ;
- sigma : evar_map
-}
-
-let sig_it x = x.it
-let sig_sig x = x.sigma
-let on_sig s f =
- let sigma', v = f s.sigma in
- { s with sigma = sigma' }, v
-
-(*******************************************************************)
-(* The state monad with state an evar map. *)
-
-module MonadR =
- Monad.Make (struct
-
- type +'a t = evar_map -> evar_map * 'a
-
- let return a = fun s -> (s,a)
-
- let (>>=) x f = fun s ->
- let (s',a) = x s in
- f a s'
-
- let (>>) x y = fun s ->
- let (s',()) = x s in
- y s'
-
- let map f x = fun s ->
- on_snd f (x s)
-
- end)
-
-module Monad =
- Monad.Make (struct
-
- type +'a t = evar_map -> 'a * evar_map
-
- let return a = fun s -> (a,s)
-
- let (>>=) x f = fun s ->
- let (a,s') = x s in
- f a s'
-
- let (>>) x y = fun s ->
- let ((),s') = x s in
- y s'
-
- let map f x = fun s ->
- on_fst f (x s)
-
- end)
-
-(**********************************************************)
-(* Failure explanation *)
-
-type unsolvability_explanation = SeveralInstancesFound of int
-
-(**********************************************************)
-(* Pretty-printing *)
-
-let pr_existential_key sigma evk = str "?" ++ pr_id (evar_ident evk sigma)
-
-let pr_instance_status (sc,typ) =
- begin match sc with
- | IsSubType -> str " [or a subtype of it]"
- | IsSuperType -> str " [or a supertype of it]"
- | Conv -> mt ()
- end ++
- begin match typ with
- | CoerceToType -> str " [up to coercion]"
- | TypeNotProcessed -> mt ()
- | TypeProcessed -> str " [type is checked]"
- end
-
-let pr_meta_map mmap =
- let pr_name = function
- Name id -> str"[" ++ pr_id id ++ str"]"
- | _ -> mt() in
- let pr_meta_binding = function
- | (mv,Cltyp (na,b)) ->
- hov 0
- (pr_meta mv ++ pr_name na ++ str " : " ++
- print_constr b.rebus ++ fnl ())
- | (mv,Clval(na,(b,s),t)) ->
- hov 0
- (pr_meta mv ++ pr_name na ++ str " := " ++
- print_constr b.rebus ++
- str " : " ++ print_constr t.rebus ++
- spc () ++ pr_instance_status s ++ fnl ())
- in
- prlist pr_meta_binding (metamap_to_list mmap)
-
-let pr_decl ((id,b,_),ok) =
- match b with
- | None -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}")
- | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++
- print_constr c ++ str (if ok then ")" else "}")
-
-let rec pr_evar_source = function
- | Evar_kinds.QuestionMark _ -> str "underscore"
- | Evar_kinds.CasesType false -> str "pattern-matching return predicate"
- | Evar_kinds.CasesType true ->
- str "subterm of pattern-matching return predicate"
- | Evar_kinds.BinderType (Name id) -> str "type of " ++ Nameops.pr_id id
- | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder"
- | Evar_kinds.ImplicitArg (c,(n,ido),b) ->
- let id = Option.get ido in
- str "parameter " ++ pr_id id ++ spc () ++ str "of" ++
- spc () ++ print_constr (printable_constr_of_global c)
- | Evar_kinds.InternalHole -> str "internal placeholder"
- | Evar_kinds.TomatchTypeParameter (ind,n) ->
- pr_nth n ++ str " argument of type " ++ print_constr (mkInd ind)
- | Evar_kinds.GoalEvar -> str "goal evar"
- | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause"
- | Evar_kinds.MatchingVar _ -> str "matching variable"
- | Evar_kinds.VarInstance id -> str "instance of " ++ pr_id id
- | Evar_kinds.SubEvar evk ->
- str "subterm of " ++ str (string_of_existential evk)
-
-let pr_evar_info evi =
- let phyps =
- try
- 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
- let pb =
- match evi.evar_body with
- | Evar_empty -> mt ()
- | Evar_defined c -> spc() ++ str"=> " ++ print_constr c
- in
- let candidates =
- match evi.evar_body, evi.evar_candidates with
- | Evar_empty, Some l ->
- spc () ++ str "{" ++
- prlist_with_sep (fun () -> str "|") print_constr l ++ str "}"
- | _ ->
- mt ()
- in
- let src = str "(" ++ pr_evar_source (snd evi.evar_source) ++ str ")" in
- hov 2
- (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]" ++
- candidates ++ spc() ++ src)
-
-let compute_evar_dependency_graph (sigma : evar_map) =
- (* Compute the map binding ev to the evars whose body depends on ev *)
- let fold evk evi acc =
- let fold_ev evk' acc =
- let tab =
- try EvMap.find evk' acc
- with Not_found -> Evar.Set.empty
- in
- EvMap.add evk' (Evar.Set.add evk tab) acc
- in
- match evar_body evi with
- | Evar_empty -> assert false
- | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term c) acc
- in
- EvMap.fold fold sigma.defn_evars EvMap.empty
-
-let evar_dependency_closure n sigma =
- (** Create the DAG of depth [n] representing the recursive dependencies of
- undefined evars. *)
- let graph = compute_evar_dependency_graph sigma in
- let rec aux n curr accu =
- if Int.equal n 0 then Evar.Set.union curr accu
- else
- let fold evk accu =
- try
- let deps = EvMap.find evk graph in
- Evar.Set.union deps accu
- with Not_found -> accu
- in
- (** Consider only the newly added evars *)
- let ncurr = Evar.Set.fold fold curr Evar.Set.empty in
- (** Merge the others *)
- let accu = Evar.Set.union curr accu in
- aux (n - 1) ncurr accu
- in
- let undef = EvMap.domain (undefined_map sigma) in
- aux n undef Evar.Set.empty
-
-let evar_dependency_closure n sigma =
- let deps = evar_dependency_closure n sigma in
- let map = EvMap.bind (fun ev -> find sigma ev) deps in
- EvMap.bindings map
-
-let has_no_evar sigma =
- EvMap.is_empty sigma.defn_evars && EvMap.is_empty sigma.undf_evars
-
-let pr_evd_level evd = pr_uctx_level evd.universes
-
-let pr_evar_universe_context ctx =
- let prl = pr_uctx_level ctx in
- if is_empty_evar_universe_context ctx then mt ()
- else
- (str"UNIVERSES:"++brk(0,1)++
- h 0 (Univ.pr_universe_context_set prl ctx.uctx_local) ++ fnl () ++
- str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
- h 0 (Univ.LSet.pr prl ctx.uctx_univ_algebraic) ++ fnl() ++
- str"UNDEFINED UNIVERSES:"++brk(0,1)++
- h 0 (Universes.pr_universe_opt_subst ctx.uctx_univ_variables) ++ fnl())
-
-let print_env_short env =
- let pr_body n = function
- | None -> pr_name n
- | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in
- let pr_named_decl (n, b, _) = pr_body (Name n) b in
- let pr_rel_decl (n, b, _) = pr_body n b in
- let nc = List.rev (named_context env) in
- let rc = List.rev (rel_context env) in
- str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++
- str "[" ++ pr_sequence pr_rel_decl rc ++ str "]"
-
-let pr_evar_constraints pbs =
- let pr_evconstr (pbty, env, t1, t2) =
- print_env_short env ++ spc () ++ str "|-" ++ spc () ++
- print_constr_env env t1 ++ spc () ++
- str (match pbty with
- | Reduction.CONV -> "=="
- | Reduction.CUMUL -> "<=") ++
- spc () ++ print_constr_env env t2
- in
- prlist_with_sep fnl pr_evconstr pbs
-
-let pr_evar_map_gen with_univs pr_evars sigma =
- let { universes = uvs } = sigma in
- let evs = if has_no_evar sigma then mt () else pr_evars sigma ++ fnl ()
- and svs = if with_univs then pr_evar_universe_context uvs else mt ()
- and cstrs =
- if List.is_empty sigma.conv_pbs then mt ()
- else
- str "CONSTRAINTS:" ++ brk (0, 1) ++
- pr_evar_constraints sigma.conv_pbs ++ fnl ()
- and metas =
- if Metamap.is_empty sigma.metas then mt ()
- else
- str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma.metas
- in
- evs ++ svs ++ cstrs ++ metas
-
-let pr_evar_list sigma l =
- let pr (ev, evi) =
- h 0 (str (string_of_existential ev) ++
- str "==" ++ pr_evar_info evi ++
- (if evi.evar_body == Evar_empty
- then str " {" ++ pr_id (evar_ident ev sigma) ++ str "}"
- else mt ()))
- in
- h 0 (prlist_with_sep fnl pr l)
-
-let pr_evar_by_depth depth sigma = match depth with
-| None ->
- (* Print all evars *)
- str"EVARS:"++brk(0,1)++pr_evar_list sigma (to_list sigma)++fnl()
-| Some n ->
- (* Print all evars *)
- str"UNDEFINED EVARS:"++
- (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++
- brk(0,1)++
- pr_evar_list sigma (evar_dependency_closure n sigma)++fnl()
-
-let pr_evar_by_filter filter sigma =
- let defined = Evar.Map.filter filter sigma.defn_evars in
- let undefined = Evar.Map.filter filter sigma.undf_evars in
- let prdef =
- if Evar.Map.is_empty defined then mt ()
- else str "DEFINED EVARS:" ++ brk (0, 1) ++
- pr_evar_list sigma (Evar.Map.bindings defined)
- in
- let prundef =
- if Evar.Map.is_empty undefined then mt ()
- else str "UNDEFINED EVARS:" ++ brk (0, 1) ++
- pr_evar_list sigma (Evar.Map.bindings undefined)
- in
- prdef ++ prundef
-
-let pr_evar_map ?(with_univs=true) depth sigma =
- pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_depth depth sigma) sigma
-
-let pr_evar_map_filter ?(with_univs=true) filter sigma =
- pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_filter filter sigma) sigma
-
-let pr_metaset metas =
- str "[" ++ pr_sequence pr_meta (Metaset.elements metas) ++ str "]"