diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-26 14:49:08 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-14 13:25:56 +0200 |
| commit | e68f8c904b7ee8fee9f98f75e37ab6d01b54731f (patch) | |
| tree | bea31974cad014170e42f0bb87ac2163500092c9 /pretyping | |
| parent | 5b432bf03f623b144871181446c68479482abe32 (diff) | |
Typing: define functional alternatives to e_* functions
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typing.ml | 10 | ||||
| -rw-r--r-- | pretyping/typing.mli | 3 |
2 files changed, 13 insertions, 0 deletions
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 *) |