diff options
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 657 |
1 files changed, 188 insertions, 469 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index a6b6f742..f6e13e1f 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1,22 +1,25 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp open CErrors +open Sorts open Util open Names open Nameops -open Term +open Constr open Vars -open Termops open Environ -open Globnames -open Context.Named.Declaration + +(* module RelDecl = Context.Rel.Declaration *) +module NamedDecl = Context.Named.Declaration (** Generic filters *) module Filter : @@ -124,10 +127,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) @@ -149,13 +151,13 @@ let make_evar hyps ccl = { evar_hyps = hyps; evar_body = Evar_empty; evar_filter = Filter.identity; - evar_source = (Loc.ghost,Evar_kinds.InternalHole); + evar_source = Loc.tag @@ Evar_kinds.InternalHole; evar_candidates = None; evar_extra = Store.empty } let instance_mismatch () = - anomaly (Pp.str "Signature and its instance do not match") + anomaly (Pp.str "Signature and its instance do not match.") let evar_concl evi = evi.evar_concl @@ -226,7 +228,7 @@ let evar_instance_array test_id info args = if i < len then let c = Array.unsafe_get args i in if test_id d c then instrec filter ctxt (succ i) - else (get_id d, c) :: instrec filter ctxt (succ i) + else (NamedDecl.get_id d, c) :: instrec filter ctxt (succ i) else instance_mismatch () | _ -> instance_mismatch () in @@ -235,7 +237,7 @@ let evar_instance_array test_id info args = let map i d = if (i < len) then let c = Array.unsafe_get args i in - if test_id d c then None else Some (get_id d, c) + if test_id d c then None else Some (NamedDecl.get_id d, c) else instance_mismatch () in List.map_filter_i map (evar_context info) @@ -243,7 +245,7 @@ let evar_instance_array test_id info args = instrec filter (evar_context info) 0 let make_evar_instance_array info args = - evar_instance_array (isVarId % get_id) info args + evar_instance_array (NamedDecl.get_id %> isVarId) info args let instantiate_evar_array info c args = let inst = make_evar_instance_array info args in @@ -251,22 +253,8 @@ let instantiate_evar_array info c args = | [] -> c | _ -> replace_vars inst c -type evar_universe_context = UState.t - -type 'a in_evar_universe_context = 'a * evar_universe_context -let empty_evar_universe_context = UState.empty -let is_empty_evar_universe_context = UState.is_empty -let union_evar_universe_context = UState.union -let evar_universe_context_set = UState.context_set -let evar_universe_context_constraints = UState.constraints -let evar_context_universe_context = UState.context -let evar_universe_context_of = UState.of_context_set -let evar_universe_context_subst = UState.subst -let add_constraints_context = UState.add_constraints -let add_universe_constraints_context = UState.add_universe_constraints -let constrain_variables = UState.constrain_variables -let evar_universe_context_of_binders = UState.of_binders +type 'a in_evar_universe_context = 'a * UState.t (*******************************************************************) (* Metamaps *) @@ -282,9 +270,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 - | _ -> fold_constr collrec acc c + | _ -> Constr.fold collrec acc c in collrec Int.Set.empty c @@ -359,12 +347,10 @@ module EvMap = Evar.Map module EvNames : sig -open Misctypes - type t val empty : t -val add_name_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> t -> t +val add_name_undefined : Id.t option -> Evar.t -> evar_info -> t -> t val remove_name_defined : Evar.t -> t -> t val rename : Evar.t -> Id.t -> t -> t val reassign_name_defined : Evar.t -> Evar.t -> t -> t @@ -374,25 +360,17 @@ val key : Id.t -> t -> Evar.t end = struct -type t = Id.t EvMap.t * existential_key Idmap.t - -let empty = (EvMap.empty, Idmap.empty) - -let add_name_newly_undefined naming evk evi (evtoid, idtoev as names) = - let id = match naming with - | Misctypes.IntroAnonymous -> None - | Misctypes.IntroIdentifier id -> - if Idmap.mem id idtoev then - user_err_loc - (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id); - Some id - | Misctypes.IntroFresh id -> - let id = Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in - Some id - in +type t = Id.t EvMap.t * Evar.t Id.Map.t + +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 -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev) + | Some id -> + 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 @@ -404,15 +382,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 @@ -420,23 +398,25 @@ 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 +type goal_kind = ToShelve | ToGiveUp + type evar_map = { (** Existential variables *) defn_evars : evar_info EvMap.t; undf_evars : evar_info EvMap.t; evar_names : EvNames.t; (** Universes *) - universes : evar_universe_context; + universes : UState.t; (** Conversion problems *) conv_pbs : evar_constraint list; last_mods : Evar.Set.t; @@ -454,6 +434,7 @@ type evar_map = { name) of the evar which will be instantiated with a term containing [e]. *) + future_goals_status : goal_kind EvMap.t; extras : Store.t; } @@ -462,9 +443,9 @@ type evar_map = { let rename evk id evd = { evd with evar_names = EvNames.rename evk id evd.evar_names } -let add_with_name ?(naming = Misctypes.IntroAnonymous) d e i = match i.evar_body with +let add_with_name ?name d e i = match i.evar_body with | Evar_empty -> - let evar_names = EvNames.add_name_undefined naming e i d.evar_names in + let evar_names = EvNames.add_name_undefined name e i d.evar_names in { d with undf_evars = EvMap.add e i d.undf_evars; evar_names } | Evar_defined _ -> let evar_names = EvNames.remove_name_defined e d.evar_names in @@ -477,13 +458,12 @@ 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 ?naming evi = +let new_evar evd ?name evi = let evk = new_untyped_evar () in - let evd = add_with_name evd ?naming evk evi in + let evd = add_with_name evd ?name evk evi in (evd, evk) let remove d e = @@ -494,7 +474,8 @@ let remove d e = | 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 future_goals_status = EvMap.remove e d.future_goals_status in + { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status } let find d e = try EvMap.find e d.undf_evars @@ -504,15 +485,6 @@ 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 } @@ -573,14 +545,14 @@ 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 + 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 } + { d with universes = UState.add_constraints d.universes c } let add_universe_constraints d c = - { d with universes = add_universe_constraints_context d.universes c } + { d with universes = UState.add_universe_constraints d.universes c } (*** /Lifting... ***) @@ -605,7 +577,7 @@ let create_evar_defs sigma = { sigma with let empty = { defn_evars = EvMap.empty; undf_evars = EvMap.empty; - universes = empty_evar_universe_context; + universes = UState.empty; conv_pbs = []; last_mods = Evar.Set.empty; metas = Metamap.empty; @@ -613,6 +585,7 @@ let empty = { evar_names = EvNames.empty; (* id<->key for undefined evars *) future_goals = []; principal_future_goal = None; + future_goals_status = EvMap.empty; extras = Store.empty; } @@ -628,14 +601,14 @@ let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d = 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 + else UState.union 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' } + { evd with universes = UState.union evd.universes uctx' } let set_universe_context evd uctx' = { evd with universes = uctx' } @@ -650,17 +623,22 @@ 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 -> if EvMap.mem evk def then - anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice") + anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice.") else - anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar") + 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 *) @@ -673,20 +651,26 @@ 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 restrict evk filter ?candidates evd = +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 let evar_info' = { evar_info with evar_filter = filter; evar_candidates = candidates; - evar_extra = Store.empty } in + evar_source = (match src with None -> evar_info.evar_source | Some src -> src) } in + let last_mods = match evd.conv_pbs with + | [] -> evd.last_mods + | _ -> Evar.Set.add evk evd.last_mods in let evar_names = EvNames.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 (mkVar % get_id) ctxt 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; evar_names }, evk' + defn_evars; last_mods; evar_names }, evk' let downcast evk ccl evd = let evar_info = EvMap.find evk evd.undf_evars in @@ -716,39 +700,31 @@ 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) - | _ -> Loc.ghost + | _ -> None (** 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 + match kind c with | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) - | _ -> fold_constr evrec acc c + | _ -> Constr.fold evrec acc c in evrec Evar.Set.empty c let evars_of_named_context nc = - List.fold_right (fun decl s -> - Option.fold_left (fun s t -> - Evar.Set.union s (evars_of_term t)) - (Evar.Set.union s (evars_of_term (get_type decl))) (get_value decl)) - nc Evar.Set.empty + Context.Named.fold_outside + (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term constr))) + nc + ~init:Evar.Set.empty let evars_of_filtered_evar_info evi = Evar.Set.union (evars_of_term evi.evar_concl) @@ -773,8 +749,12 @@ let evar_universe_context d = d.universes let universe_context_set d = UState.context_set d.universes -let pr_uctx_level = UState.pr_uctx_level -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 } @@ -806,18 +786,9 @@ let new_sort_variable ?loc ?name rigid d = let add_global_univ d u = { d with universes = UState.add_global_univ d.universes u } -let make_flexible_variable evd b u = - { evd with universes = UState.make_flexible_variable evd.universes b u } - -let make_evar_universe_context e l = - let uctx = UState.make (Environ.universes e) in - match l with - | 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)) - uctx us +let make_flexible_variable evd ~algebraic u = + { evd with universes = + UState.make_flexible_variable evd.universes ~algebraic u } (****************************************) (* Operations on constants *) @@ -868,7 +839,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 = @@ -886,15 +857,10 @@ let set_eq_sort env d s1 s2 = | Some (u1, u2) -> if not (type_in_type env) then add_universe_constraints d - (Universes.Constraints.singleton (u1,Universes.UEq,u2)) + (Universes.Constraints.singleton (Universes.UEq (u1,u2))) else d -let has_lub evd u1 u2 = - 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) @@ -912,7 +878,7 @@ let set_leq_sort env evd s1 s2 = | None -> evd | Some (u1, u2) -> if not (type_in_type env) then - add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2)) + add_universe_constraints evd (Universes.Constraints.singleton (Universes.ULe (u1,u2))) else evd let check_eq evd s s' = @@ -921,10 +887,6 @@ let check_eq evd s s' = let check_leq evd s s' = UGraph.check_leq (UState.ugraph evd.universes) s s' -let normalize_evar_universe_context_variables = UState.normalize_variables - -let abstract_undefined_variables = UState.abstract_undefined_variables - let fix_undefined_variables evd = { evd with universes = UState.fix_undefined_variables evd.universes } @@ -933,59 +895,27 @@ let refresh_undefined_universes evd = let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in evd', subst -let normalize_evar_universe_context = UState.normalize - -let nf_univ_variables evd = - let subst, uctx' = normalize_evar_universe_context_variables evd.universes in +let nf_univ_variables evd = + let subst, uctx' = UState.normalize_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 +let minimize_universes evd = + let subst, uctx' = UState.normalize_variables evd.universes in + let uctx' = UState.minimize uctx' in {evd with universes = uctx'} 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 let update_sigma_env evd env = { evd with universes = UState.update_sigma_env evd.universes env } -(* 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.conv env - ~evars:((existential_opt_value evd), (UState.ugraph evd.universes)) - t u - | Reduction.CUMUL -> Reduction.conv_leq env - ~evars:((existential_opt_value evd), (UState.ugraph evd.universes)) - t u - -let test_conversion env d pb t u = - try test_conversion_gen env d pb t u; true - with _ -> false - exception UniversesDiffer = UState.UniversesDiffer -let eq_constr_univs evd t u = - let fold cstr sigma = - try Some (add_universe_constraints sigma cstr) - with Univ.UniverseInconsistency _ | UniversesDiffer -> None - in - match Universes.eq_constr_univs_infer (UState.ugraph evd.universes) fold t u evd with - | None -> evd, false - | Some evd -> evd, true - -let e_eq_constr_univs evdref t u = - let evd, b = eq_constr_univs !evdref t u in - evdref := evd; b - (**********************************************************) (* Side effects *) @@ -999,25 +929,72 @@ let drop_side_effects evd = 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_future_goal ?tag evk evd = + { evd with future_goals = evk::evd.future_goals; + future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status } -let declare_principal_goal evk evd = +let declare_principal_goal ?tag evk evd = match evd.principal_future_goal with | None -> { evd with future_goals = evk::evd.future_goals; - principal_future_goal=Some evk; } - | Some _ -> CErrors.error "Only one main subgoal per instantiation." + principal_future_goal=Some evk; + future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status; + } + | Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.") + +type future_goals = Evar.t list * Evar.t option * goal_kind EvMap.t 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 save_future_goals evd = + (evd.future_goals, evd.principal_future_goal, evd.future_goals_status) -let restore_future_goals evd gls pgl = - { evd with future_goals = gls ; principal_future_goal = pgl } +let reset_future_goals evd = + { evd with future_goals = [] ; principal_future_goal = None; + future_goals_status = EvMap.empty } + +let restore_future_goals evd (gls,pgl,map) = + { evd with future_goals = gls ; principal_future_goal = pgl; + future_goals_status = map } + +let fold_future_goals f sigma (gls,pgl,map) = + List.fold_left f sigma gls + +let map_filter_future_goals f (gls,pgl,map) = + (* Note: map is now a superset of filtered evs, but its size should + not be too big, so that's probably ok not to update it *) + (List.map_filter f gls,Option.bind pgl f,map) + +let filter_future_goals f (gls,pgl,map) = + (List.filter f gls,Option.bind pgl (fun a -> if f a then Some a else None),map) + +let dispatch_future_goals_gen distinguish_shelf (gls,pgl,map) = + let rec aux (comb,shelf,givenup as acc) = function + | [] -> acc + | evk :: gls -> + let acc = + try match EvMap.find evk map with + | ToGiveUp -> (comb,shelf,evk::givenup) + | ToShelve -> + if distinguish_shelf then (comb,evk::shelf,givenup) + else raise Not_found + with Not_found -> (evk::comb,shelf,givenup) in + aux acc gls in + (* Note: this reverses the order of initial list on purpose *) + let (comb,shelf,givenup) = aux ([],[],[]) gls in + (comb,shelf,givenup,pgl) + +let dispatch_future_goals = + dispatch_future_goals_gen true + +let extract_given_up_future_goals goals = + let (comb,_,givenup,_) = dispatch_future_goals_gen false goals in + (comb,givenup) + +let shelve_on_future_goals shelved (gls,pgl,map) = + (shelved @ gls, pgl, List.fold_right (fun evk -> EvMap.add evk ToShelve) shelved map) (**********************************************************) (* Accessing metas *) @@ -1034,6 +1011,7 @@ let set_metas evd metas = { effects = evd.effects; evar_names = evd.evar_names; future_goals = evd.future_goals; + future_goals_status = evd.future_goals_status; principal_future_goal = evd.principal_future_goal; extras = evd.extras; } @@ -1076,7 +1054,7 @@ let try_meta_fvalue evd mv = let meta_fvalue evd mv = try try_meta_fvalue evd mv - with Not_found -> anomaly ~label:"meta_fvalue" (Pp.str "meta has no value") + 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 @@ -1095,7 +1073,7 @@ let meta_declare mv v ?(name=Anonymous) evd = 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") + | _ -> anomaly ~label:"meta_assign" (Pp.str "already defined.") in let metas = Metamap.modify mv modify evd.metas in set_metas evd metas @@ -1103,7 +1081,7 @@ let meta_assign mv (v, pb) evd = 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") + | _ -> anomaly ~label:"meta_reassign" (Pp.str "not yet defined.") in let metas = Metamap.modify mv modify evd.metas in set_metas evd metas @@ -1117,7 +1095,7 @@ 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 + if with_univs then UState.union evd2.universes evd1.universes else evd2.universes in {evd2 with universes; metas; } @@ -1137,14 +1115,14 @@ let retract_coercible_metas evd = 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) + | Anonymous -> Loc.tag Evar_kinds.GoalEvar + | Name id -> Loc.tag @@ 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") + | _ -> anomaly (str "Not an evar resulting of a dependent binding.") (**********************************************************) (* Extra data *) @@ -1154,10 +1132,6 @@ 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 (*******************************************************************) @@ -1222,279 +1196,24 @@ module Monad = type unsolvability_explanation = SeveralInstancesFound of int -(**********************************************************) -(* Pretty-printing *) - -let pr_evar_suggested_name evk sigma = - let base_id evk' evi = - match evar_ident evk' sigma with - | Some id -> id - | None -> 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 - in - let names = EvMap.mapi base_id sigma.undf_evars in - let id = EvMap.find evk names in - let fold evk' id' (seen, n) = - if seen then (seen, n) - else if Evar.equal evk evk' then (true, n) - else if Id.equal id id' then (seen, succ n) - else (seen, n) - in - let (_, n) = EvMap.fold fold names (false, 0) in - if n = 0 then id else Nameops.add_suffix id (string_of_int (pred n)) - -let pr_existential_key sigma evk = match evar_ident evk sigma with -| None -> - str "?" ++ pr_id (pr_evar_suggested_name evk sigma) -| Some id -> - str "?" ++ pr_id id - -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 protect f x = - try f x - with e -> str "EXCEPTION: " ++ str (Printexc.to_string e) - -let print_constr a = protect print_constr a - -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 (decl,ok) = - let id = get_id decl in - match get_value decl 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 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 (evar_universe_context_set ctx)) ++ fnl () ++ - str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ - h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++ - str"UNDEFINED UNIVERSES:"++brk(0,1)++ - h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ 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 decl = pr_body (Name (get_id decl)) (get_value decl) in - let pr_rel_decl decl = let open Context.Rel.Declaration in - pr_body (get_name decl) (get_value decl) 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) = - let env = - (** We currently allow evar instances to refer to anonymous de - Bruijn indices, so we protect the error printing code in this - case by giving names to every de Bruijn variable in the - rel_context of the conversion problem. MS: we should rather - stop depending on anonymous variables, they can be used to - indicate independency. Also, this depends on a strategy for - naming/renaming. *) - Namegen.make_all_name_different env - in - 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_existential_key sigma ev ++ 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 "]" +(** Deprecated *) +type evar_universe_context = UState.t +let empty_evar_universe_context = UState.empty +let union_evar_universe_context = UState.union +let evar_universe_context_set = UState.context_set +let evar_universe_context_constraints = UState.constraints +let evar_context_universe_context = UState.context +let evar_universe_context_of = UState.of_context_set +let evar_universe_context_subst = UState.subst +let add_constraints_context = UState.add_constraints +let constrain_variables = UState.constrain_variables +let evar_universe_context_of_binders = UState.of_binders +let make_evar_universe_context e l = + let g = Environ.universes e in + match l with + | None -> UState.make g + | Some l -> UState.make_with_initial_binders g l +let normalize_evar_universe_context_variables = UState.normalize_variables +let abstract_undefined_variables = UState.abstract_undefined_variables +let normalize_evar_universe_context = UState.minimize +let nf_constraints = minimize_universes |