Dnets now consider axioms as being opaque for pattern recognition.

7 files changed, 91 insertions, 71 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 488bcb5208..784322679f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -266,7 +266,7 @@ let flags_of_state st =
 let auto_flags_of_state st =
   auto_unif_flags_of TransparentState.full st
 
-let hintmap_of sigma secvars hdc concl =
+let hintmap_of env sigma secvars hdc concl =
   match hdc with
   | None -> Hint_db.map_none ~secvars
   | Some hdc ->
@@ -274,7 +274,7 @@ let hintmap_of sigma secvars hdc concl =
        (fun db -> match Hint_db.map_existential sigma ~secvars hdc concl db with
                   | ModeMatch l -> l
                   | ModeMismatch -> [])
-     else Hint_db.map_auto sigma ~secvars hdc concl
+     else Hint_db.map_auto env sigma ~secvars hdc concl
 
 let exists_evaluable_reference env = function
   | EvalConstRef _ -> true
@@ -300,23 +300,24 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
   Proofview.Goal.enter begin fun gl ->
     let concl = Tacmach.New.pf_concl gl in
     let sigma = Tacmach.New.project gl in
+    let env = Proofview.Goal.env gl in
     let secvars = compute_secvars gl in
     Tacticals.New.tclFIRST
       ((dbg_assumption dbg)::intro_tac::
           (List.map Tacticals.New.tclCOMPLETE
-             (trivial_resolve sigma dbg mod_delta db_list local_db secvars concl)))
+             (trivial_resolve env sigma dbg mod_delta db_list local_db secvars concl)))
   end
 
-and my_find_search_nodelta sigma db_list local_db secvars hdc concl =
+and my_find_search_nodelta env sigma db_list local_db secvars hdc concl =
   List.map (fun hint -> (None,hint))
-    (List.map_append (hintmap_of sigma secvars hdc concl) (local_db::db_list))
+    (List.map_append (hintmap_of env sigma secvars hdc concl) (local_db::db_list))
 
 and my_find_search mod_delta =
   if mod_delta then my_find_search_delta
   else my_find_search_nodelta
 
-and my_find_search_delta sigma db_list local_db secvars hdc concl =
-  let f = hintmap_of sigma secvars hdc concl in
+and my_find_search_delta env sigma db_list local_db secvars hdc concl =
+  let f = hintmap_of env sigma secvars hdc concl in
     if occur_existential sigma concl then
       List.map_append
         (fun db ->
@@ -340,7 +341,7 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
               | None -> Hint_db.map_none ~secvars db
               | Some hdc ->
                   if TransparentState.is_empty st
-                  then Hint_db.map_auto sigma ~secvars hdc concl db
+                  then Hint_db.map_auto env sigma ~secvars hdc concl db
                   else match Hint_db.map_existential sigma ~secvars hdc concl db with
                       | ModeMatch l -> l
                       | ModeMismatch -> []
@@ -381,7 +382,7 @@ and tac_of_hint dbg db_list local_db concl (flags, h) =
   in
   tclLOG dbg pr_hint (FullHint.run h tactic)
 
-and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl =
+and trivial_resolve env sigma dbg mod_delta db_list local_db secvars cl =
   try
     let head =
       try let hdconstr = decompose_app_bound sigma cl in
@@ -390,7 +391,7 @@ and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl =
     in
       List.map (tac_of_hint dbg db_list local_db cl)
         (priority
-            (my_find_search mod_delta sigma db_list local_db secvars head cl))
+            (my_find_search mod_delta env sigma db_list local_db secvars head cl))
   with Not_found -> []
 
 (** The use of the "core" database can be de-activated by passing
@@ -430,7 +431,7 @@ let h_trivial ?(debug=Off) lems l = gen_trivial ~debug lems l
 (*                       The classical Auto tactic                        *)
 (**************************************************************************)
 
-let possible_resolve sigma dbg mod_delta db_list local_db secvars cl =
+let possible_resolve env sigma dbg mod_delta db_list local_db secvars cl =
   try
     let head =
       try let hdconstr = decompose_app_bound sigma cl in
@@ -438,7 +439,7 @@ let possible_resolve sigma dbg mod_delta db_list local_db secvars cl =
       with Bound -> None
     in
       List.map (tac_of_hint dbg db_list local_db cl)
-        (my_find_search mod_delta sigma db_list local_db secvars head cl)
+        (my_find_search mod_delta env sigma db_list local_db secvars head cl)
   with Not_found -> []
 
 let extend_local_db decl db gl =
@@ -473,12 +474,13 @@ let search d n mod_delta db_list local_db =
              ( Proofview.Goal.enter begin fun gl ->
                let concl = Tacmach.New.pf_concl gl in
                let sigma = Tacmach.New.project gl in
+               let env = Proofview.Goal.env gl in
                let secvars = compute_secvars gl in
                let d' = incr_dbg d in
                Tacticals.New.tclFIRST
                  (List.map
                     (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db))
-                    (possible_resolve sigma d mod_delta db_list local_db secvars concl))
+                    (possible_resolve env sigma d mod_delta db_list local_db secvars concl))
              end))
     end []
   in
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 1f148e01fa..bacb5a7b8f 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -49,17 +49,25 @@ let decomp sigma t =
   in
     decrec [] t
 
-let constr_val_discr sigma t =
+let evaluable_constant c env =
+  (* This is a hack to work around a broken Print Module implementation, see
+     bug #2668. *)
+  if Environ.mem_constant c env then Environ.evaluable_constant c env
+  else true
+
+let constr_val_discr env sigma t =
   let open GlobRef in
   let c, l = decomp sigma t in
     match EConstr.kind sigma c with
     | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l)
     | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l)
     | Var id -> Label(GRLabel (VarRef id),l)
-    | Const _ -> Everything
+    | Const (c, _) ->
+      if evaluable_constant c env then Everything
+      else Label(GRLabel (ConstRef c),l)
     | _ -> Nothing
 
-let constr_pat_discr t =
+let constr_pat_discr env t =
   if not (Patternops.occur_meta_pattern t) then
     None
   else
@@ -68,16 +76,23 @@ let constr_pat_discr t =
     | PRef ((IndRef _) as ref), args
     | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
     | PRef ((VarRef v) as ref), args -> Some(GRLabel ref,args)
+    | PRef ((ConstRef c) as ref), args ->
+      if evaluable_constant c env then None
+      else Some (GRLabel ref, args)
     | _ -> None
 
-let constr_val_discr_st sigma ts t =
+let constr_val_discr_st env sigma ts t =
   let c, l = decomp sigma t in
   let open GlobRef in
     match EConstr.kind sigma c with
-    | Const (c,u) -> if TransparentState.is_transparent_constant ts c then Everything else Label(GRLabel (ConstRef c),l)
+    | Const (c,u) ->
+      if evaluable_constant c env && TransparentState.is_transparent_constant ts c then Everything
+      else Label(GRLabel (ConstRef c),l)
     | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l)
     | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l)
-    | Var id -> if TransparentState.is_transparent_variable ts id then Everything else Label(GRLabel (VarRef id),l)
+    | Var id ->
+      if Environ.evaluable_named id env && TransparentState.is_transparent_variable ts id then Everything
+      else Label(GRLabel (VarRef id),l)
     | Prod (n, d, c) -> Label(ProdLabel, [d; c])
     | Lambda (n, d, c) ->
       if List.is_empty l then
@@ -88,52 +103,54 @@ let constr_val_discr_st sigma ts t =
     | Rel _ | Meta _ | Cast _ | LetIn _ | App _ | Case _ | Fix _ | CoFix _
     | Proj _ | Int _ | Float _ | Array _ -> Nothing
 
-let constr_pat_discr_st ts t =
+let constr_pat_discr_st env ts t =
   let open GlobRef in
   match decomp_pat t with
   | PRef ((IndRef _) as ref), args
   | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
-  | PRef ((VarRef v) as ref), args when not (TransparentState.is_transparent_variable ts v) ->
-      Some(GRLabel ref,args)
+  | PRef ((VarRef v) as ref), args ->
+    if Environ.evaluable_named v env && (TransparentState.is_transparent_variable ts v) then None
+    else Some(GRLabel ref,args)
+  | PRef ((ConstRef c) as ref), args ->
+    if evaluable_constant c env && TransparentState.is_transparent_constant ts c then None
+    else Some (GRLabel ref, args)
   | PVar v, args when not (TransparentState.is_transparent_variable ts v) ->
       Some(GRLabel (VarRef v),args)
-  | PRef ((ConstRef c) as ref), args when not (TransparentState.is_transparent_constant ts c) ->
-      Some (GRLabel ref, args)
   | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c])
   | PLambda (_, d, c), [] -> Some (LambdaLabel, [d ; c])
   | PSort s, [] -> Some (SortLabel, [])
   | _ -> None
 
-let bounded_constr_pat_discr_st st (t,depth) =
+let bounded_constr_pat_discr_st env st (t,depth) =
   if Int.equal depth 0 then
     None
   else
-    match constr_pat_discr_st st t with
+    match constr_pat_discr_st env st t with
       | None -> None
       | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
 
-let bounded_constr_val_discr_st sigma st (t,depth) =
+let bounded_constr_val_discr_st env sigma st (t,depth) =
   if Int.equal depth 0 then
     Nothing
   else
-    match constr_val_discr_st sigma st t with
+    match constr_val_discr_st env sigma st t with
       | Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l)
       | Nothing -> Nothing
       | Everything -> Everything
 
-let bounded_constr_pat_discr (t,depth) =
+let bounded_constr_pat_discr env (t,depth) =
   if Int.equal depth 0 then
     None
   else
-    match constr_pat_discr t with
+    match constr_pat_discr env t with
       | None -> None
       | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
 
-let bounded_constr_val_discr sigma (t,depth) =
+let bounded_constr_val_discr env sigma (t,depth) =
   if Int.equal depth 0 then
     Nothing
   else
-    match constr_val_discr sigma t with
+    match constr_val_discr env sigma t with
       | Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l)
       | Nothing -> Nothing
       | Everything -> Everything
@@ -153,21 +170,21 @@ struct
 
   type pattern = Dn.pattern
 
-  let pattern st pat = match st with
-  | None -> Dn.pattern bounded_constr_pat_discr (pat, !dnet_depth)
-  | Some st -> Dn.pattern (bounded_constr_pat_discr_st st) (pat, !dnet_depth)
+  let pattern env st pat = match st with
+  | None -> Dn.pattern (bounded_constr_pat_discr env) (pat, !dnet_depth)
+  | Some st -> Dn.pattern (bounded_constr_pat_discr_st env st) (pat, !dnet_depth)
 
   let empty = Dn.empty
   let add = Dn.add
   let rmv = Dn.rmv
 
-  let lookup sigma = function
+  let lookup env sigma = function
     | None ->
         (fun dn t ->
-             Dn.lookup dn (bounded_constr_val_discr sigma) (t,!dnet_depth))
+             Dn.lookup dn (bounded_constr_val_discr env sigma) (t,!dnet_depth))
     | Some st ->
         (fun dn t ->
-             Dn.lookup dn (bounded_constr_val_discr_st sigma st) (t,!dnet_depth))
+             Dn.lookup dn (bounded_constr_val_discr_st env sigma st) (t,!dnet_depth))
 
   let app f dn = Dn.app f dn
 
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 2caa193202..ab201a1872 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -30,14 +30,14 @@ sig
 
   type pattern
 
-  val pattern : TransparentState.t option -> constr_pattern -> pattern
+  val pattern : Environ.env -> TransparentState.t option -> constr_pattern -> pattern
 
   val empty : t
 
   val add : t -> pattern -> Z.t -> t
   val rmv : t -> pattern -> Z.t -> t
 
-  val lookup : Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list
+  val lookup : Environ.env -> Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list
   val app : (Z.t -> unit) -> t -> unit
 end
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 378a3e718b..2f55cc071f 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -257,13 +257,13 @@ let shelve_dependencies gls =
      Feedback.msg_debug (str" shelving dependent subgoals: " ++ pr_gls sigma gls);
    shelve_goals gls)
 
-let hintmap_of sigma hdc secvars concl =
+let hintmap_of env sigma hdc secvars concl =
   match hdc with
   | None -> fun db -> ModeMatch (Hint_db.map_none ~secvars db)
   | Some hdc ->
      fun db ->
        if Hint_db.use_dn db then (* Using dnet *)
-         Hint_db.map_eauto sigma ~secvars hdc concl db
+         Hint_db.map_eauto env sigma ~secvars hdc concl db
       else Hint_db.map_existential sigma ~secvars hdc concl db
 
 (** Hack to properly solve dependent evars that are typeclasses *)
@@ -373,7 +373,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
         | Extern _ -> (tac, b, true, name, lazy (FullHint.print env sigma h ++ pp))
         | _ -> (tac, b, false, name, lazy (FullHint.print env sigma h ++ pp))
   in
-  let hint_of_db = hintmap_of sigma hdc secvars concl in
+  let hint_of_db = hintmap_of env sigma hdc secvars concl in
   let hintl = List.map_filter (fun db -> match hint_of_db db with
       | ModeMatch l -> Some (db, l)
       | ModeMismatch -> None)
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 17e6a6edb4..e920093648 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -67,7 +67,7 @@ open Auto
 let unify_e_resolve flags h =
   Hints.hint_res_pf ~with_evars:true ~with_classes:true ~flags h
 
-let hintmap_of sigma secvars concl =
+let hintmap_of env sigma secvars concl =
   (* Warning: for computation sharing, we need to return a closure *)
   let hdc = try Some (decompose_app_bound sigma concl) with Bound -> None in
   match hdc with
@@ -78,7 +78,7 @@ let hintmap_of sigma secvars concl =
           match Hint_db.map_existential sigma ~secvars hdc concl db with
           | ModeMatch l -> l
           | ModeMismatch -> [])
-     else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db)
+     else (fun db -> Hint_db.map_auto env sigma ~secvars hdc concl db)
    (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
 
 let e_exact flags h =
@@ -106,7 +106,7 @@ let rec e_trivial_fail_db db_list local_db =
   end
 
 and e_my_find_search env sigma db_list local_db secvars concl =
-  let hint_of_db = hintmap_of sigma secvars concl in
+  let hint_of_db = hintmap_of env sigma secvars concl in
   let hintl =
       List.map_append (fun db ->
         let flags = auto_flags_of_state (Hint_db.transparent_state db) in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 4532f97a27..7d065df19b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -243,7 +243,7 @@ sig
   type t
   val empty : t
   val add : TransparentState.t option -> t -> Pattern.constr_pattern -> stored_data -> t
-  val lookup : Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> stored_data list
+  val lookup : Environ.env -> Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> stored_data list
 end =
 struct
   module Data = struct type t = stored_data let compare = pri_order_int end
@@ -257,18 +257,18 @@ struct
 
   let add st net p v = ref (Diff ((st, p, v), net))
 
-  let rec force net = match !net with
+  let rec force env net = match !net with
   | Bnet dn -> dn
   | Diff ((st, p, v), rem) ->
-    let dn = force rem in
-    let p = Bnet.pattern st p in
+    let dn = force env rem in
+    let p = Bnet.pattern env st p in
     let dn = Bnet.add dn p v in
     let () = net := (Bnet dn) in
     dn
 
-  let lookup sigma st net p =
-    let dn = force net in
-    Bnet.lookup sigma st dn p
+  let lookup env sigma st net p =
+    let dn = force env net in
+    Bnet.lookup env sigma st dn p
 end
 
 type search_entry = {
@@ -307,8 +307,8 @@ let rebuild_dn st se =
   in
   { se with sentry_bnet = dn' }
 
-let lookup_tacs sigma concl st se =
-  let l'  = Bounded_net.lookup sigma st se.sentry_bnet concl in
+let lookup_tacs env sigma concl st se =
+  let l'  = Bounded_net.lookup env sigma st se.sentry_bnet concl in
   let sl' = List.stable_sort pri_order_int l' in
   List.merge pri_order_int se.sentry_nopat sl'
 
@@ -529,14 +529,14 @@ val map_none : secvars:Id.Pred.t -> t -> full_hint list
 val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
 val map_existential : evar_map -> secvars:Id.Pred.t ->
                       (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode
-val map_eauto : evar_map -> secvars:Id.Pred.t ->
+val map_eauto : Environ.env -> evar_map -> secvars:Id.Pred.t ->
                 (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode
-val map_auto : evar_map -> secvars:Id.Pred.t ->
+val map_auto : Environ.env -> evar_map -> secvars:Id.Pred.t ->
                (GlobRef.t * constr array) -> constr -> t -> full_hint list
 val add_one : env -> evar_map -> hint_entry -> t -> t
 val add_list : env -> evar_map -> hint_entry list -> t -> t
-val remove_one : GlobRef.t -> t -> t
-val remove_list : GlobRef.t list -> t -> t
+val remove_one : Environ.env -> GlobRef.t -> t -> t
+val remove_list : Environ.env -> GlobRef.t list -> t -> t
 val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit
 val use_dn : t -> bool
 val transparent_state : t -> TransparentState.t
@@ -629,10 +629,10 @@ struct
     merge_entry secvars db se.sentry_nopat se.sentry_pat
 
   (* Precondition: concl has no existentials *)
-  let map_auto sigma ~secvars (k,args) concl db =
+  let map_auto env sigma ~secvars (k,args) concl db =
     let se = find k db in
     let st = if db.use_dn then  (Some db.hintdb_state) else None in
-    let pat = lookup_tacs sigma concl st se in
+    let pat = lookup_tacs env sigma concl st se in
     merge_entry secvars db [] pat
 
   let map_existential sigma ~secvars (k,args) concl db =
@@ -642,11 +642,11 @@ struct
       else ModeMismatch
 
   (* [c] contains an existential *)
-  let map_eauto sigma ~secvars (k,args) concl db =
+  let map_eauto env sigma ~secvars (k,args) concl db =
     let se = find k db in
       if matches_modes sigma args se.sentry_mode then
         let st = if db.use_dn then Some db.hintdb_state else None in
-        let pat = lookup_tacs sigma concl st se in
+        let pat = lookup_tacs env sigma concl st se in
         ModeMatch (merge_entry secvars db [] pat)
       else ModeMismatch
 
@@ -720,14 +720,14 @@ struct
     if sl1' == se.sentry_nopat && sl2' == se.sentry_pat then se
     else rebuild_dn st { se with sentry_nopat = sl1'; sentry_pat = sl2' }
 
-  let remove_list grs db =
+  let remove_list env grs db =
     let filter (_, h) =
       match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in
     let hintmap = GlobRef.Map.map (remove_he db.hintdb_state filter) db.hintdb_map in
     let hintnopat = List.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
       { db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
 
-  let remove_one gr db = remove_list [gr] db
+  let remove_one env gr db = remove_list env [gr] db
 
   let get_entry se =
     let h = List.merge pri_order_int se.sentry_nopat se.sentry_pat in
@@ -1044,8 +1044,9 @@ let add_transparency dbname target b =
   in searchtable_add (dbname, Hint_db.set_transparent_state db st')
 
 let remove_hint dbname grs =
+  let env = Global.env () in
   let db = get_db dbname in
-  let db' = Hint_db.remove_list grs db in
+  let db' = Hint_db.remove_list env grs db in
     searchtable_add (dbname, db')
 
 type hint_action =
@@ -1463,7 +1464,7 @@ let pr_hint_term env sigma cl =
               (fun db -> match Hint_db.map_existential sigma ~secvars:Id.Pred.full hdc cl db with
               | ModeMatch l -> l
               | ModeMismatch -> [])
-            else Hint_db.map_auto sigma ~secvars:Id.Pred.full hdc cl
+            else Hint_db.map_auto env sigma ~secvars:Id.Pred.full hdc cl
         with Bound -> Hint_db.map_none ~secvars:Id.Pred.full
       in
       let fn db = List.map (fun x -> 0, x) (fn db) in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 0b9da27ab3..e061bd7648 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -134,18 +134,18 @@ module Hint_db :
     (** All hints associated to the reference, respecting modes if evars appear in the
         arguments and using the discrimination net.
         Returns a [ModeMismatch] if there are declared modes and none matches. *)
-    val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> FullHint.t list with_mode
+    val map_eauto : env -> evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> FullHint.t list with_mode
 
     (** All hints associated to the reference.
         Precondition: no evars should appear in the arguments, so no modes
         are checked. *)
-    val map_auto : evar_map -> secvars:Id.Pred.t ->
+    val map_auto : env -> evar_map -> secvars:Id.Pred.t ->
        (GlobRef.t * constr array) -> constr -> t -> FullHint.t list
 
     val add_one : env -> evar_map -> hint_entry -> t -> t
     val add_list : env -> evar_map -> hint_entry list -> t -> t
-    val remove_one : GlobRef.t -> t -> t
-    val remove_list : GlobRef.t list -> t -> t
+    val remove_one : Environ.env -> GlobRef.t -> t -> t
+    val remove_list : Environ.env -> GlobRef.t list -> t -> t
     val iter : (GlobRef.t option ->
                 hint_mode array list -> FullHint.t list -> unit) -> t -> unit