From 011de69dab3afcd265f6e38aab05548654a606c8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 22 Oct 2020 19:41:15 +0200
Subject: Adding a typed interpretation of patterns.

---
 interp/constrintern.ml  | 9 +++++++++
 interp/constrintern.mli | 6 ++++++
 2 files changed, 15 insertions(+)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 959b61a3d7..7dbc6c86a6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2471,6 +2471,15 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign)
             ~pattern_mode:true ~ltacvars env sigma c in
   pattern_of_glob_constr c
 
+let interp_constr_pattern env sigma ?(expected_type=WithoutTypeConstraint) c =
+  let kind_for_intern = match expected_type with OfType _ -> WithoutTypeConstraint | _ -> expected_type in
+  let c = intern_gen kind_for_intern ~pattern_mode:true env sigma c in
+  let flags = { Pretyping.no_classes_no_fail_inference_flags with expand_evars = false } in
+  let sigma, c = understand_tcc ~flags env sigma ~expected_type c in
+  (* FIXME: it is necessary to be unsafe here because of the way we handle
+     evars in the pretyper. Sometimes they get solved eagerly. *)
+  pattern_of_constr env sigma (EConstr.Unsafe.to_constr c)
+
 let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
       { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c =
   let tmp_scope = scope_of_type_kind env sigma kind in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 898a3e09c8..11d756803f 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -136,10 +136,16 @@ val interp_type_evars_impls : ?flags:inference_flags -> env -> evar_map ->
 
 (** Interprets constr patterns *)
 
+(** Without typing *)
 val intern_constr_pattern :
   env -> evar_map -> ?as_type:bool -> ?ltacvars:ltac_sign ->
     constr_pattern_expr -> patvar list * constr_pattern
 
+(** With typing *)
+val interp_constr_pattern :
+  env -> evar_map -> ?expected_type:typing_constraint ->
+    constr_pattern_expr -> constr_pattern
+
 (** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
 val intern_reference : qualid -> GlobRef.t
 
-- 
cgit v1.2.3


From 2355b3ed9a9af853b67f406d61404c4c05f8c8e5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 22 Oct 2020 19:41:47 +0200
Subject: Typing patterns and using type constraints in Search.

We accept patterns that we failed to type as a fallback.
---
 interp/constrintern.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7dbc6c86a6..efab586f8a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2472,8 +2472,7 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign)
   pattern_of_glob_constr c
 
 let interp_constr_pattern env sigma ?(expected_type=WithoutTypeConstraint) c =
-  let kind_for_intern = match expected_type with OfType _ -> WithoutTypeConstraint | _ -> expected_type in
-  let c = intern_gen kind_for_intern ~pattern_mode:true env sigma c in
+  let c = intern_gen expected_type ~pattern_mode:true env sigma c in
   let flags = { Pretyping.no_classes_no_fail_inference_flags with expand_evars = false } in
   let sigma, c = understand_tcc ~flags env sigma ~expected_type c in
   (* FIXME: it is necessary to be unsafe here because of the way we handle
-- 
cgit v1.2.3