aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/eConstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/eConstr.ml')
-rw-r--r--engine/eConstr.ml54
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