diff options
| -rw-r--r-- | engine/eConstr.ml | 37 | ||||
| -rw-r--r-- | engine/eConstr.mli | 3 | ||||
| -rw-r--r-- | engine/evarutil.ml | 40 |
3 files changed, 26 insertions, 54 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 7d4d17c63..2de6d7ae4 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -19,8 +19,10 @@ sig type t val kind : Evd.evar_map -> t -> (t, t) Constr.kind_of_term val kind_upto : Evd.evar_map -> constr -> (constr, types) Constr.kind_of_term +val whd_evar : Evd.evar_map -> t -> t val of_kind : (t, t) Constr.kind_of_term -> t val of_constr : Constr.t -> t +val to_constr : evar_map -> t -> Constr.t val unsafe_to_constr : t -> Constr.t val unsafe_eq : (t, Constr.t) eq end = @@ -32,40 +34,43 @@ let safe_evar_value sigma ev = try Some (Evd.existential_value sigma ev) with NotInstantiatedEvar | Not_found -> None -let rec kind sigma c = - let c0 = Constr.kind c in - match c0 with +let rec whd_evar sigma c = + match Constr.kind c with | Evar (evk, args) -> (match safe_evar_value sigma (evk, args) with - Some c -> kind sigma c - | None -> c0) + Some c -> whd_evar sigma c + | None -> c) | Sort (Type u) -> let u' = Evd.normalize_universe sigma u in - if u' == u then c0 else Sort (Type u') + 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 c0 else Const (c', u') + 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 c0 else Ind (i, u') + 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 c0 else Construct (co, u') - | App (c, args) when isEvar c -> + if u' == u then c else mkConstructU (co, u') + | App (f, args) when isEvar f -> (** Enforce smart constructor invariant on applications *) - let ev = destEvar c in + let ev = destEvar f in begin match safe_evar_value sigma ev with - | None -> c0 - | Some c -> kind sigma (mkApp (c, args)) + | None -> c + | Some f -> whd_evar sigma (mkApp (f, args)) end - | _ -> c0 + | _ -> c +let kind sigma c = Constr.kind (whd_evar sigma c) let kind_upto = kind let of_kind = Constr.of_kind let of_constr c = c let unsafe_to_constr c = c let unsafe_eq = Refl +let rec to_constr sigma t = + Constr.map (fun t -> to_constr sigma t) (whd_evar sigma t) + end include API @@ -457,10 +462,6 @@ let fold sigma f acc c = match kind sigma c with | CoFix (_,(lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl -let to_constr sigma t = - let rec map c = Constr.map map (Constr.of_kind (kind_upto sigma c)) in - map (unsafe_to_constr t) - let compare_gen k eq_inst eq_sort eq_constr c1 c2 = (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr c1 c2 diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 83536d6f8..7992c0633 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -34,6 +34,8 @@ val kind : Evd.evar_map -> t -> (t, t) Constr.kind_of_term (** Same as {!Constr.kind} except that it expands evars and normalizes universes on the fly. *) +val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t) Constr.kind_of_term + val to_constr : Evd.evar_map -> t -> Constr.t (** Returns the evar-normal form of the argument. See {!Evarutil.nf_evar}. *) @@ -146,6 +148,7 @@ val decompose_prod_assum : Evd.evar_map -> t -> rel_context * t val decompose_prod_n_assum : Evd.evar_map -> int -> t -> rel_context * t val existential_type : Evd.evar_map -> existential -> types +val whd_evar : Evd.evar_map -> constr -> constr (** {6 Equality} *) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index ce6d06f23..1624dc93e 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -21,10 +21,6 @@ open Sigma.Notations module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -let safe_evar_info sigma evk = - try Some (Evd.find sigma evk) - with Not_found -> None - let safe_evar_value sigma ev = try Some (Evd.existential_value sigma ev) with NotInstantiatedEvar | Not_found -> None @@ -72,40 +68,12 @@ let rec flush_and_check_evars sigma c = let flush_and_check_evars sigma c = flush_and_check_evars sigma (EConstr.Unsafe.to_constr c) -(* let nf_evar_key = Profile.declare_profile "nf_evar" *) -(* let nf_evar = Profile.profile2 nf_evar_key Reductionops.nf_evar *) - -let rec whd_evar sigma c = - match kind_of_term c with - | Evar (evk, args) -> - begin match safe_evar_info sigma evk with - | Some ({ evar_body = Evar_defined c } as info) -> - let args = Array.map (fun c -> whd_evar sigma c) args in - let c = instantiate_evar_array info c args in - whd_evar sigma c - | _ -> c - end - | Sort (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') - | _ -> c - (** Term exploration up to instantiation. *) -let kind_of_term_upto sigma t = - Constr.kind (whd_evar sigma t) +let kind_of_term_upto = EConstr.kind_upto -let rec nf_evar0 sigma t = Constr.map (fun t -> nf_evar0 sigma t) (whd_evar sigma t) -let whd_evar sigma c = EConstr.of_constr (whd_evar sigma (EConstr.Unsafe.to_constr c)) -let nf_evar sigma c = EConstr.of_constr (nf_evar0 sigma (EConstr.Unsafe.to_constr c)) +let nf_evar0 sigma t = EConstr.to_constr sigma (EConstr.of_constr t) +let whd_evar = EConstr.whd_evar +let nf_evar sigma c = EConstr.of_constr (EConstr.to_constr sigma c) let j_nf_evar sigma j = { uj_val = nf_evar sigma j.uj_val; |