diff options
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 158 |
1 files changed, 111 insertions, 47 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index f6e13e1f..a438e059 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -21,6 +21,9 @@ open Environ (* module RelDecl = Context.Rel.Declaration *) module NamedDecl = Context.Named.Declaration +type econstr = constr +type etypes = types + (** Generic filters *) module Filter : sig @@ -129,8 +132,6 @@ end module Store = Store.Make () -type evar = Evar.t - let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk) type evar_body = @@ -170,6 +171,8 @@ 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_candidates evi = evi.evar_candidates + let evar_hyps evi = evi.evar_hyps let evar_filtered_hyps evi = match Filter.repr (evar_filter evi) with @@ -507,8 +510,8 @@ let raw_map f d = in ans in - let defn_evars = EvMap.smartmapi f d.defn_evars in - let undf_evars = EvMap.smartmapi f d.undf_evars in + let defn_evars = EvMap.Smart.mapi f d.defn_evars in + let undf_evars = EvMap.Smart.mapi f d.undf_evars in { d with defn_evars; undf_evars; } let raw_map_undefined f d = @@ -521,7 +524,7 @@ let raw_map_undefined f d = in ans in - { d with undf_evars = EvMap.smartmapi f d.undf_evars; } + { d with undf_evars = EvMap.Smart.mapi f d.undf_evars; } let is_evar = mem @@ -537,10 +540,14 @@ let existential_value d (n, args) = | Evar_empty -> raise NotInstantiatedEvar +let existential_value0 = existential_value + let existential_opt_value d ev = try Some (existential_value d ev) with NotInstantiatedEvar -> None +let existential_opt_value0 = existential_opt_value + let existential_type d (n, args) = let info = try find d n @@ -548,6 +555,8 @@ let existential_type d (n, args) = anomaly (str "Evar " ++ str (string_of_existential n) ++ str " was not declared.") in instantiate_evar_array info info.evar_concl args +let existential_type0 = existential_type + let add_constraints d c = { d with universes = UState.add_constraints d.universes c } @@ -613,11 +622,13 @@ let merge_universe_context evd uctx' = let set_universe_context evd uctx' = { evd with universes = uctx' } +(* TODO: make unique *) let add_conv_pb ?(tail=false) pb d = - (** MS: we have duplicates here, why? *) if tail then {d with conv_pbs = d.conv_pbs @ [pb]} else {d with conv_pbs = pb::d.conv_pbs} +let conv_pbs d = d.conv_pbs + let evar_source evk d = (find d evk).evar_source let evar_ident evk evd = EvNames.ident evk evd.evar_names @@ -763,7 +774,7 @@ let universe_subst evd = UState.subst evd.universes let merge_context_set ?loc ?(sideff=false) rigid evd ctx' = - {evd with universes = UState.merge ?loc sideff rigid evd.universes ctx'} + {evd with universes = UState.merge ?loc ~sideff ~extend:true rigid evd.universes ctx'} let merge_universe_subst evd subst = {evd with universes = UState.merge_subst evd.universes subst } @@ -794,22 +805,20 @@ let make_flexible_variable evd ~algebraic u = (* Operations on constants *) (****************************************) -let fresh_sort_in_family ?loc ?(rigid=univ_flexible) env evd s = - with_context_set ?loc rigid evd (Universes.fresh_sort_in_family env s) +let fresh_sort_in_family ?loc ?(rigid=univ_flexible) evd s = + with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family s) let fresh_constant_instance ?loc env evd c = - with_context_set ?loc univ_flexible evd (Universes.fresh_constant_instance env c) + with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c) let fresh_inductive_instance ?loc env evd i = - with_context_set ?loc univ_flexible evd (Universes.fresh_inductive_instance env i) + with_context_set ?loc univ_flexible evd (UnivGen.fresh_inductive_instance env i) let fresh_constructor_instance ?loc env evd c = - with_context_set ?loc univ_flexible evd (Universes.fresh_constructor_instance env c) + with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c) let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr = - with_context_set ?loc rigid evd (Universes.fresh_global_instance ?names env gr) - -let whd_sort_variable evd t = t + with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?names env gr) let is_sort_variable evd s = UState.is_sort_variable evd.universes s @@ -833,18 +842,18 @@ let universe_rigidity evd l = else UnivRigid let normalize_universe evd = - let vars = ref (UState.subst evd.universes) in - let normalize = Universes.normalize_universe_opt_subst vars in + let vars = UState.subst evd.universes in + let normalize = UnivSubst.normalize_universe_opt_subst vars in normalize let normalize_universe_instance evd l = - let vars = ref (UState.subst evd.universes) in - let normalize = Universes.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in + let vars = UState.subst evd.universes in + let normalize = UnivSubst.level_subst_of (UnivSubst.normalize_univ_variable_opt_subst vars) in Univ.Instance.subst_fn normalize l let normalize_sort evars s = match s with - | Prop _ -> s + | Prop | Set -> s | Type u -> let u' = normalize_universe evars u in if u' == u then s else Type u' @@ -857,7 +866,7 @@ 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 (Universes.UEq (u1,u2))) + (UnivProblem.Set.singleton (UnivProblem.UEq (u1,u2))) else d @@ -869,7 +878,7 @@ let set_leq_level d u1 u2 = let set_eq_instances ?(flex=false) d u1 u2 = add_universe_constraints d - (Universes.enforce_eq_instances_univs flex u1 u2 Universes.Constraints.empty) + (UnivProblem.enforce_eq_instances_univs flex u1 u2 UnivProblem.Set.empty) let set_leq_sort env evd s1 s2 = let s1 = normalize_sort evd s1 @@ -878,7 +887,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 (Universes.ULe (u1,u2))) + add_universe_constraints evd (UnivProblem.Set.singleton (UnivProblem.ULe (u1,u2))) else evd let check_eq evd s s' = @@ -887,6 +896,9 @@ let check_eq evd s s' = let check_leq evd s s' = UGraph.check_leq (UState.ugraph evd.universes) s s' +let check_constraints evd csts = + UGraph.check_constraints csts (UState.ugraph evd.universes) + let fix_undefined_variables evd = { evd with universes = UState.fix_undefined_variables evd.universes } @@ -1031,11 +1043,11 @@ let map_metas_fvalue f evd = | 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) + set_metas evd (Metamap.Smart.map map evd.metas) let map_metas f evd = let map cl = map_clb f cl in - set_metas evd (Metamap.smartmap map evd.metas) + set_metas evd (Metamap.Smart.map map evd.metas) let meta_opt_fvalue evd mv = match Metamap.find mv evd.metas with @@ -1065,6 +1077,7 @@ let meta_ftype evd mv = | Clval(_,_,b) -> b let meta_type evd mv = (meta_ftype evd mv).rebus +let meta_type0 = meta_type let meta_declare mv v ?(name=Anonymous) evd = let metas = Metamap.add mv (Cltyp(name,mk_freelisted v)) evd.metas in @@ -1110,7 +1123,7 @@ let retract_coercible_metas evd = Cltyp (na, typ) | v -> v in - let metas = Metamap.smartmapi map evd.metas in + let metas = Metamap.Smart.mapi map evd.metas in !mc, set_metas evd metas let evar_source_of_meta mv evd = @@ -1196,24 +1209,75 @@ module Monad = type unsolvability_explanation = SeveralInstancesFound of int -(** 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 +module MiniEConstr = struct + + module ESorts = + struct + type t = Sorts.t + let make s = s + let kind sigma = function + | Sorts.Type u -> Sorts.sort_of_univ (normalize_universe sigma u) + | s -> s + let unsafe_to_sorts s = s + end + + module EInstance = + struct + type t = Univ.Instance.t + let make i = i + let kind sigma i = + if Univ.Instance.is_empty i then i + else normalize_universe_instance sigma i + let empty = Univ.Instance.empty + let is_empty = Univ.Instance.is_empty + let unsafe_to_instance t = t + end + + type t = econstr + + let safe_evar_value sigma ev = + try Some (existential_value sigma ev) + with NotInstantiatedEvar | Not_found -> None + + let rec whd_evar sigma c = + match Constr.kind c with + | Evar ev -> + begin match safe_evar_value sigma ev with + | Some c -> whd_evar sigma c + | None -> c + end + | App (f, args) when isEvar f -> + (** Enforce smart constructor invariant on applications *) + let ev = destEvar f in + begin match safe_evar_value sigma ev with + | None -> c + | Some f -> whd_evar sigma (mkApp (f, args)) + end + | Cast (c0, k, t) when isEvar c0 -> + (** Enforce smart constructor invariant on casts. *) + let ev = destEvar c0 in + begin match safe_evar_value sigma ev with + | None -> c + | Some c -> whd_evar sigma (mkCast (c, k, t)) + end + | _ -> c + + let kind sigma c = Constr.kind (whd_evar sigma c) + let kind_upto = kind + let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c) + let of_kind = Constr.of_kind + let of_constr c = c + let unsafe_to_constr c = c + let unsafe_eq = Refl + + let to_constr ?(abort_on_undefined_evars=true) sigma c = + let evar_value ev = safe_evar_value sigma ev in + UnivSubst.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c + + let of_named_decl d = d + let unsafe_to_named_decl d = d + let of_rel_decl d = d + let unsafe_to_rel_decl d = d + let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d + +end |