Dnets now consider axioms as being opaque for pattern recognition.

1 files changed, 42 insertions, 25 deletions

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