From e68f8c904b7ee8fee9f98f75e37ab6d01b54731f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 26 Apr 2018 14:49:08 +0200
Subject: Typing: define functional alternatives to e_* functions

---
 pretyping/typing.ml  | 10 ++++++++++
 pretyping/typing.mli |  3 +++
 2 files changed, 13 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 281e33e9b..5477d804a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -400,6 +400,11 @@ let e_check env evdref c t =
     error_actual_type_core env !evdref j t
   | Some sigma -> evdref := sigma
 
+let check env sigma c t =
+  let evdref = ref sigma in
+  e_check env evdref c t;
+  !evdref
+
 (* Type of a constr *)
 
 let unsafe_type_of env evd c =
@@ -416,6 +421,11 @@ let e_sort_of env evdref c =
   let a = e_type_judgment env evdref j in
   a.utj_type
 
+let sort_of env sigma c =
+  let evdref = ref sigma in
+  let a = e_sort_of env evdref c in
+  !evdref, a
+
 (* Try to solve the existential variables by typing *)
 
 let type_of ?(refresh=false) env evd c =
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 2239dda5f..da05102f2 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -28,15 +28,18 @@ val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
 val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types
 
 (** Typecheck a type and return its sort *)
+val sort_of : env -> evar_map -> types -> evar_map * Sorts.t
 val e_sort_of : env -> evar_map ref -> types -> Sorts.t
 
 (** Typecheck a term has a given type (assuming the type is OK) *)
+val check : env -> evar_map -> constr -> types -> evar_map
 val e_check   : env -> evar_map ref -> constr -> types -> unit
 
 (** Returns the instantiated type of a metavariable *)
 val meta_type : evar_map -> metavariable -> types
 
 (** Solve existential variables using typing *)
+val solve_evars : env -> evar_map -> constr -> evar_map * constr
 val e_solve_evars : env -> evar_map ref -> constr -> constr
 
 (** Raise an error message if incorrect elimination for this inductive *)
-- 
cgit v1.2.3