Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + a flag suspectingly renamed in a clearer way

13 files changed, 44 insertions, 35 deletions

diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index bfa43cde1..398c12707 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -25,10 +25,8 @@ echo $TRAVIS_PULL_REQUEST
 echo $TRAVIS_BRANCH
 echo $TRAVIS_COMMIT
 
-if [ $TRAVIS_PULL_REQUEST == "678" ] || [ $TRAVIS_BRANCH == "coqlib-part-02" ]; then
-
-    mathcomp_CI_BRANCH=coqlib-part-02
-    mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git
-
+if [ $TRAVIS_PULL_REQUEST == "590" ] || [ $TRAVIS_BRANCH == "trunk+algebraic-matchingvar" ]; then
+    mathcomp_CI_BRANCH=trunk+pr590-patvar
+    mathcomp_CI_GITURL=https://github.com/herbelin/math-comp.git
 fi
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f6da10c96..19be62972 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -663,9 +663,11 @@ let rec extern inctx scopes vars r =
   | GEvar (n,l) ->
       extern_evar n (List.map (on_snd (extern false scopes vars)) l)
 
-  | GPatVar (b,n) ->
+  | GPatVar kind ->
       if !print_meta_as_hole then CHole (None, Misctypes.IntroAnonymous, None) else
-        if b then CPatVar n else CEvar (n,[])
+       (match kind with
+         | Evar_kinds.SecondOrderPatVar n -> CPatVar n
+         | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[]))
 
   | GApp (f,args) ->
       (match f with
@@ -1037,13 +1039,13 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with
       with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
       GVar id
   | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
-  | PMeta (Some n) -> GPatVar (false,n)
+  | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n)
   | PProj (p,c) -> GApp (CAst.make @@ GRef (ConstRef (Projection.constant p),None),
 			 [glob_of_pat env sigma c])
   | PApp (f,args) ->
       GApp (glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args)
   | PSoApp (n,args) ->
-      GApp (CAst.make @@ GPatVar (true,n),
+      GApp (CAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar n),
         List.map (glob_of_pat env sigma) args)
   | PProd (na,t,c) ->
       GProd (na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 190369e8f..120258b45 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1506,7 +1506,7 @@ let extract_explicit_arg imps args =
 (**********************************************************************)
 (* Main loop                                                          *)
 
-let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
+let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
   let rec intern env = CAst.with_loc_val (fun ?loc -> function
     | CRef (ref,us) ->
 	let (c,imp,subscopes,l),_ =
@@ -1749,12 +1749,12 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	CAst.make ?loc @@
 	GHole (k, naming, solve)
     (* Parsing pattern variables *)
-    | CPatVar n when allow_patvar ->
+    | CPatVar n when pattern_mode ->
 	CAst.make ?loc @@
-	GPatVar (true,n)
-    | CEvar (n, []) when allow_patvar ->
+	GPatVar (Evar_kinds.SecondOrderPatVar n)
+    | CEvar (n, []) when pattern_mode ->
 	CAst.make ?loc @@
-	GPatVar (false,n)
+	GPatVar (Evar_kinds.FirstOrderPatVar n)
     (* end *)
     (* Parsing existential variables *)
     | CEvar (n, l) ->
@@ -1944,13 +1944,13 @@ let empty_ltac_sign = {
 }
 
 let intern_gen kind env
-               ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign)
+               ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
                c =
   let tmp_scope = scope_of_type_kind kind in
   internalize env {ids = extract_ids env; unb = false;
 		         tmp_scope = tmp_scope; scopes = [];
 			 impls = impls}
-    allow_patvar (ltacvars, Id.Map.empty) c
+    pattern_mode (ltacvars, Id.Map.empty) c
 
 let intern_constr env c = intern_gen WithoutTypeConstraint env c
 
@@ -2023,7 +2023,7 @@ let interp_type_evars env evdref ?(impls=empty_internalization_env) c =
 
 let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c =
   let c = intern_gen (if as_type then IsType else WithoutTypeConstraint)
-            ~allow_patvar:true ~ltacvars env c in
+            ~pattern_mode:true ~ltacvars env c in
   pattern_of_glob_constr c
 
 let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 644f60d85..324f7a389 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -83,7 +83,7 @@ val intern_constr : env -> constr_expr -> glob_constr
 val intern_type : env -> constr_expr -> glob_constr
 
 val intern_gen : typing_constraint -> env ->
-  ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
+  ?impls:internalization_env -> ?pattern_mode:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> glob_constr
 
 val intern_pattern : env -> cases_pattern_expr ->
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli
index 835e94c77..ac0d96e96 100644
--- a/intf/evar_kinds.mli
+++ b/intf/evar_kinds.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Globnames
+open Misctypes
 
 (** The kinds of existential variable *)
 
@@ -16,6 +17,8 @@ open Globnames
 
 type obligation_definition_status = Define of bool | Expand
 
+type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar
+
 type t =
   | ImplicitArg of global_reference * (int * Id.t option)
      * bool (** Force inference *)
@@ -27,6 +30,6 @@ type t =
   | TomatchTypeParameter of inductive * int
   | GoalEvar
   | ImpossibleCase
-  | MatchingVar of bool * Id.t
+  | MatchingVar of matching_var_kind
   | VarInstance of Id.t
   | SubEvar of Constr.existential_key
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index 33c71884a..5da20c9d1 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -39,7 +39,7 @@ type glob_constr_r =
       (** An identifier that cannot be regarded as "GRef".
           Bound variables are typically represented this way. *)
   | GEvar   of existential_name * (Id.t * glob_constr) list
-  | GPatVar of bool * patvar (** Used for patterns only *)
+  | GPatVar of Evar_kinds.matching_var_kind (** Used for patterns only *)
   | GApp    of glob_constr * glob_constr list
   | GLambda of Name.t * binding_kind *  glob_constr * glob_constr
   | GProd   of Name.t * binding_kind * glob_constr * glob_constr
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 4946285e1..6581ac15e 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -142,7 +142,7 @@ let rec abstract_glob_constr c = function
 
 let interp_casted_constr_with_implicits env sigma impls c  =
   Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
-    ~allow_patvar:false c
+    c
 
 (*
    Construct a fixpoint as a Glob_term
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 0096abfa6..d201cf949 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -189,7 +189,7 @@ let intern_binding_name ist x =
      and if a term w/o ltac vars, check the name is indeed quantified *)
   x
 
-let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env; extra} c =
+let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} c =
   let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
   let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in
   let ltacvars = {
@@ -198,7 +198,7 @@ let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env; extra} c =
     ltac_extra = extra;
   } in
   let c' =
-    warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c
+    warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env) c
   in
   (c',if !strict_check then None else Some c)
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 594c4fa15..10c0319b2 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -589,7 +589,7 @@ let interp_uconstr ist env sigma = function
       } in
       { closure ; term =  intern_gen WithoutTypeConstraint ~ltacvars env ce }
 
-let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
+let interp_gen kind ist pattern_mode flags env sigma (c,ce) =
   let constrvars = extract_ltac_constr_context ist env sigma in
   let vars = {
     Pretyping.ltac_constrs = constrvars.typed;
@@ -617,7 +617,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
       } in
       let kind_for_intern =
         match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in
-      intern_gen kind_for_intern ~allow_patvar ~ltacvars env c
+      intern_gen kind_for_intern ~pattern_mode ~ltacvars env c
   in
   (* Jason Gross: To avoid unnecessary modifications to tacinterp, as
       suggested by Arnaud Spiwack, we run push_trace immediately.  We do
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 6fb1b6089..e53d19b59 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -12,6 +12,7 @@ open Nameops
 open Globnames
 open Misctypes
 open Glob_term
+open Evar_kinds
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
 
@@ -59,6 +60,11 @@ let cast_type_eq eq t1 t2 = match t1, t2 with
   | CastNative t1, CastNative t2 -> eq t1 t2
   | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> false
 
+let matching_var_kind_eq k1 k2 = match k1, k2 with
+| FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2
+| SecondOrderPatVar id1, SecondOrderPatVar id2 -> Id.equal id1 id2
+| (FirstOrderPatVar _ | SecondOrderPatVar _), _ -> false
+
 let tomatch_tuple_eq f (c1, p1) (c2, p2) =
   let eqp (_, (i1, na1)) (_, (i2, na2)) =
     eq_ind i1 i2 && List.equal Name.equal na1 na2
@@ -97,8 +103,7 @@ let mk_glob_constr_eq f { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with
   | GVar id1, GVar id2 -> Id.equal id1 id2
   | GEvar (id1, arg1), GEvar (id2, arg2) ->
     Id.equal id1 id2 && List.equal (instance_eq f) arg1 arg2
-  | GPatVar (b1, pat1), GPatVar (b2, pat2) ->
-    (b1 : bool) == b2 && Id.equal pat1 pat2
+  | GPatVar k1, GPatVar k2 -> matching_var_kind_eq k1 k2
   | GApp (f1, arg1), GApp (f2, arg2) ->
     f f1 f2 && List.equal f arg1 arg2
   | GLambda (na1, bk1, t1, c1), GLambda (na2, bk2, t2, c2) ->
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 0818a5525..71dbc39f3 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -143,7 +143,7 @@ let pattern_of_constr env sigma t =
           match kind_of_term f with
           | Evar (evk,args) ->
             (match snd (Evd.evar_source evk sigma) with
-              Evar_kinds.MatchingVar (true,id) -> Some id
+              Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar id) -> Some id
             | _ -> None)
           | _ -> None
          with
@@ -156,13 +156,14 @@ let pattern_of_constr env sigma t =
       pattern_of_constr env (EConstr.Unsafe.to_constr (Retyping.expand_projection env sigma p (EConstr.of_constr c) []))
     | Evar (evk,ctxt as ev) ->
       (match snd (Evd.evar_source evk sigma) with
-      | Evar_kinds.MatchingVar (b,id) ->
-        assert (not b); PMeta (Some id)
+      | Evar_kinds.MatchingVar (Evar_kinds.FirstOrderPatVar id) ->
+        PMeta (Some id)
       | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ ->
         (* These are the two evar kinds used for existing goals *)
         (* see Proofview.mark_in_evm *)
          if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value sigma ev)
          else PEvar (evk,Array.map (pattern_of_constr env) ctxt)
+      | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
       | _ -> 
 	 PMeta None)
     | Case (ci,p,a,br) ->
@@ -329,12 +330,12 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function
   | GVar id ->
       (try PRel (List.index Name.equal (Name id) vars)
        with Not_found -> PVar id)
-  | GPatVar (false,n) ->
+  | GPatVar (Evar_kinds.FirstOrderPatVar n) ->
       metas := n::!metas; PMeta (Some n)
   | GRef (gr,_) ->
       PRef (canonical_gr gr)
   (* Hack to avoid rewriting a complete interpretation of patterns *)
-  | GApp ({ CAst.v = GPatVar (true,n) }, cl) ->
+  | GApp ({ CAst.v = GPatVar (Evar_kinds.SecondOrderPatVar n) }, cl) ->
       metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
   | GApp (c,cl) ->
       PApp (pat_of_raw metas vars c,
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b0663af70..1839c87b1 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -625,13 +625,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in
 	inh_conv_coerce_to_tycon ?loc env evdref j tycon
 
-  | GPatVar (someta,n) ->
+  | GPatVar kind ->
     let env = ltac_interp_name_env k0 lvar env !evdref in
     let ty =
       match tycon with
       | Some ty -> ty
       | None -> new_type_evar env evdref loc in
-    let k = Evar_kinds.MatchingVar (someta,n) in
+    let k = Evar_kinds.MatchingVar kind in
       { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
 
   | GHole (k, naming, None) ->
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 2ba18ceb4..d15a0724d 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -260,7 +260,7 @@ let mkGProd id c1 c2 = CAst.make @@
 let mkGArrow c1 c2 = CAst.make @@
   GProd (Anonymous, Explicit, c1, c2)
 let mkGVar id = CAst.make @@ GVar (Id.of_string id)
-let mkGPatVar id = CAst.make @@ GPatVar((false, Id.of_string id))
+let mkGPatVar id = CAst.make @@ GPatVar(Evar_kinds.FirstOrderPatVar (Id.of_string id))
 let mkGRef r = CAst.make @@ GRef (Lazy.force r, None)
 let mkGAppRef r args = mkGApp (mkGRef r) args