From 3a0b543af4ac99b29efdebe27b1d204d044a7bf0 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 31 Mar 2018 17:43:18 +0200 Subject: Evar maps contain econstrs. We bootstrap the circular evar_map <-> econstr dependency by moving the internal EConstr.API module to Evd.MiniEConstr. Then we make the Evd functions use econstr. --- engine/eConstr.ml | 148 +++++----------------------------------------------- engine/eConstr.mli | 5 +- engine/evarutil.ml | 51 +++++++++--------- engine/evarutil.mli | 2 +- engine/evd.ml | 105 +++++++++++++++++++++++++++++++++++++ engine/evd.mli | 133 ++++++++++++++++++++++++++++++++-------------- engine/proofview.ml | 9 ++-- engine/termops.ml | 17 +++--- 8 files changed, 258 insertions(+), 212 deletions(-) (limited to 'engine') diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 01b4fe851..a72bdee12 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -13,138 +13,8 @@ open Util open Names open Constr open Context -open Evd - -module API : -sig -module ESorts : -sig -type t -val make : Sorts.t -> t -val kind : Evd.evar_map -> t -> Sorts.t -val unsafe_to_sorts : t -> Sorts.t -end -module EInstance : -sig -type t -val make : Univ.Instance.t -> t -val kind : Evd.evar_map -> t -> Univ.Instance.t -val empty : t -val is_empty : t -> bool -val unsafe_to_instance : t -> Univ.Instance.t -end -type t -val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -val kind_upto : Evd.evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term -val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type -val whd_evar : Evd.evar_map -> t -> t -val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t -val of_constr : Constr.t -> t -val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t -val unsafe_to_constr : t -> Constr.t -val unsafe_eq : (t, Constr.t) eq -val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, t) Context.Named.Declaration.pt -val unsafe_to_named_decl : (t, t) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt -val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt -val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t) Context.Rel.Declaration.pt -val to_rel_decl : Evd.evar_map -> (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt -end = -struct - -module ESorts = -struct - type t = Sorts.t - let make s = s - let kind sigma = function - | Sorts.Type u -> Sorts.sort_of_univ (Evd.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 Evd.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 = Constr.t - -let safe_evar_value sigma ev = - try Some (Evd.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 rec to_constr c = match Constr.kind c with -| Evar ev -> - begin match safe_evar_value sigma ev with - | Some c -> to_constr c - | None -> - if abort_on_undefined_evars then - anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term") - else - Constr.map (fun c -> to_constr c) c - end -| Sort (Sorts.Type u) -> - let u' = Evd.normalize_universe sigma u in - if u' == u then c else mkSort (Sorts.sort_of_univ u') -| Const (c', u) when not (Univ.Instance.is_empty u) -> - let u' = Evd.normalize_universe_instance sigma u in - if u' == u then c else mkConstU (c', u') -| Ind (i, u) when not (Univ.Instance.is_empty u) -> - let u' = Evd.normalize_universe_instance sigma u in - if u' == u then c else mkIndU (i, u') -| Construct (co, u) when not (Univ.Instance.is_empty u) -> - let u' = Evd.normalize_universe_instance sigma u in - if u' == u then c else mkConstructU (co, u') -| _ -> Constr.map (fun c -> to_constr c) c -in to_constr 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 - -include API +include Evd.MiniEConstr type types = t type constr = t @@ -387,8 +257,7 @@ let decompose_prod_n_assum sigma n c = in prodec_rec Context.Rel.empty n c -let existential_type sigma (evk, args) = - of_constr (existential_type sigma (evk, Array.map unsafe_to_constr args)) +let existential_type = Evd.existential_type let map sigma f c = match kind sigma c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ @@ -749,7 +618,7 @@ let universes_of_constr env sigma c = LSet.fold LSet.add (Universe.levels u) s | Evar (k, args) -> let concl = Evd.evar_concl (Evd.find sigma k) in - fold sigma aux (aux s (of_constr concl)) c + fold sigma aux (aux s concl) c | _ -> fold sigma aux s c in aux LSet.empty c @@ -907,6 +776,10 @@ let named_context e = cast_named_context (sym unsafe_eq) (named_context e) let val_of_named_context e = val_of_named_context (cast_named_context unsafe_eq e) let named_context_of_val e = cast_named_context (sym unsafe_eq) (named_context_of_val e) +let of_existential : Constr.existential -> existential = + let gen : type a b. (a,b) eq -> 'c * b array -> 'c * a array = fun Refl x -> x in + gen unsafe_eq + let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e) let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e) let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e) @@ -922,7 +795,7 @@ let map_rel_context_in_env f env sign = let fresh_global ?loc ?rigid ?names env sigma reference = let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in - evd, of_constr t + evd, t let is_global sigma gr c = Globnames.is_global gr (to_constr sigma c) @@ -934,5 +807,10 @@ let to_instance = EInstance.unsafe_to_instance let to_constr = unsafe_to_constr let to_rel_decl = unsafe_to_rel_decl let to_named_decl = unsafe_to_named_decl +let to_named_context = + let gen : type a b. (a, b) eq -> (a,a) Context.Named.pt -> (b,b) Context.Named.pt + = fun Refl x -> x + in + gen unsafe_eq let eq = unsafe_eq end diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 9cc9bf680..9a5b5ec3a 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -13,7 +13,7 @@ open Names open Constr open Environ -type t +type t = Evd.econstr (** Type of incomplete terms. Essentially a wrapper around {!Constr.t} ensuring that {!Constr.kind} does not observe defined evars. *) @@ -290,6 +290,7 @@ val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool (** {5 Extra} *) +val of_existential : Constr.existential -> existential val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, types) Context.Named.Declaration.pt val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, types) Context.Rel.Declaration.pt @@ -308,6 +309,8 @@ sig val to_named_decl : (t, types) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt (** Physical identity. Does not care for defined evars. *) + val to_named_context : (t, types) Context.Named.pt -> Context.Named.t + val to_sorts : ESorts.t -> Sorts.t (** Physical identity. Does not care for normalization. *) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index c707b37b6..065b42bf6 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -23,7 +23,8 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration let safe_evar_value sigma ev = - try Some (Evd.existential_value sigma ev) + let ev = EConstr.of_existential ev in + try Some (EConstr.Unsafe.to_constr @@ Evd.existential_value sigma ev) with NotInstantiatedEvar | Not_found -> None (** Combinators *) @@ -44,11 +45,11 @@ let evd_comb2 f evdref x y = z let e_new_global evdref x = - EConstr.of_constr (evd_comb1 (Evd.fresh_global (Global.env())) evdref x) + evd_comb1 (Evd.fresh_global (Global.env())) evdref x let new_global evd x = let (evd, c) = Evd.fresh_global (Global.env()) evd x in - (evd, EConstr.of_constr c) + (evd, c) (****************************************************) (* Expanding/testing/exposing existential variables *) @@ -61,7 +62,7 @@ exception Uninstantiated_evar of Evar.t let rec flush_and_check_evars sigma c = match kind c with | Evar (evk,_ as ev) -> - (match existential_opt_value sigma ev with + (match existential_opt_value0 sigma ev with | None -> raise (Uninstantiated_evar evk) | Some c -> flush_and_check_evars sigma c) | _ -> Constr.map (flush_and_check_evars sigma) c @@ -102,7 +103,8 @@ let nf_evar_map_universes evm = if Univ.LMap.is_empty subst then evm, nf_evar0 evm else let f = nf_evars_universes evm in - Evd.raw_map (fun _ -> map_evar_info f) evm, f + let f' c = EConstr.of_constr (f (EConstr.Unsafe.to_constr c)) in + Evd.raw_map (fun _ -> map_evar_info f') evm, f let nf_named_context_evar sigma ctx = Context.Named.map (nf_evar0 sigma) ctx @@ -115,7 +117,7 @@ let nf_env_evar sigma env = let rel' = nf_rel_context_evar sigma (EConstr.rel_context env) in EConstr.push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env) -let nf_evar_info evc info = map_evar_info (nf_evar0 evc) info +let nf_evar_info evc info = map_evar_info (nf_evar evc) info let nf_evar_map evm = Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm @@ -414,7 +416,6 @@ let push_rel_context_to_named_context env sigma typ = let default_source = Loc.tag @@ Evar_kinds.InternalHole let restrict_evar evd evk filter ?src candidates = - let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in Evd.declare_future_goal evk' evd, evk' @@ -424,8 +425,6 @@ let new_pure_evar_full evd evi = (evd, evk) let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ = - let typ = EConstr.Unsafe.to_constr typ in - let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in let default_naming = Misctypes.IntroAnonymous in let naming = Option.default default_naming naming in let name = match naming with @@ -513,7 +512,7 @@ let generalize_evar_over_rels sigma (ev,args) = List.fold_left2 (fun (c,inst as x) a d -> if isRel sigma a then (mkNamedProd_or_LetIn d c,a::inst) else x) - (EConstr.of_constr evi.evar_concl,[]) (Array.to_list args) sign + (evi.evar_concl,[]) (Array.to_list args) sign (************************************) (* Removing a dependency in an evar *) @@ -549,7 +548,8 @@ let rec check_and_clear_in_constr env evdref err ids global c = | Evar (evk,l as ev) -> if Evd.is_defined !evdref evk then (* If evk is already defined we replace it by its definition *) - let nc = Evd.existential_value !evdref ev in + let nc = Evd.existential_value !evdref (EConstr.of_existential ev) in + let nc = EConstr.Unsafe.to_constr nc in (check_and_clear_in_constr env evdref err ids global nc) else (* We check for dependencies to elements of ids in the @@ -559,8 +559,7 @@ let rec check_and_clear_in_constr env evdref err ids global c = removed *) let evi = Evd.find_undefined !evdref evk in let ctxt = Evd.evar_filtered_context evi in - let ctxt = List.map (fun d -> map_named_decl EConstr.of_constr d) ctxt in - let (rids,filter) = + let (rids,filter) = List.fold_right2 (fun h a (ri,filter) -> try @@ -586,7 +585,8 @@ let rec check_and_clear_in_constr env evdref err ids global c = try let nids = Id.Map.domain rids in let global = Id.Set.exists is_section_variable nids in - check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids global (evar_concl evi) + let concl = EConstr.Unsafe.to_constr (evar_concl evi) in + check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids global concl with ClearDependencyError (rid,err) -> raise (ClearDependencyError (Id.Map.find rid rids,err)) in @@ -597,7 +597,7 @@ let rec check_and_clear_in_constr env evdref err ids global c = let evd = !evdref in let (evd,_) = restrict_evar evd evk filter None in evdref := evd; - Evd.existential_value !evdref ev + Evd.existential_value0 !evdref ev | _ -> Constr.map (check_and_clear_in_constr env evdref err ids global) c @@ -643,7 +643,7 @@ let clear_hyps2_in_evi env evdref hyps t concl ids = let queue_set q is_dependent set = Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set let queue_term q is_dependent c = - queue_set q is_dependent (evars_of_term c) + queue_set q is_dependent (evars_of_term (EConstr.Unsafe.to_constr c)) let process_dependent_evar q acc evm is_dependent e = let evi = Evd.find evm e in @@ -656,12 +656,12 @@ let process_dependent_evar q acc evm is_dependent e = match decl with | LocalAssum _ -> () | LocalDef (_,b,_) -> queue_term q true b - end (Environ.named_context_of_val evi.evar_hyps); + end (EConstr.named_context_of_val evi.evar_hyps); match evi.evar_body with | Evar_empty -> if is_dependent then Evar.Map.add e None acc else acc | Evar_defined b -> - let subevars = evars_of_term b in + let subevars = evars_of_term (EConstr.Unsafe.to_constr b) in (* evars appearing in the definition of an evar [e] are marked as dependent when [e] is dependent itself: if [e] is a non-dependent goal, then, unless they are reach from another @@ -729,11 +729,11 @@ let undefined_evars_of_named_context evd nc = ~init:Evar.Set.empty let undefined_evars_of_evar_info evd evi = - Evar.Set.union (undefined_evars_of_term evd (EConstr.of_constr evi.evar_concl)) + Evar.Set.union (undefined_evars_of_term evd evi.evar_concl) (Evar.Set.union (match evi.evar_body with | Evar_empty -> Evar.Set.empty - | Evar_defined b -> undefined_evars_of_term evd (EConstr.of_constr b)) + | Evar_defined b -> undefined_evars_of_term evd b) (undefined_evars_of_named_context evd (named_context_of_val evi.evar_hyps))) @@ -781,10 +781,11 @@ let filtered_undefined_evars_of_evar_info ?cache sigma evi = in let accu = match evi.evar_body with | Evar_empty -> Evar.Set.empty - | Evar_defined b -> evars_of_term b + | Evar_defined b -> evars_of_term (EConstr.Unsafe.to_constr b) in - let accu = Evar.Set.union (undefined_evars_of_term sigma (EConstr.of_constr evi.evar_concl)) accu in - evars_of_named_context cache accu (evar_filtered_context evi) + let accu = Evar.Set.union (undefined_evars_of_term sigma evi.evar_concl) accu in + let ctxt = EConstr.Unsafe.to_named_context (evar_filtered_context evi) in + evars_of_named_context cache accu ctxt (* spiwack: this is a more complete version of {!Termops.occur_evar}. The latter does not look recursively into an @@ -794,7 +795,7 @@ let occur_evar_upto sigma n c = let c = EConstr.Unsafe.to_constr c in let rec occur_rec c = match kind c with | Evar (sp,_) when Evar.equal sp n -> raise Occur - | Evar e -> Option.iter occur_rec (existential_opt_value sigma e) + | Evar e -> Option.iter occur_rec (existential_opt_value0 sigma e) | _ -> Constr.iter occur_rec c in try occur_rec c; false with Occur -> true @@ -849,6 +850,8 @@ let compare_constructor_instances evd u u' = let eq_constr_univs_test sigma1 sigma2 t u = (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) let open Evd in + let t = EConstr.Unsafe.to_constr t + and u = EConstr.Unsafe.to_constr u in let fold cstr sigma = try Some (add_universe_constraints sigma cstr) with Univ.UniverseInconsistency _ | UniversesDiffer -> None diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 972b0b9e1..40c1ee082 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -201,7 +201,7 @@ val kind_of_term_upto : evar_map -> Constr.constr -> universes. The term [t] is interpreted in [sigma1] while [u] is interpreted in [sigma2]. The universe constraints in [sigma2] are assumed to be an extention of those in [sigma1]. *) -val eq_constr_univs_test : evar_map -> evar_map -> Constr.constr -> Constr.constr -> bool +val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool (** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns [Inl sigma'] where [sigma'] is [sigma] augmented with universe diff --git a/engine/evd.ml b/engine/evd.ml index f6e13e1f4..6dcec2760 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 @@ -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 } @@ -1065,6 +1074,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 @@ -1217,3 +1227,98 @@ 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 rec to_constr c = match Constr.kind c with + | Evar ev -> + begin match safe_evar_value sigma ev with + | Some c -> to_constr c + | None -> + if abort_on_undefined_evars then + anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term") + else + Constr.map (fun c -> to_constr c) c + end + | Sort (Sorts.Type u) -> + let u' = normalize_universe sigma u in + if u' == u then c else mkSort (Sorts.sort_of_univ u') + | Const (c', u) when not (Univ.Instance.is_empty u) -> + let u' = normalize_universe_instance sigma u in + if u' == u then c else mkConstU (c', u') + | Ind (i, u) when not (Univ.Instance.is_empty u) -> + let u' = normalize_universe_instance sigma u in + if u' == u then c else mkIndU (i, u') + | Construct (co, u) when not (Univ.Instance.is_empty u) -> + let u' = normalize_universe_instance sigma u in + if u' == u then c else mkConstructU (co, u') + | _ -> Constr.map (fun c -> to_constr c) c + in to_constr 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 diff --git a/engine/evd.mli b/engine/evd.mli index 911799c44..5ce16459c 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -28,6 +28,9 @@ open Environ It also contains conversion constraints, debugging information and information about meta variables. *) +type econstr +type etypes = econstr + (** {5 Existential variables and unification states} *) type evar = Evar.t @@ -86,16 +89,16 @@ end type evar_body = | Evar_empty - | Evar_defined of constr + | Evar_defined of econstr module Store : Store.S (** Datatype used to store additional information in evar maps. *) type evar_info = { - evar_concl : constr; + evar_concl : econstr; (** Type of the evar. *) - evar_hyps : named_context_val; + evar_hyps : named_context_val; (** TODO econstr? *) (** Context of the evar. *) evar_body : evar_body; (** Optional content of the evar. *) @@ -105,16 +108,16 @@ type evar_info = { in the solution *) evar_source : Evar_kinds.t located; (** Information about the evar. *) - evar_candidates : constr list option; + evar_candidates : econstr list option; (** List of possible solutions when known that it is a finite list *) evar_extra : Store.t (** Extra store, used for clever hacks. *) } -val make_evar : named_context_val -> types -> evar_info -val evar_concl : evar_info -> constr -val evar_context : evar_info -> Context.Named.t -val evar_filtered_context : evar_info -> Context.Named.t +val make_evar : named_context_val -> etypes -> evar_info +val evar_concl : evar_info -> econstr +val evar_context : evar_info -> (econstr, etypes) Context.Named.pt +val evar_filtered_context : evar_info -> (econstr, etypes) Context.Named.pt val evar_hyps : evar_info -> named_context_val val evar_filtered_hyps : evar_info -> named_context_val val evar_body : evar_info -> evar_body @@ -122,8 +125,8 @@ val evar_filter : evar_info -> Filter.t val evar_env : evar_info -> env val evar_filtered_env : evar_info -> env -val map_evar_body : (constr -> constr) -> evar_body -> evar_body -val map_evar_info : (constr -> constr) -> evar_info -> evar_info +val map_evar_body : (econstr -> econstr) -> evar_body -> evar_body +val map_evar_info : (econstr -> econstr) -> evar_info -> evar_info (** {6 Unification state} **) @@ -190,7 +193,7 @@ val raw_map_undefined : (Evar.t -> evar_info -> evar_info) -> evar_map -> evar_m (** Same as {!raw_map}, but restricted to undefined evars. For efficiency reasons. *) -val define : Evar.t-> constr -> evar_map -> evar_map +val define : Evar.t-> econstr -> evar_map -> evar_map (** Set the body of an evar to the given constr. It is expected that: {ul {- The evar is already present in the evarmap.} @@ -198,7 +201,7 @@ val define : Evar.t-> constr -> evar_map -> evar_map {- All the evars present in the constr should be present in the evar map.} } *) -val cmap : (constr -> constr) -> evar_map -> evar_map +val cmap : (econstr -> econstr) -> evar_map -> evar_map (** Map the function on all terms in the evar map. *) val is_evar : evar_map -> Evar.t-> bool @@ -222,20 +225,26 @@ val drop_all_defined : evar_map -> evar_map exception NotInstantiatedEvar -val existential_value : evar_map -> existential -> constr +val existential_value : evar_map -> econstr pexistential -> econstr (** [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has no body and [Not_found] if it does not exist in [sigma] *) -val existential_type : evar_map -> existential -> types +val existential_value0 : evar_map -> existential -> constr + +val existential_type : evar_map -> econstr pexistential -> etypes -val existential_opt_value : evar_map -> existential -> constr option +val existential_type0 : evar_map -> existential -> types + +val existential_opt_value : evar_map -> econstr pexistential -> econstr option (** Same as {!existential_value} but returns an option instead of raising an exception. *) +val existential_opt_value0 : evar_map -> existential -> constr option + val evar_instance_array : (Context.Named.Declaration.t -> 'a -> bool) -> evar_info -> 'a array -> (Id.t * 'a) list -val instantiate_evar_array : evar_info -> constr -> constr array -> constr +val instantiate_evar_array : evar_info -> econstr -> econstr array -> econstr val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> evar_map -> evar_map -> evar_map @@ -243,7 +252,7 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> (** {6 Misc} *) -val restrict : Evar.t-> Filter.t -> ?candidates:constr list -> +val restrict : Evar.t-> Filter.t -> ?candidates:econstr list -> ?src:Evar_kinds.t located -> evar_map -> evar_map * Evar.t (** Restrict an undefined evar into a new evar by filtering context and possibly limiting the instances to a set of candidates *) @@ -251,7 +260,7 @@ val restrict : Evar.t-> Filter.t -> ?candidates:constr list -> val is_restricted_evar : evar_info -> Evar.t option (** Tell if an evar comes from restriction of another evar, and if yes, which *) -val downcast : Evar.t-> types -> evar_map -> evar_map +val downcast : Evar.t-> etypes -> evar_map -> evar_map (** Change the type of an undefined evar to a new type assumed to be a subtype of its current type; subtyping must be ensured by caller *) @@ -341,7 +350,7 @@ val shelve_on_future_goals : Evar.t list -> future_goals -> future_goals Evar maps also keep track of the universe constraints defined at a given point. This section defines the relevant manipulation functions. *) -val whd_sort_variable : evar_map -> constr -> constr +val whd_sort_variable : evar_map -> econstr -> econstr exception UniversesDiffer @@ -397,8 +406,8 @@ type 'a freelisted = { rebus : 'a; freemetas : Metaset.t } -val metavars_of : constr -> Metaset.t -val mk_freelisted : constr -> constr freelisted +val metavars_of : econstr -> Metaset.t +val mk_freelisted : econstr -> econstr freelisted val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted (** Status of an instance found by unification wrt to the meta it solves: @@ -436,12 +445,12 @@ 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 + | Cltyp of Name.t * econstr freelisted + | Clval of Name.t * (econstr freelisted * instance_status) * econstr freelisted (** Unification constraints *) type conv_pb = Reduction.conv_pb -type evar_constraint = conv_pb * env * constr * constr +type evar_constraint = conv_pb * env * econstr * econstr val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map val extract_changed_conv_pbs : evar_map -> @@ -457,7 +466,7 @@ val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option val evars_of_term : constr -> Evar.Set.t (** including evars in instances of evars *) -val evars_of_named_context : Context.Named.t -> Evar.Set.t +val evars_of_named_context : (econstr, etypes) Context.Named.pt -> Evar.Set.t val evars_of_filtered_evar_info : evar_info -> Evar.Set.t @@ -465,19 +474,20 @@ val evars_of_filtered_evar_info : evar_info -> Evar.Set.t val meta_list : evar_map -> (metavariable * clbinding) list val meta_defined : evar_map -> metavariable -> bool -val meta_value : evar_map -> metavariable -> constr +val meta_value : evar_map -> metavariable -> econstr (** [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if meta has no value *) -val meta_fvalue : evar_map -> metavariable -> constr freelisted * instance_status -val meta_opt_fvalue : evar_map -> metavariable -> (constr freelisted * instance_status) option -val meta_type : evar_map -> metavariable -> types -val meta_ftype : evar_map -> metavariable -> types freelisted +val meta_fvalue : evar_map -> metavariable -> econstr freelisted * instance_status +val meta_opt_fvalue : evar_map -> metavariable -> (econstr freelisted * instance_status) option +val meta_type : evar_map -> metavariable -> etypes +val meta_type0 : evar_map -> metavariable -> types +val meta_ftype : evar_map -> metavariable -> etypes freelisted val meta_name : evar_map -> metavariable -> Name.t val meta_declare : - metavariable -> types -> ?name:Name.t -> evar_map -> evar_map -val meta_assign : metavariable -> constr * instance_status -> evar_map -> evar_map -val meta_reassign : metavariable -> constr * instance_status -> evar_map -> evar_map + metavariable -> etypes -> ?name:Name.t -> evar_map -> evar_map +val meta_assign : metavariable -> econstr * instance_status -> evar_map -> evar_map +val meta_reassign : metavariable -> econstr * instance_status -> evar_map -> evar_map val clear_metas : evar_map -> evar_map @@ -485,10 +495,10 @@ val clear_metas : evar_map -> evar_map val meta_merge : ?with_univs:bool -> evar_map -> evar_map -> evar_map val undefined_metas : evar_map -> metavariable list -val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map -val map_metas : (constr -> constr) -> evar_map -> evar_map +val map_metas_fvalue : (econstr -> econstr) -> evar_map -> evar_map +val map_metas : (econstr -> econstr) -> evar_map -> evar_map -type metabinding = metavariable * constr * instance_status +type metabinding = metavariable * econstr * instance_status val retract_coercible_metas : evar_map -> metabinding list * evar_map @@ -639,13 +649,13 @@ val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> eva val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> - evar_map -> Globnames.global_reference -> evar_map * constr + evar_map -> Globnames.global_reference -> evar_map * econstr (********************************************************************) (* constr with holes and pending resolution of classes, conversion *) (* problems, candidates, etc. *) -type open_constr = evar_map * constr (* Special case when before is empty *) +type open_constr = evar_map * econstr (* Special case when before is empty *) (** Partially constructed constrs. *) @@ -665,3 +675,50 @@ val create_evar_defs : evar_map -> evar_map (** Create an [evar_map] with empty meta map: *) +(** Use this module only to bootstrap EConstr *) +module MiniEConstr : sig + module ESorts : sig + type t + val make : Sorts.t -> t + val kind : evar_map -> t -> Sorts.t + val unsafe_to_sorts : t -> Sorts.t + end + + module EInstance : sig + type t + val make : Univ.Instance.t -> t + val kind : evar_map -> t -> Univ.Instance.t + val empty : t + val is_empty : t -> bool + val unsafe_to_instance : t -> Univ.Instance.t + end + + type t = econstr + + val kind : evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term + val kind_upto : evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term + val kind_of_type : evar_map -> t -> (t, t) Term.kind_of_type + + val whd_evar : evar_map -> t -> t + + val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t + + val of_constr : Constr.t -> t + + val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t + + val unsafe_to_constr : t -> Constr.t + + val unsafe_eq : (t, Constr.t) eq + + val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> + (t, t) Context.Named.Declaration.pt + val unsafe_to_named_decl : (t, t) Context.Named.Declaration.pt -> + (Constr.t, Constr.types) Context.Named.Declaration.pt + val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt -> + (Constr.t, Constr.types) Context.Rel.Declaration.pt + val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> + (t, t) Context.Rel.Declaration.pt + val to_rel_decl : evar_map -> (t, t) Context.Rel.Declaration.pt -> + (Constr.t, Constr.types) Context.Rel.Declaration.pt +end diff --git a/engine/proofview.ml b/engine/proofview.ml index 639f48e77..54237ceb4 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -45,9 +45,9 @@ let compact el ({ solution } as pv) = let pruned_solution = Evd.drop_all_defined solution in let apply_subst_einfo _ ei = Evd.({ ei with - evar_concl = nf0 ei.evar_concl; + evar_concl = nf ei.evar_concl; evar_hyps = Environ.map_named_val nf0 ei.evar_hyps; - evar_candidates = Option.map (List.map nf0) ei.evar_candidates }) in + evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in Feedback.msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size)); @@ -875,8 +875,7 @@ module Progress = struct (** equality function on hypothesis contexts *) let eq_named_context_val sigma1 sigma2 ctx1 ctx2 = - let open Environ in - let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in + let c1 = EConstr.named_context_of_val ctx1 and c2 = EConstr.named_context_of_val ctx2 in let eq_named_declaration d1 d2 = match d1, d2 with | LocalAssum (i1,t1), LocalAssum (i2,t2) -> @@ -1101,7 +1100,7 @@ module Goal = struct let gmake_with info env sigma goal state = { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; sigma = sigma ; - concl = EConstr.of_constr (Evd.evar_concl info); + concl = Evd.evar_concl info; state = state ; self = goal } diff --git a/engine/termops.ml b/engine/termops.ml index b7531f6fc..df43be28e 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -115,7 +115,7 @@ let pr_evar_suggested_name evk sigma = | _,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 sigma (EConstr.of_constr evi.evar_concl) Anonymous + Namegen.id_of_name_using_hdchar env sigma evi.evar_concl Anonymous in let names = EvMap.mapi base_id (undefined_map sigma) in let id = EvMap.find evk names in @@ -154,7 +154,7 @@ let protect f x = with e -> str "EXCEPTION: " ++ str (Printexc.to_string e) let print_kconstr a = - protect (fun c -> print_constr (EConstr.of_constr c)) a + protect (fun c -> print_constr c) a let pr_meta_map evd = let open Evd in @@ -197,11 +197,11 @@ let pr_evar_source = function let print_constr = print_kconstr in let id = Option.get ido in str "parameter " ++ Id.print id ++ spc () ++ str "of" ++ - spc () ++ print_constr (printable_constr_of_global c) + spc () ++ print_constr (EConstr.of_constr @@ printable_constr_of_global c) | Evar_kinds.InternalHole -> str "internal placeholder" | Evar_kinds.TomatchTypeParameter (ind,n) -> let print_constr = print_kconstr in - pr_nth n ++ str " argument of type " ++ print_constr (mkInd ind) + pr_nth n ++ str " argument of type " ++ print_constr (EConstr.mkInd ind) | Evar_kinds.GoalEvar -> str "goal evar" | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause" | Evar_kinds.MatchingVar _ -> str "matching variable" @@ -256,7 +256,7 @@ let compute_evar_dependency_graph sigma = in match evar_body evi with | Evar_empty -> acc - | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term c) acc + | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term (EConstr.Unsafe.to_constr c)) acc in Evd.fold fold sigma EvMap.empty @@ -314,7 +314,8 @@ let print_env_short env = let print_constr = print_kconstr in let pr_rel_decl = function | RelDecl.LocalAssum (n,_) -> Name.print n - | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := " ++ print_constr b ++ str ")" + | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := " + ++ print_constr (EConstr.of_constr b) ++ str ")" in let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in let nc = List.rev (named_context env) in @@ -335,11 +336,11 @@ let pr_evar_constraints sigma pbs = Namegen.make_all_name_different env sigma in print_env_short env ++ spc () ++ str "|-" ++ spc () ++ - protect (print_constr_env env sigma) (EConstr.of_constr t1) ++ spc () ++ + protect (print_constr_env env sigma) t1 ++ spc () ++ str (match pbty with | Reduction.CONV -> "==" | Reduction.CUMUL -> "<=") ++ - spc () ++ protect (print_constr_env env Evd.empty) (EConstr.of_constr t2) + spc () ++ protect (print_constr_env env Evd.empty) t2 in prlist_with_sep fnl pr_evconstr pbs -- cgit v1.2.3