Quelle constr_matching.ml Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq 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:CWarnings.CoreCategories.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 rec sorec ctx env subst (p:constr_pattern) 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 EConstr.isRefX env sigma ref cT -> subst

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

      | PSort ps, Sort s ->
        if UnivGen.QualityOrSet.equal ps (ESorts.quality_or_set 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 (Environ.QInd.equal env 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 ->
        let args2 = Evd.expand_existential sigma (c2, args2) in
         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

      | PString s1, String s2 when Pstring.equal s1 s2 -> 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 _
         | PString _ | PArray _), _ -> raise PatternMatchingFailure

      | PUninstantiated _, _ -> .

  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,hdr), _, _, br) = expand_case env sigma (ci, u, pms, hd0, iv, c1, lc0) in
      let hd =
        let (ctx, hd) = decompose_lambda_decls 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_lambda_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 (fst hd0), hd) in
        let map_br (nas, _) br = (nas, br) in
        mk_ctx (mkCase (ci,u,pms,(hd,hdr),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 _|String _ ->
    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)

quality98%

¤ Dauer der Verarbeitung: 0.17 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.