diff options
Diffstat (limited to 'engine/eConstr.ml')
-rw-r--r-- | engine/eConstr.ml | 54 |
1 files changed, 43 insertions, 11 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 094841d69..166340b41 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -16,12 +16,19 @@ 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 type t -val kind : Evd.evar_map -> t -> (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term +val kind : Evd.evar_map -> t -> (t, t, ESorts.t, Univ.Instance.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) kind_of_type val whd_evar : Evd.evar_map -> t -> t -val of_kind : (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term -> t +val of_kind : (t, t, ESorts.t, Univ.Instance.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 @@ -33,6 +40,16 @@ val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t) end = struct +module ESorts = +struct + type t = Sorts.t + let make s = s + let kind sigma = function + | Type u -> sort_of_univ (Evd.normalize_universe sigma u) + | s -> s + let unsafe_to_sorts s = s +end + type t = Constr.t let safe_evar_value sigma ev = @@ -46,9 +63,6 @@ let rec whd_evar sigma c = | Some c -> whd_evar sigma c | None -> 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') @@ -82,8 +96,25 @@ 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) +let rec to_constr sigma c = match Constr.kind c with +| Evar ev -> + begin match safe_evar_value sigma ev with + | Some c -> to_constr sigma c + | None -> Constr.map (fun c -> to_constr 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') +| _ -> Constr.map (fun c -> to_constr sigma c) c let of_named_decl d = d let unsafe_to_named_decl d = d @@ -108,14 +139,14 @@ type rel_context = (constr, types) Context.Rel.pt let in_punivs a = (a, Univ.Instance.empty) -let mkProp = of_kind (Sort Sorts.prop) -let mkSet = of_kind (Sort Sorts.set) -let mkType u = of_kind (Sort (Sorts.Type u)) +let mkProp = of_kind (Sort (ESorts.make Sorts.prop)) +let mkSet = of_kind (Sort (ESorts.make Sorts.set)) +let mkType u = of_kind (Sort (ESorts.make (Sorts.Type u))) let mkRel n = of_kind (Rel n) let mkVar id = of_kind (Var id) let mkMeta n = of_kind (Meta n) let mkEvar e = of_kind (Evar e) -let mkSort s = of_kind (Sort s) +let mkSort s = of_kind (Sort (ESorts.make s)) let mkCast (b, k, t) = of_kind (Cast (b, k, t)) let mkProd (na, t, u) = of_kind (Prod (na, t, u)) let mkLambda (na, t, c) = of_kind (Lambda (na, t, c)) @@ -730,6 +761,7 @@ let fresh_global ?loc ?rigid ?names env sigma reference = module Unsafe = struct +let to_sorts = ESorts.unsafe_to_sorts let to_constr = unsafe_to_constr let to_rel_decl = unsafe_to_rel_decl let to_named_decl = unsafe_to_named_decl |