Source file constr_matching.ml

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(*i*)
open Pp
open CErrors
open Util
open Names
open Constr
open Context
open Termops
open EConstr
open Vars
open Pattern
open Patternops
open Context.Rel.Declaration
open Ltac_pretype
(*i*)

let error_instantiate_pattern id l =
  let is = match l with
  | [_] -> "is"
  | _ -> "are"
  in
  user_err  (str "Cannot substitute the term bound to " ++ Id.print id
    ++ strbrk " in pattern because the term refers to " ++ pr_enum Id.print l
    ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")

type instantiated_pattern = constr_pattern

let instantiate_pattern env sigma lvar c =
  let open EConstr in
  let open Vars in
  let rec aux vars = function
  | PVar id as x ->
      (try
        let ctx,c = Id.Map.find id lvar in
        try
          let inst =
            List.map
              (fun id -> mkRel (List.index Name.equal (Name id) vars))
              ctx
          in
          let c = substl inst c in
          pattern_of_constr env sigma c
        with Not_found (* List.index failed *) ->
          let vars =
            List.map_filter (function Name id -> Some id | _ -> None) vars in
          error_instantiate_pattern id (List.subtract Id.equal ctx vars)
       with Not_found (* Map.find failed *) ->
         x)
  | c ->
      map_pattern_with_binders (fun id vars -> id::vars) aux vars c in
  if Id.Map.is_empty lvar then c else aux [] c

(* Given a term with second-order variables in it,
   represented by Meta's, and possibly applied using [SOAPP] to
   terms, this function will perform second-order, binding-preserving,
   matching, in the case where the pattern is a pattern in the sense
   of Dale Miller.

   ALGORITHM:

   Given a pattern, we decompose it, flattening Cast's and apply's,
   recursing on all operators, and pushing the name of the binder each
   time we descend a binder.

   When we reach a first-order variable, we ask that the corresponding
   term's free-rels all be higher than the depth of the current stack.

   When we reach a second-order application, we ask that the
   intersection of the free-rels of the term and the current stack be
   contained in the arguments of the application, and in that case, we
   construct a LAMBDA with the names on the stack.

 *)

type binding_bound_vars = Id.Set.t
type bound_ident_map = Id.t Id.Map.t

exception PatternMatchingFailure

let warn_meta_collision =
  CWarnings.create ~name:"meta-collision" ~category:"ltac"
         (fun name ->
          strbrk "Collision between bound variable " ++ Id.print name ++
            strbrk " and a metavariable of same name.")


let constrain sigma n (ids, m) ((names,seen as names_seen), terms as subst) =
  let open EConstr in
  try
    let (ids', m') = Id.Map.find n terms in
    if List.equal Id.equal ids ids' && eq_constr sigma m m' then subst
    else raise PatternMatchingFailure
  with Not_found ->
    let () = if Id.Map.mem n names then warn_meta_collision n in
    (names_seen, Id.Map.add n (ids, m) terms)

let add_binders na1 na2 binding_vars ((names,seen), terms as subst) =
  match na1, na2.binder_name with
  | Name id1, Name id2 when Id.Set.mem id1 binding_vars ->
    if Id.Map.mem id1 names then
      let () = Glob_ops.warn_variable_collision id1 in
      subst
    else
      let id2 = Namegen.next_ident_away id2 seen in
      let names = Id.Map.add id1 id2 names in
      let seen = Id.Set.add id2 seen in
      let () = if Id.Map.mem id1 terms then
        warn_meta_collision id1 in
      ((names,seen), terms)
  | _ -> subst

let rec build_lambda sigma vars ctx m = match vars with
| [] ->
  if Vars.closed0 sigma m then m else raise PatternMatchingFailure
| n :: vars ->
  (* change [ x1 ... xn y z1 ... zm |- t ] into
     [ x1 ... xn z1 ... zm |- lam y. t ] *)
  let pre, suf = List.chop (pred n) ctx in
  let (na, t, suf) = match suf with
  | [] -> assert false
  | (_, id, t) :: suf ->
     (map_annot Name.mk_name id, t, suf)
  in
  (* Check that the abstraction is legal by generating a transitive closure of
     its dependencies. *)
  let is_nondep t clear = match clear with
  | [] -> true
  | _ ->
    let rels = free_rels sigma t in
    let check i b = b || not (Int.Set.mem i rels) in
    List.for_all_i check 1 clear
  in
  let fold (_, _, t) clear = is_nondep t clear :: clear in
  (* Produce a list of booleans: true iff we keep the hypothesis *)
  let clear = List.fold_right fold pre [false] in
  let clear = List.drop_last clear in
  (* If the conclusion depends on a variable we cleared, failure *)
  let () = if not (is_nondep m clear) then raise PatternMatchingFailure in
  (* Create the abstracted term *)
  let fold (k, accu) keep =
    if keep then
      let k = succ k in
      (k, Some k :: accu)
    else (k, None :: accu)
  in
  let keep, shift = List.fold_left fold (0, []) clear in
  let shift = List.rev shift in
  let map = function
  | None -> mkProp (* dummy term *)
  | Some i -> mkRel (i + 1)
  in
  (* [x1 ... xn y z1 ... zm] -> [x1 ... xn f(z1) ... f(zm) y] *)
  let subst =
    List.map map shift @
    mkRel 1 ::
    List.mapi (fun i _ -> mkRel (i + keep + 2)) suf
  in
  let map i (na, id, c) =
    let i = succ i in
    let subst = List.skipn i subst in
    let subst = List.map (fun c -> Vars.lift (- i) c) subst in
    (na, id, substl subst c)
  in
  let pre = List.mapi map pre in
  let pre = List.filter_with clear pre in
  let m = substl subst m in
  let map i =
    if i > n then i - n + keep
    else match List.nth shift (i - 1) with
    | None ->
      (* We cleared a variable that we wanted to abstract! *)
      raise PatternMatchingFailure
    | Some k -> k
  in
  let vars = List.map map vars in
  (* Create the abstraction *)
  let m = mkLambda (na, Vars.lift keep t, m) in
  build_lambda sigma vars (pre @ suf) m

let rec extract_bound_aux k accu frels ctx = match ctx with
| [] -> accu
| (na, _, _) :: ctx ->
  if Int.Set.mem k frels then
    begin match na with
    | Name id ->
      let () = if Id.Set.mem id accu then raise PatternMatchingFailure in
      extract_bound_aux (k + 1) (Id.Set.add id accu) frels ctx
    | Anonymous -> raise PatternMatchingFailure
    end
  else extract_bound_aux (k + 1) accu frels ctx

let extract_bound_vars frels ctx =
  extract_bound_aux 1 Id.Set.empty frels ctx

let dummy_constr = EConstr.mkProp

let make_renaming ids = function
| (Name id, _, _) ->
  begin
    try EConstr.mkRel (List.index Id.equal id ids)
    with Not_found -> dummy_constr
  end
| _ -> dummy_constr

let push_binder na1 na2 t ctx =
  let id2 = map_annot (function
      | Name id2 -> id2
      | Anonymous ->
        let avoid = Id.Set.of_list (List.map (fun (_,id,_) -> id.binder_name) ctx) in
        Namegen.next_ident_away Namegen.default_non_dependent_ident avoid) na2
  in
  (na1, id2, t) :: ctx

(* This is an optimization of the main pattern-matching which shares
   the longest common prefix of the body and type of a fixpoint. The
   only practical effect at the time of writing is in binding variable
   names: these variable names must be bound only once since the user
   view at a fix displays only a (maximal) shared common prefix *)

let rec match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env' subst t1 t2 b1 b2 =
  match t1, EConstr.kind sigma t2, b1, EConstr.kind sigma b2 with
  | PProd(na1,c1,t1'), Prod(na2,c2,t2'), PLambda (_,c1',b1'), Lambda (na2',c2',b2') ->
     let ctx = push_binder na1 na2 c2 ctx in
     let ctx' = push_binder na1 na2' c2' ctx' in
     let env = EConstr.push_rel (LocalAssum (na2,c2)) env in
     let subst = sorec ctx env subst c1 c2 in
     let subst = sorec ctx env subst c1' c2' in
     let subst = add_binders na1 na2 binding_vars subst in
     match_under_common_fix_binders sorec sigma binding_vars
       ctx ctx' env env' subst t1' t2' b1' b2'
  | PLetIn(na1,c1,u1,t1), LetIn(na2,c2,u2,t2), PLetIn(_,c1',u1',b1), LetIn(na2',c2',u2',b2) ->
     let ctx = push_binder na1 na2 u2 ctx in
     let ctx' = push_binder na1 na2' u2' ctx' in
     let env = EConstr.push_rel (LocalDef (na2,c2,t2)) env in
     let subst = sorec ctx env subst c1 c2 in
     let subst = sorec ctx env subst c1' c2' in
     let subst = Option.fold_left (fun subst u1 -> sorec ctx env subst u1 u2) subst u1 in
     let subst = Option.fold_left (fun subst u1' -> sorec ctx env subst u1' u2') subst u1' in
     let subst = add_binders na1 na2 binding_vars subst in
     match_under_common_fix_binders sorec sigma binding_vars
       ctx ctx' env env' subst t1 t2 b1 b2
  | _ ->
     sorec ctx' env' (sorec ctx env subst t1 t2) b1 b2

let merge_binding sigma allow_bound_rels ctx n cT subst =
  let c = match ctx with
  | [] -> (* Optimization *)
    ([], cT)
  | _ ->
    let frels = free_rels sigma cT in
    if allow_bound_rels then
      let vars = extract_bound_vars frels ctx in
      let ordered_vars = Id.Set.elements vars in
      let rename binding = make_renaming ordered_vars binding in
      let renaming = List.map rename ctx in
      (ordered_vars, Vars.substl renaming cT)
    else
      let depth = List.length ctx in
      let min_elt = try Int.Set.min_elt frels with Not_found -> succ depth in
      if depth < min_elt then
        ([], Vars.lift (- depth) cT)
      else raise PatternMatchingFailure
  in
  constrain sigma n c subst

let matches_core env sigma allow_bound_rels
    (binding_vars,pat) c =
  let open EConstr in
  let convref ref c =
    let open GlobRef in
    match ref, EConstr.kind sigma c with
    | VarRef id, Var id' -> Names.Id.equal id id'
    | ConstRef c, Const (c',_) -> Environ.QConstant.equal env c c'
    | IndRef i, Ind (i', _) -> Names.Ind.CanOrd.equal i i'
    | ConstructRef c, Construct (c',u) -> Names.Construct.CanOrd.equal c c'
    | _, _ -> false
  in
  let rec sorec ctx env subst p t =
    let cT = strip_outer_cast sigma t in
    match p, EConstr.kind sigma cT with
      | PSoApp (n,args),m ->
        let fold (ans, seen) = function
        | PRel n ->
          let () = if Int.Set.mem n seen then user_err (str "Non linear second-order pattern") in
          (n :: ans, Int.Set.add n seen)
        | _ -> user_err (str "Only bound indices allowed in second order pattern matching.")
        in
        let relargs, relset = List.fold_left fold ([], Int.Set.empty) args in
        let frels = free_rels sigma cT in
        if Int.Set.subset frels relset then
          constrain sigma n ([], build_lambda sigma relargs ctx cT) subst
        else
          raise PatternMatchingFailure

      | PMeta (Some n), m -> merge_binding sigma allow_bound_rels ctx n cT subst

      | PMeta None, m -> subst

      | PRef (GlobRef.VarRef v1), Var v2 when Id.equal v1 v2 -> subst

      | PVar v1, Var v2 when Id.equal v1 v2 -> subst

      | PRef ref, _ when convref ref cT -> subst

      | PRel n1, Rel n2 when Int.equal n1 n2 -> subst

      | PSort ps, Sort s ->
        if Sorts.family_equal ps (Sorts.family (ESorts.kind sigma s))
        then subst else raise PatternMatchingFailure

      | PApp (p, [||]), _ -> sorec ctx env subst p t

      | PApp (PApp (h, a1), a2), _ ->
          sorec ctx env subst (PApp(h,Array.append a1 a2)) t

      | PApp (PMeta meta,args1), App (c2,args2) ->
         (let diff = Array.length args2 - Array.length args1 in
          if diff >= 0 then
            let args21, args22 = Array.chop diff args2 in
            let c = mkApp(c2,args21) in
            let subst =
              match meta with
              | None -> subst
              | Some n -> merge_binding sigma allow_bound_rels ctx n c subst in
            Array.fold_left2 (sorec ctx env) subst args1 args22
          else (* Might be a projection on the right *)
            match EConstr.kind sigma c2 with
            | Proj (pr, c) ->
              (try let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in
                     sorec ctx env subst p term
               with Retyping.RetypeError _ -> raise PatternMatchingFailure)
            | _ -> raise PatternMatchingFailure)

      | PApp (c1,arg1), App (c2,arg2) ->
        (match c1, EConstr.kind sigma c2 with
         | PRef (GlobRef.ConstRef r), Proj (pr,c)
           when not (Environ.QConstant.equal env r (Projection.constant pr)) ->
           raise PatternMatchingFailure
        | PProj (pr1,c1), Proj (pr,c) ->
          if Environ.QProjection.equal env pr1 pr then
            try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c) arg1 arg2
            with Invalid_argument _ -> raise PatternMatchingFailure
          else raise PatternMatchingFailure
        | _, Proj (pr,c) ->
          (try let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in
                 sorec ctx env subst p term
           with Retyping.RetypeError _ -> raise PatternMatchingFailure)
        | _, _ ->
          try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c2) arg1 arg2
          with Invalid_argument _ -> raise PatternMatchingFailure)

      | PApp (PRef (GlobRef.ConstRef c1), _), Proj (pr, c2)
        when not (Environ.QConstant.equal env c1 (Projection.constant pr)) ->
        raise PatternMatchingFailure

      | PApp (c, args), Proj (pr, c2) ->
        (try let term = Retyping.expand_projection env sigma pr c2 [] in
               sorec ctx env subst p term
         with Retyping.RetypeError _ -> raise PatternMatchingFailure)

      | PProj (p1,c1), Proj (p2,c2) when Environ.QProjection.equal env p1 p2 ->
          sorec ctx env subst c1 c2

      | PProd (na1,c1,d1), Prod(na2,c2,d2) ->
          sorec (push_binder na1 na2 c2 ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env)
            (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2

      | PLambda (na1,c1,d1), Lambda(na2,c2,d2) ->
          sorec (push_binder na1 na2 c2 ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env)
            (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2

      | PLetIn (na1,c1,Some t1,d1), LetIn(na2,c2,t2,d2) ->
          sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env)
            (add_binders na1 na2 binding_vars (sorec ctx env (sorec ctx env subst c1 c2) t1 t2)) d1 d2

      | PLetIn (na1,c1,None,d1), LetIn(na2,c2,t2,d2) ->
          sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env)
            (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2

      | PIf (a1,b1,b1'), Case (ci, u2, pms2, p2, iv, a2, ([|b2;b2'|] as br2)) ->
          let (_, _, _, p2, _, _, br2) = EConstr.annotate_case env sigma (ci, u2, pms2, p2, iv, a2, br2) in
          let ctx_b2,b2 = br2.(0) in
          let ctx_b2',b2' = br2.(1) in
          let n = Context.Rel.length ctx_b2 in
          let n' = Context.Rel.length ctx_b2' in
          if Vars.noccur_between sigma 1 n b2 && Vars.noccur_between sigma 1 n' b2' then
            let f l (LocalAssum (na,t) | LocalDef (na,_,t)) = push_binder Anonymous na t l in
            let ctx_br = List.fold_left f ctx ctx_b2 in
            let ctx_br' = List.fold_left f ctx ctx_b2' in
            let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
            sorec ctx_br' (push_rel_context ctx_b2' env)
              (sorec ctx_br (push_rel_context ctx_b2 env)
                 (sorec ctx env subst a1 a2) b1 b2) b1' b2'
          else
            raise PatternMatchingFailure

      | PCase (ci1, p1, a1, br1), Case (ci2, u2, pms2, p2, iv, a2, br2) ->
          let (_, _, _, p2, _, _, br2) = EConstr.annotate_case env sigma (ci2, u2, pms2, p2, iv, a2, br2) in
          let n2 = Array.length br2 in
          let () = match ci1.cip_ind with
          | None -> ()
          | Some ind1 ->
            (* ppedrot: Something spooky going here. The comparison used to be
               the generic one, so I may have broken something. *)
            if not (Ind.CanOrd.equal ind1 ci2.ci_ind) then raise PatternMatchingFailure
          in
          let () =
            if not ci1.cip_extensible && not (Int.equal (List.length br1) n2)
            then raise PatternMatchingFailure
          in
          let sorec_under_ctx subst (n, c1) (decls, c2) =
            let env = push_rel_context decls env in
            let rec fold (ctx, subst) nas decls = match nas, decls with
            | [], _ ->
              (* Historical corner case: less bound variables are allowed in
                destructuring let-bindings. See #13735. *)
                (ctx, subst)
            | na1 :: nas, d :: decls ->
              let na2 = Context.Rel.Declaration.get_annot d in
              let t = Context.Rel.Declaration.get_type d in
              let ctx = push_binder na1 na2 t ctx in
              let subst = add_binders na1 na2 binding_vars subst in
              fold (ctx, subst) nas decls
            | _, [] ->
              assert false
            in
            let ctx, subst = fold (ctx, subst) (Array.to_list n) (List.rev decls) in
            sorec ctx env subst c1 c2
          in
          let chk_branch subst (j,n,c) =
            (* (ind,j+1) is normally known to be a correct constructor
               and br2 a correct match over the same inductive *)
            assert (j < n2);
            sorec_under_ctx subst (n, c) br2.(j)
          in
          let subst = sorec ctx env subst a1 a2 in
          let subst = match p1 with
          | None -> subst
          | Some p1 -> sorec_under_ctx subst p1 p2
          in
          List.fold_left chk_branch subst br1

      |	PFix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(lna2,tl2,bl2))
           when Array.equal Int.equal ln1 ln2 && i1 = i2 ->
          let ctx' = Array.fold_left3 (fun ctx na1 na2 t2 -> push_binder na1 na2 t2 ctx) ctx lna1 lna2 tl2 in
          let env' = Array.fold_left2 (fun env na2 c2 -> EConstr.push_rel (LocalAssum (na2,c2)) env) env lna2 tl2 in
          let subst = Array.fold_left4 (match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env') subst tl1 tl2 bl1 bl2 in
          Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2

      |	PCoFix (i1,(lna1,tl1,bl1)), CoFix (i2,(lna2,tl2,bl2))
           when i1 = i2 ->
          let ctx' = Array.fold_left3 (fun ctx na1 na2 t2 -> push_binder na1 na2 t2 ctx) ctx lna1 lna2 tl2 in
          let env' = Array.fold_left2 (fun env na2 c2 -> EConstr.push_rel (LocalAssum (na2,c2)) env) env lna2 tl2 in
          let subst = Array.fold_left4 (match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env') subst tl1 tl2 bl1 bl2 in
          Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2

      | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 ->
         List.fold_left2 (sorec ctx env) subst args1 args2
      | PInt i1, Int i2 when Uint63.equal i1 i2 -> subst

      | PFloat f1, Float f2 when Float64.equal f1 f2 -> subst

      | PArray(pt,pdef,pty), Array(_u,t,def,ty)
             when Array.length pt = Array.length t ->
         sorec ctx env (sorec ctx env (Array.fold_left2 (sorec ctx env) subst pt t) pdef def) pty ty

      | (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _
         | PProd _ | PLetIn _ | PSort _ | PIf _ | PCase _
         | PFix _ | PCoFix _| PEvar _ | PInt _ | PFloat _ | PArray _), _ -> raise PatternMatchingFailure

  in
  sorec [] env ((Id.Map.empty,Id.Set.empty), Id.Map.empty) pat c

let matches_core_closed env sigma pat c =
  let names, subst = matches_core env sigma false pat c in
  (fst names, Id.Map.map snd subst)

let extended_matches env sigma pat c =
  let (names,_), subst = matches_core env sigma true pat c in
  names, subst

let matches env sigma pat c =
  snd (matches_core_closed env sigma (Id.Set.empty,pat) c)

type context = constr Lazy.t

let special_meta = (-1)

let empty_context = Lazy.from_val (mkMeta special_meta)
let repr_context c = Lazy.force c
let instantiate_context ctxt c =
  let ctxt = EConstr.Unsafe.to_constr (Lazy.force ctxt) in
  let c = EConstr.Unsafe.to_constr c in
  EConstr.of_constr (subst_meta [special_meta, c] ctxt)

type matching_result =
    { m_sub : bound_ident_map * patvar_map;
      m_ctx : context; }

let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) )

let isPMeta = function PMeta _ -> true | _ -> false

let matches_head env sigma pat c =
  let open EConstr in
  let head =
    match pat, EConstr.kind sigma c with
    | PApp (c1,arg1), App (c2,arg2) ->
        if isPMeta c1 then c else
        let n1 = Array.length arg1 in
        if n1 < Array.length arg2 then mkApp (c2,Array.sub arg2 0 n1) else c
    | c1, App (c2,arg2) when not (isPMeta c1) -> c2
    | _ -> c in
  matches env sigma pat head

(* Tells if it is an authorized occurrence and if the instance is closed *)
let authorized_occ env sigma closed pat c mk_ctx =
  try
    let subst = matches_core_closed env sigma pat c in
    if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst)
    then (fun next -> next ())
    else (fun next -> mkresult subst (lazy (mk_ctx (mkMeta special_meta))) next)
  with PatternMatchingFailure -> (fun next -> next ())

let subargs env v = Array.map_to_list (fun c -> (env, c)) v

(* Tries to match a subterm of [c] with [pat] *)
let sub_match ?(closed=true) env sigma pat c =
  let open EConstr in
  let rec aux env c mk_ctx next =
  let here = authorized_occ env sigma closed pat c mk_ctx in
  let next () = match EConstr.kind sigma c with
  | Cast (c1,k,c2) ->
      let next_mk_ctx = function
      | [c1] -> mk_ctx (mkCast (c1, k, c2))
      | _ -> assert false
      in
      try_aux [env, c1] next_mk_ctx next
  | Lambda (x,c1,c2) ->
      let next_mk_ctx = function
      | [c1; c2] -> mk_ctx (mkLambda (x, c1, c2))
      | _ -> assert false
      in
      let env' = EConstr.push_rel (LocalAssum (x,c1)) env in
      try_aux [(env, c1); (env', c2)] next_mk_ctx next
  | Prod (x,c1,c2) ->
      let next_mk_ctx = function
      | [c1; c2] -> mk_ctx (mkProd (x, c1, c2))
      | _ -> assert false
      in
      let env' = EConstr.push_rel (LocalAssum (x,c1)) env in
      try_aux [(env, c1); (env', c2)] next_mk_ctx next
  | LetIn (x,c1,t,c2) ->
      let next_mk_ctx = function
      | [c1; c2] -> mk_ctx (mkLetIn (x, c1, t, c2))
      | _ -> assert false
      in
      let env' = EConstr.push_rel (LocalDef (x,c1,t)) env in
      try_aux [(env, c1); (env', c2)] next_mk_ctx next
  | App (c1,lc) ->
     let lc1 = Array.sub lc 0 (Array.length lc - 1) in
     let app = mkApp (c1,lc1) in
     let mk_ctx = function
       | [app';c] -> mk_ctx (mkApp (app',[|c|]))
       | _ -> assert false in
     try_aux [(env, app); (env, Array.last lc)] mk_ctx next
  | Case (ci,u,pms,hd0,iv,c1,lc0) ->
      let (mib, mip) = Inductive.lookup_mind_specif env ci.ci_ind in
      let (_, hd, _, _, br) = expand_case env sigma (ci, u, pms, hd0, iv, c1, lc0) in
      let hd =
        let (ctx, hd) = decompose_lam_assum sigma hd in
        (push_rel_context ctx env, hd)
      in
      let map i br =
        let decls = mip.Declarations.mind_consnrealdecls.(i) in
        let (ctx, c) = decompose_lam_n_decls sigma decls br in
        (push_rel_context ctx env, c)
      in
      let lc = Array.to_list (Array.mapi map br) in
      let next_mk_ctx = function
      | c1 :: rem ->
        let pms, rem = List.chop (Array.length pms) rem in
        let pms = Array.of_list pms in
        let hd, lc = match rem with [] -> assert false | x :: l -> (x, l) in
        let hd = (fst hd0, hd) in
        let map_br (nas, _) br = (nas, br) in
        mk_ctx (mkCase (ci,u,pms,hd,iv,c1,Array.map2 map_br lc0 (Array.of_list lc)))
      | _ -> assert false
      in
      let sub = (env, c1) :: Array.fold_right (fun c accu -> (env, c) :: accu) pms (hd :: lc) in
      try_aux sub next_mk_ctx next
  | Fix (indx,(names,types,bodies as recdefs)) ->
    let nb_fix = Array.length types in
    let next_mk_ctx le =
      let (ntypes,nbodies) = CList.chop nb_fix le in
      mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in
    let env' = push_rec_types recdefs env in
    let sub = subargs env types @ subargs env' bodies in
    try_aux sub next_mk_ctx next
  | CoFix (i,(names,types,bodies as recdefs)) ->
    let nb_fix = Array.length types in
    let next_mk_ctx le =
      let (ntypes,nbodies) = CList.chop nb_fix le in
      mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in
    let env' = push_rec_types recdefs env in
    let sub = subargs env types @ subargs env' bodies in
    try_aux sub next_mk_ctx next
  | Proj (p,c') ->
    begin match Retyping.expand_projection env sigma p c' [] with
    | term -> aux env term mk_ctx next
    | exception Retyping.RetypeError _ -> next ()
    end
  | Array(u, t, def, ty) ->
    let next_mk_ctx = function
    | def :: ty :: l -> mk_ctx (mkArray(u, Array.of_list l, def, ty))
    | _ -> assert false
    in
    let sub = (env,def) :: (env,ty) :: subargs env t in
    try_aux sub next_mk_ctx next
  | Construct _|Ind _|Evar _|Const _|Rel _|Meta _|Var _|Sort _|Int _|Float _ ->
    next ()
  in
  here next

  (* Tries [sub_match] for all terms in the list *)
  and try_aux lc mk_ctx next =
    let rec try_sub_match_rec lacc lc =
      match lc with
      | [] -> next ()
      | (env, c) :: tl ->
        let mk_ctx ce = mk_ctx (List.rev_append lacc (ce :: List.map snd tl)) in
        let next () = try_sub_match_rec (c :: lacc) tl in
        aux env c mk_ctx next
    in
    try_sub_match_rec [] lc in
  let lempty () = IStream.Nil in
  let result () = aux env c (fun x -> x) lempty in
  IStream.thunk result

let match_subterm env sigma pat c = sub_match env sigma pat c

let is_matching env sigma pat c =
  try let _ = matches env sigma pat c in true
  with PatternMatchingFailure -> false

let is_matching_head env sigma pat c =
  try let _ = matches_head env sigma pat c in true
  with PatternMatchingFailure -> false

let is_matching_appsubterm ?(closed=true) env sigma pat c =
  let pat = (Id.Set.empty,pat) in
  let results = sub_match ~closed env sigma pat c in
  not (IStream.is_empty results)