Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: order_strength.prf   Sprache: SML

Untersuchung Coq©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \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)         *)
(************************************************************************)

open Pp
open CErrors
open Util
open Names
open Nameops
open Namegen
open Constr
open Context
open EConstr
open Vars
open Reduction
open Tacticals.New
open Tactics
open Pretype_errors
open Typeclasses
open Classes
open Constrexpr
open Globnames
open Evd
open Tactypes
open Locus
open Locusops
open Decl_kinds
open Elimschemes
open Environ
open Termops
open EConstr
open Libnames
open Proofview.Notations
open Context.Named.Declaration

module NamedDecl = Context.Named.Declaration
(* module RelDecl = Context.Rel.Declaration *)

(** Typeclass-based generalized rewriting. *)

type rewrite_attributes = { polymorphic : bool; program : bool; global : bool }

let rewrite_attributes =
  let open Attributes.Notations in
  Attributes.(polymorphic ++ program ++ locality) >>= fun ((polymorphic, program), locality) ->
  let global = not (Locality.make_section_locality locality) in
  Attributes.Notations.return { polymorphic; program; global }

(** Constants used by the tactic. *)

let classes_dirpath =
  Names.DirPath.make (List.map Id.of_string ["Classes";"Coq"])

let init_relation_classes () =
  if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
  else Coqlib.check_required_library ["Coq";"Classes";"RelationClasses"]

let init_setoid () =
  if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
  else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"]

let find_reference dir s =
  Coqlib.find_reference "generalized rewriting" dir s
[@@warning "-3"]

let lazy_find_reference dir s =
  let gr = lazy (find_reference dir s) in
  fun () -> Lazy.force gr

type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)

let find_global dir s =
  let gr = lazy (find_reference dir s) in
    fun (evd,cstrs) ->
      let (evd, c) = Evarutil.new_global evd (Lazy.force gr) in
 (evd, cstrs), c

(** Utility for dealing with polymorphic applications *)

(** Global constants. *)

let coq_eq_ref  () = Coqlib.lib_ref    "core.eq.type"
let coq_eq      = find_global    ["Coq""Init""Logic""eq"
let coq_f_equal = find_global    ["Coq""Init""Logic""f_equal"
let coq_all     = find_global    ["Coq""Init""Logic""all"
let impl        = find_global    ["Coq""Program""Basics""impl"

(** Bookkeeping which evars are constraints so that we can
    remove them at the end of the tactic. *)


let goalevars evars = fst evars
let cstrevars evars = snd evars

let new_cstr_evar (evd,cstrs) env t =
  (* We handle the typeclass resolution of constraints ourselves *)
  let (evd', t) = Evarutil.new_evar env evd ~typeclass_candidate:false t in
  let ev, _ = destEvar evd' t in
    (evd', Evar.Set.add ev cstrs), t

(** Building or looking up instances. *)
let e_new_cstr_evar env evars t =
  let evd', t = new_cstr_evar !evars env t in evars := evd'; t

(** Building or looking up instances. *)

let extends_undefined evars evars' =
  let f ev evi found = found || not (Evd.mem evars ev)
  in fold_undefined f evars' false

let app_poly_check env evars f args =
  let (evars, cstrs), fc = f evars in
  let evars, t = Typing.solve_evars env evars (mkApp (fc, args)) in
  (evars, cstrs), t

let app_poly_nocheck env evars f args =
  let evars, fc = f evars in 
    evars, mkApp (fc, args)

let app_poly_sort b =
  if b then app_poly_nocheck
  else app_poly_check
    
let find_class_proof proof_type proof_method env evars carrier relation =
  try
    let evars, goal = app_poly_check env evars proof_type [| carrier ; relation |] in
    let evars', c = Typeclasses.resolve_one_typeclass env (goalevars evars) goal in
      if extends_undefined (goalevars evars) evars' then raise Not_found
      else app_poly_check env (evars',cstrevars evars) proof_method [| carrier; relation; c |]
  with e when Logic.catchable_exception e -> raise Not_found
 
(** Utility functions *)

module GlobalBindings (M : sig
  val relation_classes : string list
  val morphisms : string list
  val relation : string list * string
  val app_poly : env -> evars -> (evars -> evars * constr) -> constr array -> evars * constr
  val arrow : evars -> evars * constr
end) = struct
  open M
  open Context.Rel.Declaration
  let relation : evars -> evars * constr = find_global (fst relation) (snd relation)

  let reflexive_type = find_global relation_classes "Reflexive"
  let reflexive_proof = find_global relation_classes "reflexivity"
    
  let symmetric_type = find_global relation_classes "Symmetric"
  let symmetric_proof = find_global relation_classes "symmetry"

  let transitive_type = find_global relation_classes "Transitive"
  let transitive_proof = find_global relation_classes "transitivity"

  let forall_relation = find_global morphisms "forall_relation"
  let pointwise_relation = find_global morphisms "pointwise_relation"

  let forall_relation_ref = lazy_find_reference morphisms "forall_relation"
  let pointwise_relation_ref = lazy_find_reference morphisms "pointwise_relation"

  let respectful = find_global morphisms "respectful"
  let respectful_ref = lazy_find_reference morphisms "respectful"

  let default_relation = find_global ["Coq""Classes""SetoidTactics""DefaultRelation"

  let coq_forall = find_global morphisms "forall_def"

  let subrelation = find_global relation_classes "subrelation"
  let do_subrelation = find_global morphisms "do_subrelation"
  let apply_subrelation = find_global morphisms "apply_subrelation"

  let rewrite_relation_class = find_global relation_classes "RewriteRelation"

  let proper_class = lazy (class_info (find_reference morphisms "Proper"))
  let proper_proxy_class = lazy (class_info (find_reference morphisms "ProperProxy"))
    
  let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs))))
    
  let proper_type = 
    let l = lazy (Lazy.force proper_class).cl_impl in
      fun (evd,cstrs) -> 
        let (evd, c) = Evarutil.new_global evd (Lazy.force l) in
   (evd, cstrs), c
 
  let proper_proxy_type = 
    let l = lazy (Lazy.force proper_proxy_class).cl_impl in
      fun (evd,cstrs) -> 
        let (evd, c) = Evarutil.new_global evd (Lazy.force l) in
   (evd, cstrs), c

  let proper_proof env evars carrier relation x =
    let evars, goal = app_poly env evars proper_proxy_type [| carrier ; relation; x |] in
      new_cstr_evar evars env goal

  let get_reflexive_proof env = find_class_proof reflexive_type reflexive_proof env
  let get_symmetric_proof env = find_class_proof symmetric_type symmetric_proof env
  let get_transitive_proof env = find_class_proof transitive_type transitive_proof env

  let mk_relation env evd a = 
    app_poly env evd relation [| a |]

  (** Build an inferred signature from constraints on the arguments and expected output
      relation *)

    
  let build_signature evars env m (cstrs : (types * types optionoption list)
      (finalcstr : (types * types optionoption) =
    let mk_relty evars newenv ty obj =
      match obj with
      | None | Some (_, None) ->
 let evars, relty = mk_relation env evars ty in
   if closed0 (goalevars evars) ty then 
     let env' = Environ.reset_with_named_context (Environ.named_context_val env) env in
       new_cstr_evar evars env' relty
   else new_cstr_evar evars newenv relty
      | Some (x, Some rel) -> evars, rel
    in
    let rec aux env evars ty l =
      let t = Reductionops.whd_all env (goalevars evars) ty in
 match EConstr.kind (goalevars evars) t, l with
        | Prod (na, ty, b), obj :: cstrs ->
          let b = Reductionops.nf_betaiota env (goalevars evars) b in
          if noccurn (goalevars evars) 1 b (* non-dependent product *) then
            let ty = Reductionops.nf_betaiota env (goalevars evars) ty in
     let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
     let evars, relty = mk_relty evars env ty obj in
     let evars, newarg = app_poly env evars respectful [| ty ; b' ; relty ; arg |] in
              evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs
   else
     let (evars, b, arg, cstrs) =
              aux (push_rel (LocalAssum (na, ty)) env) evars b cstrs
     in
            let ty = Reductionops.nf_betaiota env (goalevars evars) ty in
            let pred = mkLambda (na, ty, b) in
            let liftarg = mkLambda (na, ty, arg) in
            let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in
              if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
       else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument")
 | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products.")
 | _, [] ->
   (match finalcstr with
   | None | Some (_, None) ->
            let t = Reductionops.nf_betaiota env (fst evars) ty in
     let evars, rel = mk_relty evars env t None in
       evars, t, rel, [t, Some rel]
   | Some (t, Some rel) -> evars, t, rel, [t, Some rel])
    in aux env evars m cstrs

  (** Folding/unfolding of the tactic constants. *)

  let unfold_impl sigma t =
    match EConstr.kind sigma t with
    | App (arrow, [| a; b |])(*  when eq_constr arrow (Lazy.force impl) *) ->
      mkProd (make_annot Anonymous Sorts.Relevant, a, lift 1 b)
    | _ -> assert false

  let unfold_all sigma t =
    match EConstr.kind sigma t with
    | App (id, [| a; b |]) (* when eq_constr id (Lazy.force coq_all) *) ->
      (match EConstr.kind sigma b with
      | Lambda (n, ty, b) -> mkProd (n, ty, b)
      | _ -> assert false)
    | _ -> assert false

  let unfold_forall sigma t =
    match EConstr.kind sigma t with
    | App (id, [| a; b |]) (* when eq_constr id (Lazy.force coq_all) *) ->
      (match EConstr.kind sigma b with
      | Lambda (n, ty, b) -> mkProd (n, ty, b)
      | _ -> assert false)
    | _ -> assert false

  let arrow_morphism env evd ta tb a b =
    let ap = is_Prop (goalevars evd) ta and bp = is_Prop (goalevars evd) tb in
      if ap && bp then app_poly env evd impl [| a; b |], unfold_impl
      else if ap then (* Domain in Prop, CoDomain in Type *)
 (app_poly env evd arrow [| a; b |]), unfold_impl
 (* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *)
      else if bp then (* Dummy forall *)
        (app_poly env evd coq_all [| a; mkLambda (make_annot Anonymous Sorts.Relevant, a, lift 1 b) |]), unfold_forall
      else (* None in Prop, use arrow *)
 (app_poly env evd arrow [| a; b |]), unfold_impl

  let rec decomp_pointwise sigma n c =
    if Int.equal n 0 then c
    else
      match EConstr.kind sigma c with
      | App (f, [| a; b; relb |]) when Termops.is_global sigma (pointwise_relation_ref ()) f ->
 decomp_pointwise sigma (pred n) relb
      | App (f, [| a; b; arelb |]) when Termops.is_global sigma (forall_relation_ref ()) f ->
 decomp_pointwise sigma (pred n) (Reductionops.beta_applist sigma (arelb, [mkRel 1]))
      | _ -> invalid_arg "decomp_pointwise"

  let rec apply_pointwise sigma rel = function
    | arg :: args ->
      (match EConstr.kind sigma rel with
      | App (f, [| a; b; relb |]) when Termops.is_global sigma (pointwise_relation_ref ()) f ->
 apply_pointwise sigma relb args
      | App (f, [| a; b; arelb |]) when Termops.is_global sigma (forall_relation_ref ()) f ->
 apply_pointwise sigma (Reductionops.beta_applist sigma (arelb, [arg])) args
      | _ -> invalid_arg "apply_pointwise")
    | [] -> rel

  let pointwise_or_dep_relation env evd n t car rel =
    if noccurn (goalevars evd) 1 car && noccurn (goalevars evd) 1 rel then
      app_poly env evd pointwise_relation [| t; lift (-1) car; lift (-1) rel |]
    else
      app_poly env evd forall_relation
        [| t; mkLambda (make_annot n Sorts.Relevant, t, car);
           mkLambda (make_annot n Sorts.Relevant, t, rel) |]

  let lift_cstr env evars (args : constr list) c ty cstr =
    let start evars env car =
      match cstr with
      | None | Some (_, None) -> 
 let evars, rel = mk_relation env evars car in
   new_cstr_evar evars env rel
      | Some (ty, Some rel) -> evars, rel
    in
    let rec aux evars env prod n = 
      if Int.equal n 0 then start evars env prod
      else
        let sigma = goalevars evars in
 match EConstr.kind sigma (Reductionops.whd_all env sigma prod) with
        | Prod (na, ty, b) ->
   if noccurn sigma 1 b then
     let b' = lift (-1) b in
     let evars, rb = aux evars env b' (pred n) in
       app_poly env evars pointwise_relation [| ty; b'; rb |]
   else
            let evars, rb = aux evars (push_rel (LocalAssum (na, ty)) env) b (pred n) in
       app_poly env evars forall_relation
                [| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |]
 | _ -> raise Not_found
    in 
    let rec find env c ty = function
      | [] -> None
      | arg :: args ->
 try let evars, found = aux evars env ty (succ (List.length args)) in
       Some (evars, found, c, ty, arg :: args)
 with Not_found ->
          let sigma = goalevars evars in
   let ty = Reductionops.whd_all env sigma ty in
   find env (mkApp (c, [| arg |])) (prod_applist sigma ty [arg]) args
    in find env c ty args

  let unlift_cstr env sigma = function
    | None -> None
    | Some codom -> Some (decomp_pointwise (goalevars sigma) 1 codom)

  (** Looking up declared rewrite relations (instances of [RewriteRelation]) *)
  let is_applied_rewrite_relation env sigma rels t =
    match EConstr.kind sigma t with
    | App (c, args) when Array.length args >= 2 ->
      let head = if isApp sigma c then fst (destApp sigma c) else c in
 if Termops.is_global sigma (coq_eq_ref ()) head then None
 else
   (try
    let params, args = Array.chop (Array.length args - 2) args in
    let env' = push_rel_context rels env in
    let (evars, (evar, _)) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in
    let evars, inst = 
      app_poly env (evars,Evar.Set.empty)
        rewrite_relation_class [| evar; mkApp (c, params) |] in
    let _ = Typeclasses.resolve_one_typeclass env' (goalevars evars) inst in
      Some (it_mkProd_or_LetIn t rels)
    with e when CErrors.noncritical e -> None)
  | _ -> None


end

(* let my_type_of env evars c = Typing.e_type_of env evars c *)
(* let mytypeofkey = CProfile.declare_profile "my_type_of";; *)
(* let my_type_of = CProfile.profile3 mytypeofkey my_type_of *)


let type_app_poly env env evd f args =
  let evars, c = app_poly_nocheck env evd f args in
  let evd', t = Typing.type_of env (goalevars evars) c in
    (evd', cstrevars evars), c

module PropGlobal = struct
  module Consts =
  struct 
    let relation_classes = ["Coq""Classes""RelationClasses"]
    let morphisms = ["Coq""Classes""Morphisms"]
    let relation = ["Coq""Relations";"Relation_Definitions"], "relation"
    let app_poly = app_poly_nocheck
    let arrow = find_global ["Coq""Program""Basics""arrow"
    let coq_inverse = find_global ["Coq""Program""Basics""flip"
  end

  module G = GlobalBindings(Consts)

  include G
  include Consts
  let inverse env evd car rel = 
    type_app_poly env env evd coq_inverse [| car ; car; mkProp; rel |]
      (* app_poly env evd coq_inverse [| car ; car; mkProp; rel |] *)

end

module TypeGlobal = struct
  module Consts = 
    struct 
      let relation_classes = ["Coq""Classes""CRelationClasses"]
      let morphisms = ["Coq""Classes""CMorphisms"]
      let relation = relation_classes, "crelation"
      let app_poly = app_poly_check
      let arrow = find_global ["Coq""Classes""CRelationClasses""arrow"
      let coq_inverse = find_global ["Coq""Classes""CRelationClasses""flip"
    end

  module G = GlobalBindings(Consts)
  include G
  include Consts


  let inverse env (evd,cstrs) car rel = 
    let (evd, sort) = Evarutil.new_Type ~rigid:Evd.univ_flexible evd in
      app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |]

end

let sort_of_rel env evm rel =
  ESorts.kind evm (Reductionops.sort_of_arity env evm (Retyping.get_type_of env evm rel))

let is_applied_rewrite_relation = PropGlobal.is_applied_rewrite_relation

(* let _ = *)
(*   Hook.set Equality.is_applied_rewrite_relation is_applied_rewrite_relation *)

let split_head = function
    hd :: tl -> hd, tl
  | [] -> assert(false)

let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') =
  let equal x y = Constr.equal (EConstr.Unsafe.to_constr x) (EConstr.Unsafe.to_constr y) in
  pb == pb' || (ty == ty' && equal x x' && equal y y')

let problem_inclusion x y =
  List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x

let evd_convertible env evd x y =
  try
    (* Unfortunately, the_conv_x might say they are unifiable even if some
       unsolvable constraints remain, so we check that this unification
       does not introduce any new problem. *)

    let _, pbs = Evd.extract_all_conv_pbs evd in
    let evd' = Evarconv.unify_delay env evd x y in
    let _, pbs' = Evd.extract_all_conv_pbs evd' in
    if evd' == evd || problem_inclusion pbs' pbs then Some evd'
    else None
  with e when CErrors.noncritical e -> None

let convertible env evd x y =
  Reductionops.is_conv_leq env evd x y

type hypinfo = {
  prf : constr;
  car : constr;
  rel : constr;
  sort : bool(* true = Prop; false = Type *)
  c1 : constr;
  c2 : constr;
  holes : Clenv.hole list;
}

let get_symmetric_proof b = 
  if b then PropGlobal.get_symmetric_proof else TypeGlobal.get_symmetric_proof

let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite.")

let rec decompose_app_rel env evd t = 
  (* Head normalize for compatibility with the old meta mechanism *)
  let t = Reductionops.whd_betaiota evd t in
  match EConstr.kind evd t with
  | App (f, [||]) -> assert false
  | App (f, [|arg|]) ->
    let (f', argl, argr) = decompose_app_rel env evd arg in
    let ty = Typing.unsafe_type_of env evd argl in
    let r = Retyping.relevance_of_type env evd ty in
    let f'' = mkLambda (make_annot (Name default_dependent_ident) r, ty,
      mkLambda (make_annot (Name (Id.of_string "y")) r, lift 1 ty,
        mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |])))
    in (f'', argl, argr)
  | App (f, args) ->
    let len = Array.length args in
    let fargs = Array.sub args 0 (Array.length args - 2) in
    let rel = mkApp (f, fargs) in
    rel, args.(len - 2), args.(len - 1)
  | _ -> error_no_relation ()

let decompose_app_rel env evd t =
  let (rel, t1, t2) = decompose_app_rel env evd t in
  let ty = Retyping.get_type_of env evd rel in
  let () = if not (Reductionops.is_arity env evd ty) then error_no_relation () in
  (rel, t1, t2)

let decompose_applied_relation env sigma (c,l) =
  let open Context.Rel.Declaration in
  let ctype = Retyping.get_type_of env sigma c in
  let find_rel ty =
    let sigma, cl = Clenv.make_evar_clause env sigma ty in
    let sigma = Clenv.solve_evar_clause env sigma true cl l in
    let { Clenv.cl_holes = holes; Clenv.cl_concl = t } = cl in
    let (equiv, c1, c2) = decompose_app_rel env sigma t in
    let ty1 = Retyping.get_type_of env sigma c1 in
    let ty2 = Retyping.get_type_of env sigma c2 in
    match evd_convertible env sigma ty1 ty2 with
    | None -> None
    | Some sigma ->
      let sort = sort_of_rel env sigma equiv in
      let args = Array.map_of_list (fun h -> h.Clenv.hole_evar) holes in
      let value = mkApp (c, args) in
        Some (sigma, { prf=value;
                car=ty1; rel = equiv; sort = Sorts.is_prop sort;
                c1=c1; c2=c2; holes })
  in
    match find_rel ctype with
    | Some c -> c
    | None ->
 let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *)
        match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with
 | Some c -> c
 | None -> user_err Pp.(str "Cannot find an homogeneous relation to rewrite.")

let rewrite_db = "rewrite"

let conv_transparent_state = TransparentState.cst_full

let rewrite_transparent_state () =
  Hints.Hint_db.transparent_state (Hints.searchtable_map rewrite_db)

let rewrite_core_unif_flags = {
  Unification.modulo_conv_on_closed_terms = None;
  Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
  Unification.use_evars_eagerly_in_conv_on_closed_terms = true;
  Unification.modulo_delta = TransparentState.empty;
  Unification.modulo_delta_types = TransparentState.full;
  Unification.check_applied_meta_types = true;
  Unification.use_pattern_unification = true;
  Unification.use_meta_bound_pattern_unification = true;
  Unification.allowed_evars = Unification.AllowAll;
  Unification.restrict_conv_on_strict_subterms = false;
  Unification.modulo_betaiota = false;
  Unification.modulo_eta = true;
}

(* Flags used for the setoid variant of "rewrite" and for the strategies
   "hints"/"old_hints"/"terms" of "rewrite_strat", and for solving pre-existing
   evars in "rewrite" (see unify_abs) *)

let rewrite_unif_flags =
  let flags = rewrite_core_unif_flags in {
  Unification.core_unify_flags = flags;
  Unification.merge_unify_flags = flags;
  Unification.subterm_unify_flags = flags;
  Unification.allow_K_in_toplevel_higher_order_unification = true;
  Unification.resolve_evars = true
  }

let rewrite_core_conv_unif_flags = {
  rewrite_core_unif_flags with
    Unification.modulo_conv_on_closed_terms = Some conv_transparent_state;
    Unification.modulo_delta_types = conv_transparent_state;
    Unification.modulo_betaiota = true
}

(* Fallback flags for the setoid variant of "rewrite" *)
let rewrite_conv_unif_flags =
  let flags = rewrite_core_conv_unif_flags in {
  Unification.core_unify_flags = flags;
  Unification.merge_unify_flags = flags;
  Unification.subterm_unify_flags = flags;
  Unification.allow_K_in_toplevel_higher_order_unification = true;
  Unification.resolve_evars = true
  }

(* Flags for "setoid_rewrite c"/"rewrite_strat -> c" *)
let general_rewrite_unif_flags () =
  let ts = rewrite_transparent_state () in
  let core_flags =
    { rewrite_core_unif_flags with
      Unification.modulo_conv_on_closed_terms = Some ts;
      Unification.use_evars_eagerly_in_conv_on_closed_terms = true;
      Unification.modulo_delta = ts;
      Unification.modulo_delta_types = TransparentState.full;
      Unification.modulo_betaiota = true }
  in {
    Unification.core_unify_flags = core_flags;
    Unification.merge_unify_flags = core_flags;
    Unification.subterm_unify_flags = { core_flags with Unification.modulo_delta = TransparentState.empty };
    Unification.allow_K_in_toplevel_higher_order_unification = true;
    Unification.resolve_evars = true
  }

let refresh_hypinfo env sigma (is, cb) =
  let sigma, cbl = Tacinterp.interp_open_constr_with_bindings is env sigma cb in
  let sigma, hypinfo = decompose_applied_relation env sigma cbl in
  let { c1; c2; car; rel; prf; sort; holes } = hypinfo in
  sigma, (car, rel, prf, c1, c2, holes, sort)

(** FIXME: write this in the new monad interface *)
let solve_remaining_by env sigma holes by =
  match by with
  | None -> sigma
  | Some tac ->
    let map h =
      if h.Clenv.hole_deps then None
      else match EConstr.kind sigma h.Clenv.hole_evar with
      | Evar (evk, _) ->
        Some evk
      | _ -> None
    in
    (* Only solve independent holes *)
    let indep = List.map_filter map holes in
    let ist = { Geninterp.lfun = Id.Map.empty
              ; poly = false
              ; extra = Geninterp.TacStore.empty } in
    let solve_tac = match tac with
    | Genarg.GenArg (Genarg.Glbwit tag, tac) ->
      Ftactic.run (Geninterp.interp tag ist tac) (fun _ -> Proofview.tclUNIT ())
    in
    let solve_tac = tclCOMPLETE solve_tac in
    let solve sigma evk =
      let evi =
        try Some (Evd.find_undefined sigma evk)
        with Not_found -> None
      in
      match evi with
      | None -> sigma
        (* Evar should not be defined, but just in case *)
      | Some evi ->
        let env = Environ.reset_with_named_context evi.evar_hyps env in
        let ty = evi.evar_concl in
        let name, poly = Id.of_string "rewrite"false in
        let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma ty solve_tac in
        Evd.define evk (EConstr.of_constr c) sigma
    in
    List.fold_left solve sigma indep

let no_constraints cstrs = 
  fun ev _ -> not (Evar.Set.mem ev cstrs)

let poly_inverse sort =
  if sort then PropGlobal.inverse else TypeGlobal.inverse

type rewrite_proof = 
  | RewPrf of constr * constr
  (** A Relation (R : rew_car -> rew_car -> Prop) and a proof of R rew_from rew_to *)

  | RewCast of cast_kind
  (** A proof of convertibility (with casts) *)

type rewrite_result_info = {
  rew_car : constr ;
  (** A type *)
  rew_from : constr ;
  (** A term of type rew_car *)
  rew_to : constr ;
  (** A term of type rew_car *)
  rew_prf : rewrite_proof ;
  (** A proof of rew_from == rew_to *)
  rew_evars : evars;
}

type rewrite_result =
| Fail
| Identity
| Success of rewrite_result_info

type 'a strategy_input = { state : 'a ; (* a parameter: for instance, a state *)
      env : Environ.env ;
      unfresh : Id.Set.t; (* Unfresh names *)
      term1 : constr ;
      ty1 : types ; (* first term and its type (convertible to rew_from) *)
      cstr : (bool (* prop *) * constr option) ;
      evars : evars }
        
type 'a pure_strategy = { strategy :
  'a strategy_input ->
  'a * rewrite_result (* the updated state and the "result" *) }

type strategy = unit pure_strategy

let symmetry env sort rew =
  let { rew_evars = evars; rew_car = car; } = rew in
  let (rew_evars, rew_prf) = match rew.rew_prf with
  | RewCast _ -> (rew.rew_evars, rew.rew_prf)
  | RewPrf (rel, prf) ->
    try
      let evars, symprf = get_symmetric_proof sort env evars car rel in
      let prf = mkApp (symprf, [| rew.rew_from ; rew.rew_to ; prf |]) in
      (evars, RewPrf (rel, prf))
    with Not_found ->
      let evars, rel = poly_inverse sort env evars car rel in
      (evars, RewPrf (rel, prf))
  in
  { rew with rew_from = rew.rew_to; rew_to = rew.rew_from; rew_prf; rew_evars; }

(* Matching/unifying the rewriting rule against [t] *)
let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs) by t =
  try
    let left = if l2r then c1 else c2 in
    let sigma = Unification.w_unify ~flags env sigma CONV left t in
    let sigma = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs)
      ~fail:true env sigma in
    let evd = solve_remaining_by env sigma holes by in
    let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta evd c) in
    let c1 = nf c1 and c2 = nf c2
    and rew_car = nf car and rel = nf rel
    and prf = nf prf in
    let ty1 = Retyping.get_type_of env evd c1 in
    let ty2 = Retyping.get_type_of env evd c2 in
    let () = if not (convertible env evd ty2 ty1) then raise Reduction.NotConvertible in
    let rew_evars = evd, cstrs in
    let rew_prf = RewPrf (rel, prf) in
    let rew = { rew_evars; rew_prf; rew_car; rew_from = c1; rew_to = c2; } in
    let rew = if l2r then rew else symmetry env sort rew in
    Some rew
  with 
  | e when Class_tactics.catchable e -> None
  | Reduction.NotConvertible -> None

let unify_abs (car, rel, prf, c1, c2) l2r sort env (sigma, cstrs) t =
  try
    let left = if l2r then c1 else c2 in
    (* The pattern is already instantiated, so the next w_unify is
       basically an eq_constr, except when preexisting evars occur in
       either the lemma or the goal, in which case the eq_constr also
       solved this evars *)

    let sigma = Unification.w_unify ~flags:rewrite_unif_flags env sigma CONV left t in
    let rew_evars = sigma, cstrs in
    let rew_prf = RewPrf (rel, prf) in
    let rew = { rew_car = car; rew_from = c1; rew_to = c2; rew_prf; rew_evars; } in
    let rew = if l2r then rew else symmetry env sort rew in
    Some rew
  with 
  | e when Class_tactics.catchable e -> None
  | Reduction.NotConvertible -> None

type rewrite_flags = { under_lambdas : bool; on_morphisms : bool }

let default_flags = { under_lambdas = true; on_morphisms = true; }

let get_opt_rew_rel = function RewPrf (rel, prf) -> Some rel | _ -> None

let new_global (evars, cstrs) gr =
  let (sigma,c) = Evarutil.new_global evars gr in
  (sigma, cstrs), c

let make_eq sigma =
  new_global sigma Coqlib.(lib_ref "core.eq.type")
let make_eq_refl sigma =
  new_global sigma Coqlib.(lib_ref "core.eq.refl")

let get_rew_prf evars r = match r.rew_prf with
  | RewPrf (rel, prf) -> evars, (rel, prf)
  | RewCast c ->
    let evars, eq = make_eq evars in
    let evars, eq_refl = make_eq_refl evars in
    let rel = mkApp (eq, [| r.rew_car |]) in
    evars, (rel, mkCast (mkApp (eq_refl, [| r.rew_car; r.rew_from |]),
           c, mkApp (rel, [| r.rew_from; r.rew_to |])))

let poly_subrelation sort = 
  if sort then PropGlobal.subrelation else TypeGlobal.subrelation

let resolve_subrelation env avoid car rel sort prf rel' res =
  if Termops.eq_constr (fst res.rew_evars) rel rel' then res
  else
    let evars, app = app_poly_check env res.rew_evars (poly_subrelation sort) [|car; rel; rel'|] in
    let evars, subrel = new_cstr_evar evars env app in
    let appsub = mkApp (subrel, [| res.rew_from ; res.rew_to ; prf |]) in
      { res with
 rew_prf = RewPrf (rel', appsub);
 rew_evars = evars }

let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) evars =
  let evars, morph_instance, proj, sigargs, m', args, args' =
    let first = match (Array.findi (fun _ b -> not (Option.is_empty b)) args') with
    | Some i -> i
    | None -> invalid_arg "resolve_morphism" in
    let morphargs, morphobjs = Array.chop first args in
    let morphargs', morphobjs' = Array.chop first args' in
    let appm = mkApp(m, morphargs) in
    let appmtype = Typing.unsafe_type_of env (goalevars evars) appm in
    let cstrs = List.map 
      (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf)) 
      (Array.to_list morphobjs')
    in
      (* Desired signature *)
    let evars, appmtype', signature, sigargs =
      if b then PropGlobal.build_signature evars env appmtype cstrs cstr
      else TypeGlobal.build_signature evars env appmtype cstrs cstr
    in
      (* Actual signature found *)
    let cl_args = [| appmtype' ; signature ; appm |] in
    let evars, app = app_poly_sort b env evars (if b then PropGlobal.proper_type else TypeGlobal.proper_type)
      cl_args in
    let env' =
      let dosub, appsub = 
 if b then PropGlobal.do_subrelation, PropGlobal.apply_subrelation 
 else TypeGlobal.do_subrelation, TypeGlobal.apply_subrelation
      in
 EConstr.push_named
          (LocalDef (make_annot (Id.of_string "do_subrelation") Sorts.Relevant,
              snd (app_poly_sort b env evars dosub [||]),
              snd (app_poly_nocheck env evars appsub [||])))
   env
    in
    let evars, morph = new_cstr_evar evars env' app in
      evars, morph, morph, sigargs, appm, morphobjs, morphobjs'
  in
  let projargs, subst, evars, respars, typeargs =
    Array.fold_left2
      (fun (acc, subst, evars, sigargs, typeargs') x y ->
 let (carrier, relation), sigargs = split_head sigargs in
   match relation with
   | Some relation ->
       let carrier = substl subst carrier
       and relation = substl subst relation in
       (match y with
       | None ->
    let evars, proof = 
      (if b then PropGlobal.proper_proof else TypeGlobal.proper_proof) 
        env evars carrier relation x in
      [ proof ; x ; x ] @ acc, subst, evars, sigargs, x :: typeargs'
       | Some r ->
                 let evars, proof = get_rew_prf evars r in
   [ snd proof; r.rew_to; x ] @ acc, subst, evars, 
       sigargs, r.rew_to :: typeargs')
   | None ->
       if not (Option.is_empty y) then 
  user_err Pp.(str "Cannot rewrite inside dependent arguments of a function");
       x :: acc, x :: subst, evars, sigargs, x :: typeargs')
      ([], [], evars, sigargs, []) args args'
  in
  let proof = applist (proj, List.rev projargs) in
  let newt = applist (m', List.rev typeargs) in
    match respars with
 [ a, Some r ] -> evars, proof, substl subst a, substl subst r, oldt, fnewt newt
      | _ -> assert(false)

let apply_constraint env avoid car rel prf cstr res =
  match snd cstr with
  | None -> res
  | Some r -> resolve_subrelation env avoid car rel (fst cstr) prf r res

let coerce env avoid cstr res = 
  let evars, (rel, prf) = get_rew_prf res.rew_evars res in
  let res = { res with rew_evars = evars } in
    apply_constraint env avoid res.rew_car rel prf cstr res

let apply_rule unify loccs : int pure_strategy =
  let (nowhere_except_in,occs) = convert_occs loccs in
  let is_occ occ =
    if nowhere_except_in 
    then List.mem occ occs 
    else not (List.mem occ occs) 
  in
  { strategy = fun { state = occ ; env ; unfresh ;
       term1 = t ; ty1 = ty ; cstr ; evars } ->
      let unif = if isEvar (goalevars evars) t then None else unify env evars t in
 match unif with
 | None -> (occ, Fail)
        | Some rew ->
   let occ = succ occ in
     if not (is_occ occ) then (occ, Fail)
     else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity)
     else
       let res = { rew with rew_car = ty } in
       let res = Success (coerce env unfresh cstr res) in
              (occ, res)
    }

let apply_lemma l2r flags oc by loccs : strategy = { strategy =
  fun ({ state = () ; env ; term1 = t ; evars = (sigma, cstrs) } as input) ->
    let sigma, c = oc sigma in
    let sigma, hypinfo = decompose_applied_relation env sigma c in
    let { c1; c2; car; rel; prf; sort; holes } = hypinfo in
    let rew = (car, rel, prf, c1, c2, holes, sort) in
    let evars = (sigma, cstrs) in
    let unify env evars t =
      let rew = unify_eqn rew l2r flags env evars by t in
      match rew with
      | None -> None
      | Some rew -> Some rew
    in
    let _, res = (apply_rule unify loccs).strategy { input with
           state = 0 ;
           evars } in
    (), res
         }

let e_app_poly env evars f args =
  let evars', c = app_poly_nocheck env !evars f args in
    evars := evars';
    c

let make_leibniz_proof env c ty r =
  let evars = ref r.rew_evars in
  let prf = 
    match r.rew_prf with
    | RewPrf (rel, prf) -> 
 let rel = e_app_poly env evars coq_eq [| ty |] in
 let prf =
   e_app_poly env evars coq_f_equal
  [| r.rew_car; ty;
                   mkLambda (make_annot Anonymous Sorts.Relevant, r.rew_car, c);
     r.rew_from; r.rew_to; prf |]
 in RewPrf (rel, prf)
    | RewCast k -> r.rew_prf
  in
    { rew_car = ty; rew_evars = !evars;
      rew_from = subst1 r.rew_from c; rew_to = subst1 r.rew_to c; rew_prf = prf }

let reset_env env =
  let env' = Global.env_of_context (Environ.named_context_val env) in
    Environ.push_rel_context (Environ.rel_context env) env'
      
let fold_match ?(force=false) env sigma c =
  let (ci, p, c, brs) = destCase sigma c in
  let cty = Retyping.get_type_of env sigma c in
  let dep, pred, exists, (sk,eff) = 
    let env', ctx, body =
      let ctx, pred = decompose_lam_assum sigma p in
      let env' = push_rel_context ctx env in
 env', ctx, pred
    in
    let sortp = Retyping.get_sort_family_of env' sigma body in
    let sortc = Retyping.get_sort_family_of env sigma cty in
    let dep = not (noccurn sigma 1 body) in
    let pred = if dep then p else
 it_mkProd_or_LetIn (subst1 mkProp body) (List.tl ctx)
    in
    let sk = 
      if sortp == Sorts.InProp then
 if sortc == Sorts.InProp then
   if dep then case_dep_scheme_kind_from_prop
   else case_scheme_kind_from_prop
 else (
          if dep
          then case_dep_scheme_kind_from_type_in_prop
          else case_scheme_kind_from_type)
      else ((* sortc <> InProp by typing *)
 if dep
 then case_dep_scheme_kind_from_type
 else case_scheme_kind_from_type)
    in 
    let exists = Ind_tables.check_scheme sk ci.ci_ind in
      if exists || force then
 dep, pred, exists, Ind_tables.find_scheme sk ci.ci_ind
      else raise Not_found
  in
  let app =
    let ind, args = Inductiveops.find_mrectype env sigma cty in
    let pars, args = List.chop ci.ci_npar args in
    let meths = List.map (fun br -> br) (Array.to_list brs) in
      applist (mkConst sk, pars @ [pred] @ meths @ args @ [c])
  in 
    sk, (if exists then env else reset_env env), app, eff

let unfold_match env sigma sk app =
  match EConstr.kind sigma app with
  | App (f', args) when Constant.equal (fst (destConst sigma f')) sk ->
      let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in
      let v = EConstr.of_constr v in
 Reductionops.whd_beta sigma (mkApp (v, args))
  | _ -> app

let is_rew_cast = function RewCast _ -> true | _ -> false

let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
  let rec aux { state ; env ; unfresh ;
  term1 = t ; ty1 = ty ; cstr = (prop, cstr) ; evars } =
    let cstr' = Option.map (fun c -> (ty, Some c)) cstr in
      match EConstr.kind (goalevars evars) t with
      | App (m, args) ->
   let rewrite_args state success =
     let state, (args', evars', progress) =
       Array.fold_left
  (fun (state, (acc, evars, progress)) arg ->
    if not (Option.is_empty progress) && not all then 
      state, (None :: acc, evars, progress)
    else
      let argty = Retyping.get_type_of env (goalevars evars) arg in
      let state, res = s.strategy { state ; env ;
        unfresh ;
        term1 = arg ; ty1 = argty ;
        cstr = (prop,None) ;
        evars } in
      let res' =
        match res with
        | Identity ->
   let progress = if Option.is_empty progress then Some false else progress in
     (None :: acc, evars, progress)
        | Success r -> 
   (Some r :: acc, r.rew_evars, Some true)
        | Fail -> (None :: acc, evars, progress)
      in state, res')
  (state, ([], evars, success)) args
     in
     let res = 
       match progress with
       | None -> Fail
       | Some false -> Identity
       | Some true ->
  let args' = Array.of_list (List.rev args'in
    if Array.exists
      (function 
        | None -> false 
        | Some r -> not (is_rew_cast r.rew_prf)) args'
    then
      let evars', prf, car, rel, c1, c2 =
        resolve_morphism env unfresh t m args args' (prop, cstr') evars'
      in
      let res = { rew_car = ty; rew_from = c1;
    rew_to = c2; rew_prf = RewPrf (rel, prf);
    rew_evars = evars' }
      in Success res
    else 
      let args' = Array.map2
        (fun aorig anew ->
   match anew with None -> aorig
   | Some r -> r.rew_to) args args'
      in
      let res = { rew_car = ty; rew_from = t;
    rew_to = mkApp (m, args'); rew_prf = RewCast DEFAULTcast;
    rew_evars = evars' }
      in Success res
     in state, res
   in
     if flags.on_morphisms then
       let mty = Retyping.get_type_of env (goalevars evars) m in
       let evars, cstr', m, mty, argsl, args =
  let argsl = Array.to_list args in
  let lift = if prop then PropGlobal.lift_cstr else TypeGlobal.lift_cstr in
    match lift env evars argsl m mty None with
    | Some (evars, cstr', m, mty, args) ->
      evars, Some cstr', m, mty, args, Array.of_list args
    | None -> evars, None, m, mty, argsl, args
       in
       let state, m' = s.strategy { state ; env ; unfresh ;
        term1 = m ; ty1 = mty ;
        cstr = (prop, cstr') ; evars } in
  match m' with
  | Fail -> rewrite_args state None (* Standard path, try rewrite on arguments *)
  | Identity -> rewrite_args state (Some false)
  | Success r ->
      (* We rewrote the function and get a proof of pointwise rel for the arguments.
       We just apply it. *)

      let prf = match r.rew_prf with
        | RewPrf (rel, prf) ->
   let app = if prop then PropGlobal.apply_pointwise 
     else TypeGlobal.apply_pointwise 
   in
     RewPrf (app (goalevars evars) rel argsl, mkApp (prf, args))
        | x -> x
      in
      let res =
        { rew_car = Reductionops.hnf_prod_appvect env (goalevars evars) r.rew_car args;
   rew_from = mkApp(r.rew_from, args); rew_to = mkApp(r.rew_to, args);
   rew_prf = prf; rew_evars = r.rew_evars }
      in 
      let res = 
        match prf with
        | RewPrf (rel, prf) ->
   Success (apply_constraint env unfresh res.rew_car
          rel prf (prop,cstr) res)
        | _ -> Success res
      in state, res
     else rewrite_args state None
       
      | Prod (n, x, b) when noccurn (goalevars evars) 1 b ->
   let b = subst1 mkProp b in
   let tx = Retyping.get_type_of env (goalevars evars) x
   and tb = Retyping.get_type_of env (goalevars evars) b in
   let arr = if prop then PropGlobal.arrow_morphism 
     else TypeGlobal.arrow_morphism 
   in
   let (evars', mor), unfold = arr env evars tx tb x b in
   let state, res = aux { state ; env ; unfresh ;
     term1 = mor ; ty1 = ty ;
     cstr = (prop,cstr) ; evars = evars' } in
   let res = 
     match res with
     | Success r -> Success { r with rew_to = unfold (goalevars r.rew_evars) r.rew_to }
     | Fail | Identity -> res
   in state, res

      (*  if x' = None && flags.under_lambdas then *)
      (*    let lam = mkLambda (n, x, b) in *)
      (*    let lam', occ = aux env lam occ None in *)
      (*    let res =  *)
      (*      match lam' with *)
      (*      | None -> None *)
      (*      | Some (prf, (car, rel, c1, c2)) -> *)
      (*  Some (resolve_morphism env sigma t *)
      (*   ~fnewt:unfold_all *)
      (*   (Lazy.force coq_all) [| x ; lam |] [| None; lam' |] *)
      (*   cstr evars) *)
      (*    in res, occ *)
      (*  else *)

      | Prod (n, dom, codom) ->
          let lam = mkLambda (n, dom, codom) in
   let (evars', app), unfold =
     if eq_constr (fst evars) ty mkProp then
       (app_poly_sort prop env evars coq_all [| dom; lam |]), TypeGlobal.unfold_all
     else 
       let forall = if prop then PropGlobal.coq_forall else TypeGlobal.coq_forall in
  (app_poly_sort prop env evars forall [| dom; lam |]), TypeGlobal.unfold_forall
   in
   let state, res = aux { state ; env ; unfresh ;
     term1 = app ; ty1 = ty ;
     cstr = (prop,cstr) ; evars = evars' } in
   let res = 
     match res with
     | Success r -> Success { r with rew_to = unfold (goalevars r.rew_evars) r.rew_to }
     | Fail | Identity -> res
   in state, res

(* TODO: real rewriting under binders: introduce x x' (H : R x x') and rewrite with 
   H at any occurrence of x. Ask for (R ==> R') for the lambda. Formalize this.
   B. Barras' idea is to have a context of relations, of length 1, with Σ for gluing
   dependent relations and using projections to get them out.
 *)

      (* | Lambda (n, t, b) when flags.under_lambdas -> *)
      (*    let n' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n in *)
      (*    let n'' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n' in *)
      (*    let n''' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n'' in *)
      (*    let rel = new_cstr_evar cstr env (mkApp (Lazy.force coq_relation, [|t|])) in *)
      (*    let env' = Environ.push_rel_context [(n'',None,lift 2 rel);(n'',None,lift 1 t);(n', None, t)] env in *)
      (*    let b' = s env' avoid b (Typing.type_of env' (goalevars evars) (lift 2 b)) (unlift_cstr env (goalevars evars) cstr) evars in *)
      (*      (match b' with *)
      (*      | Some (Some r) -> *)
      (*  let prf = match r.rew_prf with *)
      (*    | RewPrf (rel, prf) -> *)
      (*        let rel = pointwise_or_dep_relation n' t r.rew_car rel in *)
      (*        let prf = mkLambda (n', t, prf) in *)
      (*  RewPrf (rel, prf) *)
      (*    | x -> x *)
      (*  in *)
      (*    Some (Some { r with *)
      (*      rew_prf = prf; *)
      (*      rew_car = mkProd (n, t, r.rew_car); *)
      (*      rew_from = mkLambda(n, t, r.rew_from); *)
      (*      rew_to = mkLambda (n, t, r.rew_to) }) *)
      (*      | _ -> b') *)

      | Lambda (n, t, b) when flags.under_lambdas ->
        let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in
        let open Context.Rel.Declaration in
        let env' = EConstr.push_rel (LocalAssum (n', t)) env in
 let bty = Retyping.get_type_of env' (goalevars evars) b in
 let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in
 let state, b' = s.strategy { state ; env = env' ; unfresh ;
         term1 = b ; ty1 = bty ;
         cstr = (prop, unlift env evars cstr) ;
         evars } in
 let res = 
   match b' with
   | Success r ->
     let r = match r.rew_prf with
       | RewPrf (rel, prf) ->
  let point = if prop then PropGlobal.pointwise_or_dep_relation else
      TypeGlobal.pointwise_or_dep_relation
  in
                let evars, rel = point env r.rew_evars n'.binder_name t r.rew_car rel in
                let prf = mkLambda (n', t, prf) in
    { r with rew_prf = RewPrf (rel, prf); rew_evars = evars }
       | x -> r
     in
       Success { r with
                rew_car = mkProd (n, t, r.rew_car);
                rew_from = mkLambda(n, t, r.rew_from);
                rew_to = mkLambda (n, t, r.rew_to) }
   | Fail | Identity -> b'
 in state, res
     
      | Case (ci, p, c, brs) ->
 let cty = Retyping.get_type_of env (goalevars evars) c in
 let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in
 let cstr' = Some eqty in
 let state, c' = s.strategy { state ; env ; unfresh ;
         term1 = c ; ty1 = cty ;
         cstr = (prop, cstr') ; evars = evars' } in
 let state, res = 
   match c' with
   | Success r ->
     let case = mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs) in
     let res = make_leibniz_proof env case ty r in
       state, Success (coerce env unfresh (prop,cstr) res)
   | Fail | Identity ->
     if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then
       let evars', eqty = app_poly_sort prop env evars coq_eq [| ty |] in
       let cstr = Some eqty in
       let state, found, brs' = Array.fold_left
  (fun (state, found, acc) br ->
    if not (Option.is_empty found) then 
      (state, found, fun x -> lift 1 br :: acc x)
    else
      let state, res = s.strategy { state ; env ; unfresh ;
        term1 = br ; ty1 = ty ;
        cstr = (prop,cstr) ; evars } in
        match res with
        | Success r -> (state, Some r, fun x -> mkRel 1 :: acc x)
        | Fail | Identity -> (state, None, fun x -> lift 1 br :: acc x))
  (state, None, fun x -> []) brs
       in
  match found with
  | Some r ->
    let ctxc = mkCase (ci, lift 1 p, lift 1 c, Array.of_list (List.rev (brs' c'))) in
      state, Success (make_leibniz_proof env ctxc ty r)
  | None -> state, c'
     else
       match try Some (fold_match env (goalevars evars) t) with Not_found -> None with
       | None -> state, c'
       | Some (cst, _, t', eff (*FIXME*)) ->
   let state, res = aux { state ; env ; unfresh ;
     term1 = t' ; ty1 = ty ;
     cstr = (prop,cstr) ; evars } in
  let res = 
    match res with
    | Success prf -> 
      Success { prf with
        rew_from = t; 
        rew_to = unfold_match env (goalevars evars) cst prf.rew_to }
    | x' -> c'
  in state, res
 in 
 let res = 
   match res with
   | Success r -> Success (coerce env unfresh (prop,cstr) r)
   | Fail | Identity -> res
 in state, res
      | _ -> state, Fail
  in { strategy = aux }

let all_subterms = subterm true default_flags
let one_subterm = subterm false default_flags

(** Requires transitivity of the rewrite step, if not a reduction.
    Not tail-recursive. *)


let transitivity state env unfresh prop (res : rewrite_result_info) (next : 'a pure_strategy) :
    'a * rewrite_result =
  let state, nextres =
    next.strategy { state ; env ; unfresh ;
      term1 = res.rew_to ; ty1 = res.rew_car ;
      cstr = (prop, get_opt_rew_rel res.rew_prf) ;
      evars = res.rew_evars }
  in 
  let res = 
    match nextres with
    | Fail -> Fail
    | Identity -> Success res
    | Success res' ->
      match res.rew_prf with
      | RewCast c -> Success { res' with rew_from = res.rew_from }
      | RewPrf (rew_rel, rew_prf) ->
 match res'.rew_prf with
 | RewCast _ -> Success { res with rew_to = res'.rew_to }
 | RewPrf (res'_rel, res'_prf) ->
   let trans = 
     if prop then PropGlobal.transitive_type 
     else TypeGlobal.transitive_type
   in
   let evars, prfty = 
     app_poly_sort prop env res'.rew_evars trans [| res.rew_car; rew_rel |]
   in
   let evars, prf = new_cstr_evar evars env prfty in
   let prf = mkApp (prf, [|res.rew_from; res'.rew_from; res'.rew_to;
      rew_prf; res'_prf |])
   in Success { res' with rew_from = res.rew_from;
     rew_evars = evars; rew_prf = RewPrf (res'_rel, prf) }
  in state, res

(** Rewriting strategies.

    Inspired by ELAN's rewriting strategies:
    http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.4049
*)


module Strategies =
  struct

    let fail : 'a pure_strategy =
      { strategy = fun { state } -> state, Fail }

    let id : 'a pure_strategy =
      { strategy = fun { state } -> state, Identity }

    let refl : 'a pure_strategy =
      { strategy =
 fun { state ; env ;
       term1 = t ; ty1 = ty ;
       cstr = (prop,cstr) ; evars } ->
 let evars, rel = match cstr with
   | None -> 
     let mkr = if prop then PropGlobal.mk_relation else TypeGlobal.mk_relation in
     let evars, rty = mkr env evars ty in
       new_cstr_evar evars env rty
   | Some r -> evars, r
 in
 let evars, proof =
   let proxy = 
     if prop then PropGlobal.proper_proxy_type 
     else TypeGlobal.proper_proxy_type
   in
   let evars, mty = app_poly_sort prop env evars proxy [| ty ; rel; t |] in
     new_cstr_evar evars env mty
 in
 let res = Success { rew_car = ty; rew_from = t; rew_to = t;
          rew_prf = RewPrf (rel, proof); rew_evars = evars }
 in state, res
      }

    let progress (s : 'a pure_strategy) : 'a pure_strategy = { strategy =
      fun input ->
 let state, res = s.strategy input in
   match res with
   | Fail -> state, Fail
   | Identity -> state, Fail
   | Success r -> state, Success r
            }
     
    let seq first snd : 'a pure_strategy = { strategy =
      fun ({ env ; unfresh ; cstr } as input) ->
 let state, res = first.strategy input in
   match res with
   | Fail -> state, Fail
   | Identity -> snd.strategy { input with state }
   | Success res -> transitivity state env unfresh (fst cstr) res snd
        }
     
    let choice fst snd : 'a pure_strategy = { strategy =
      fun input ->
 let state, res = fst.strategy input in
   match res with
   | Fail -> snd.strategy { input with state }
   | Identity | Success _ -> state, res
         }

    let try_ str : 'a pure_strategy = choice str id

    let check_interrupt str input =
      Control.check_for_interrupt ();
      str input

    let fix (f : 'a pure_strategy -> 'a pure_strategy) : 'a pure_strategy =
      let rec aux input = (f { strategy = fun input -> check_interrupt aux input }).strategy input in
      { strategy = aux }
    
    let any (s : 'a pure_strategy) : 'a pure_strategy =
      fix (fun any -> try_ (seq s any))

    let repeat (s : 'a pure_strategy) : 'a pure_strategy =
      seq s (any s)

    let bu (s : 'a pure_strategy) : 'a pure_strategy =
      fix (fun s' -> seq (choice (progress (all_subterms s')) s) (try_ s'))

    let td (s : 'a pure_strategy) : 'a pure_strategy =
      fix (fun s' -> seq (choice s (progress (all_subterms s'))) (try_ s'))

    let innermost (s : 'a pure_strategy) : 'a pure_strategy =
      fix (fun ins -> choice (one_subterm ins) s)

    let outermost (s : 'a pure_strategy) : 'a pure_strategy =
      fix (fun out -> choice s (one_subterm out))

    let lemmas cs : 'a pure_strategy =
      List.fold_left (fun tac (l,l2r,by) ->
 choice tac (apply_lemma l2r rewrite_unif_flags l by AllOccurrences))
 fail cs

    let inj_open hint = (); fun sigma ->
      let ctx = UState.of_context_set hint.Autorewrite.rew_ctx in
      let sigma = Evd.merge_universe_context sigma ctx in
      (sigma, (EConstr.of_constr hint.Autorewrite.rew_lemma, NoBindings))

    let old_hints (db : string) : 'a pure_strategy =
      let rules = Autorewrite.find_rewrites db in
 lemmas
   (List.map (fun hint -> (inj_open hint, hint.Autorewrite.rew_l2r,
      hint.Autorewrite.rew_tac)) rules)

    let hints (db : string) : 'a pure_strategy = { strategy =
      fun ({ term1 = t } as input) ->
      let t = EConstr.Unsafe.to_constr t in
      let rules = Autorewrite.find_matches db t in
      let lemma hint = (inj_open hint, hint.Autorewrite.rew_l2r,
   hint.Autorewrite.rew_tac) in
      let lems = List.map lemma rules in
      (lemmas lems).strategy input
       }

    let reduce (r : Redexpr.red_expr) : 'a pure_strategy = { strategy =
 fun { state = state ; env = env ; term1 = t ; ty1 = ty ; cstr = cstr ; evars = evars } ->
          let rfn, ckind = Redexpr.reduction_of_red_expr env r in
          let sigma = goalevars evars in
   let (sigma, t') = rfn env sigma t in
     if Termops.eq_constr sigma t' t then
       state, Identity
     else
       state, Success { rew_car = ty; rew_from = t; rew_to = t';
          rew_prf = RewCast ckind; 
          rew_evars = sigma, cstrevars evars }
          }
 
    let fold_glob c : 'a pure_strategy = { strategy =
      fun { state ; env ; term1 = t ; ty1 = ty ; cstr ; evars } ->
(*  let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
 let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
 let unfolded =
   try Tacred.try_red_product env sigma c
   with e when CErrors.noncritical e ->
            user_err Pp.(str "fold: the term is not unfoldable!")
 in
   try
     let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in
     let c' = Reductionops.nf_evar sigma c in
       state, Success { rew_car = ty; rew_from = t; rew_to = c';
      rew_prf = RewCast DEFAULTcast;
      rew_evars = (sigma, snd evars) }
   with e when CErrors.noncritical e -> state, Fail
      }
  

end

(** The strategy for a single rewrite, dealing with occurrences. *)

(** A dummy initial clauseenv to avoid generating initial evars before
    even finding a first application of the rewriting lemma, in setoid_rewrite
    mode *)


let rewrite_with l2r flags c occs : strategy = { strategy =
  fun ({ state = () } as input) ->
    let unify env evars t =
      let (sigma, cstrs) = evars in
      let (sigma, rew) = refresh_hypinfo env sigma c in
      unify_eqn rew l2r flags env (sigma, cstrs) None t
    in
    let app = apply_rule unify occs in
    let strat = 
      Strategies.fix (fun aux -> 
 Strategies.choice app (subterm true default_flags aux))
    in
    let _, res = strat.strategy { input with state = 0 } in
    ((), res)
            }

let apply_strategy (s : strategy) env unfresh concl (prop, cstr) evars =
  let ty = Retyping.get_type_of env (goalevars evars) concl in
  let _, res = s.strategy { state = () ; env ; unfresh ;
       term1 = concl ; ty1 = ty ;
       cstr = (prop, Some cstr) ; evars } in
  res

let solve_constraints env (evars,cstrs) =
  let oldtcs = Evd.get_typeclass_evars evars in
  let evars' = Evd.set_typeclass_evars evars cstrs in
  let evars' = Typeclasses.resolve_typeclasses env ~filter:all_evars ~split:false ~fail:true evars' in
  Evd.set_typeclass_evars evars' oldtcs

let nf_zeta =
  Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])

exception RewriteFailure of Pp.t

type result = (evar_map * constr option * types) option option

let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result =
  let sigma, sort = Typing.sort_of env sigma concl in
  let evdref = ref sigma in
  let evars = (!evdref, Evar.Set.empty) in
  let evars, cstr =
    let prop, (evars, arrow) = 
      if Sorts.is_prop sort then true, app_poly_sort true env evars impl [||]
      else false, app_poly_sort false env evars TypeGlobal.arrow [||]
    in
      match is_hyp with
      | None -> 
 let evars, t = poly_inverse prop env evars (mkSort sort) arrow in 
   evars, (prop, t)
      | Some _ -> evars, (prop, arrow)
  in
  let eq = apply_strategy strat env avoid concl cstr evars in
    match eq with
    | Fail -> None
    | Identity -> Some None
    | Success res ->
      let (_, cstrs) = res.rew_evars in
      let evars' = solve_constraints env res.rew_evars in
      let newt = Reductionops.nf_evar evars' res.rew_to in
      let evars = (* Keep only original evars (potentially instantiated) and goal evars,
     the rest has been defined and substituted already. *)

 Evar.Set.fold 
   (fun ev acc -> 
    if not (Evd.is_defined acc ev) then 
      user_err ~hdr:"rewrite"
     (str "Unsolved constraint remaining: " ++ spc () ++
                           Termops.pr_evar_info env acc (Evd.find acc ev))
    else Evd.remove acc ev) 
   cstrs evars'
      in
      let res = match res.rew_prf with
 | RewCast c -> None
 | RewPrf (rel, p) ->
   let p = nf_zeta env evars' (Reductionops.nf_evar evars' p) in
   let term =
     match abs with
     | None -> p
     | Some (t, ty) ->
              let t = Reductionops.nf_evar evars' t in
              let ty = Reductionops.nf_evar evars' ty in
                mkApp (mkLambda (make_annot (Name (Id.of_string "lemma")) Sorts.Relevant, ty, p), [| t |])
   in
   let proof = match is_hyp with
            | None -> term
            | Some id -> mkApp (term, [| mkVar id |])
          in Some proof
      in Some (Some (evars, res, newt))

(** Insert a declaration after the last declaration it depends on *)
let rec insert_dependent env sigma decl accu hyps = match hyps with
| [] -> List.rev_append accu [decl]
| ndecl :: rem ->
  if occur_var_in_decl env sigma (NamedDecl.get_id ndecl) decl then
    List.rev_append accu (decl :: hyps)
  else
    insert_dependent env sigma decl (ndecl :: accu) rem

let assert_replacing id newt tac = 
  let prf = Proofview.Goal.enter begin fun gl ->
    let concl = Proofview.Goal.concl gl in
    let env = Proofview.Goal.env gl in
    let sigma = Tacmach.New.project gl in
    let ctx = named_context env in
    let after, before = List.split_when (NamedDecl.get_id %> Id.equal id) ctx in
    let nc = match before with
    | [] -> assert false
    | d :: rem -> insert_dependent env sigma
                    (LocalAssum (make_annot (NamedDecl.get_id d) Sorts.Relevant, newt)) [] after @ rem
    in
    let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
    Refine.refine ~typecheck:true begin fun sigma ->
      let (sigma, ev) = Evarutil.new_evar env' sigma concl in
      let (sigma, ev') = Evarutil.new_evar env sigma newt in
      let map d =
        let n = NamedDecl.get_id d in
        if Id.equal n id then ev' else mkVar n
      in
      let (e, _) = destEvar sigma ev in
      (sigma, mkEvar (e, Array.map_of_list map nc))
    end
  end in
  Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)

let newfail n s = 
  Proofview.tclZERO (Refiner.FailError (n, lazy s))

let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
  let open Proofview.Notations in
  (* For compatibility *)
  let beta = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in
  let beta_hyp id = Tactics.reduct_in_hyp Reductionops.nf_betaiota (id, InHyp) in
  let treat sigma res = 
    match res with
    | None -> newfail 0 (str "Nothing to rewrite")
    | Some None -> if progress then newfail 0 (str"Failed to progress")
     else Proofview.tclUNIT ()
    | Some (Some res) ->
        let (undef, prf, newt) = res in
        let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in
        let gls = List.rev (Evd.fold_undefined fold undef []) in
        let gls = List.map Proofview.with_empty_state gls in
          match clause, prf with
 | Some id, Some p ->
            let tac = tclTHENLIST [
              Refine.refine ~typecheck:true (fun h -> (h,p));
              Proofview.Unsafe.tclNEWGOALS gls;
            ] in
            Proofview.Unsafe.tclEVARS undef <*>
     tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id)
 | Some id, None ->
            Proofview.Unsafe.tclEVARS undef <*>
            convert_hyp ~check:false (LocalAssum (make_annot id Sorts.Relevant, newt)) <*>
            beta_hyp id
 | None, Some p ->
            Proofview.Unsafe.tclEVARS undef <*>
            Proofview.Goal.enter begin fun gl ->
            let env = Proofview.Goal.env gl in
            let make = begin fun sigma ->
              let (sigma, ev) = Evarutil.new_evar env sigma newt in
              (sigma, mkApp (p, [| ev |]))
            end in
            Refine.refine ~typecheck:true make <*> Proofview.Unsafe.tclNEWGOALS gls
            end
 | None, None ->
            Proofview.Unsafe.tclEVARS undef <*>
            convert_concl ~check:false newt DEFAULTcast
  in
  Proofview.Goal.enter begin fun gl ->
    let concl = Proofview.Goal.concl gl in
    let env = Proofview.Goal.env gl in
    let sigma = Tacmach.New.project gl in
    let ty = match clause with
    | None -> concl
    | Some id -> EConstr.of_constr (Environ.named_type id env)
    in
    let env = match clause with
    | None -> env
    | Some id ->
      (* Only consider variables not depending on [id] *)
      let ctx = named_context env in
      let filter decl = not (occur_var_in_decl env sigma id decl) in
      let nctx = List.filter filter ctx in
      Environ.reset_with_named_context (val_of_named_context nctx) env
    in
    try
      let res =
        cl_rewrite_clause_aux ?abs strat env Id.Set.empty sigma ty clause
      in
      let sigma = match origsigma with None -> sigma | Some sigma -> sigma in
      treat sigma res <*>
      (* For compatibility *)
      beta <*> Proofview.shelve_unifiable
    with
    | PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) ->
      raise (RewriteFailure (Himsg.explain_pretype_error env evd e))
  end

let tactic_init_setoid () = 
  try init_setoid (); Proofview.tclUNIT ()
  with e when CErrors.noncritical e -> Tacticals.New.tclFAIL 0 (str"Setoid library not loaded")

let cl_rewrite_clause_strat progress strat clause =
  tactic_init_setoid () <*>
  (if progress then Proofview.tclPROGRESS else fun x -> x)
   (Proofview.tclOR
      (cl_rewrite_clause_newtac ~progress strat clause)
      (fun (e, info) -> match e with
       | RewriteFailure e ->
  tclZEROMSG (str"setoid rewrite failed: " ++ e)
       | Refiner.FailError (n, pp) -> 
   tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp)
       | e -> Proofview.tclZERO ~info e))

(** Setoid rewriting when called with "setoid_rewrite" *)
let cl_rewrite_clause l left2right occs clause =
  let strat = rewrite_with left2right (general_rewrite_unif_flags ()) l occs in
    cl_rewrite_clause_strat true strat clause

(** Setoid rewriting when called with "rewrite_strat" *)
let cl_rewrite_clause_strat strat clause =
  cl_rewrite_clause_strat false strat clause
  
let apply_glob_constr c l2r occs = (); fun ({ state = () ; env = env } as input) ->
  let c sigma =
    let (sigma, c) = Pretyping.understand_tcc env sigma c in
    (sigma, (c, NoBindings))
  in
  let flags = general_rewrite_unif_flags () in
  (apply_lemma l2r flags c None occs).strategy input

let interp_glob_constr_list env =
  let make c = (); fun sigma ->
    let sigma, c = Pretyping.understand_tcc env sigma c in
    (sigma, (c, NoBindings))
  in
  List.map (fun c -> make c, true, None)

(* Syntax for rewriting with strategies *)

type unary_strategy = 
    Subterms | Subterm | Innermost | Outermost
  | Bottomup | Topdown | Progress | Try | Any | Repeat

type binary_strategy = 
  | Compose | Choice

type ('constr,'redexpr) strategy_ast = 
  | StratId | StratFail | StratRefl
  | StratUnary of unary_strategy * ('constr,'redexpr) strategy_ast
  | StratBinary of binary_strategy 
    * ('constr,'redexpr) strategy_ast * ('constr,'redexpr) strategy_ast
  | StratConstr of 'constr * bool
  | StratTerms of 'constr list
  | StratHints of bool * string
  | StratEval of 'redexpr
  | StratFold of 'constr

let rec map_strategy (f : 'a -> 'a2) (g : 'b -> 'b2) : ('a,'b) strategy_ast -> ('a2,'b2) strategy_ast = function
  | StratId | StratFail | StratRefl as s -> s
  | StratUnary (s, str) -> StratUnary (s, map_strategy f g str)
  | StratBinary (s, str, str') -> StratBinary (s, map_strategy f g str, map_strategy f g str')
  | StratConstr (c, b) -> StratConstr (f c, b)
  | StratTerms l -> StratTerms (List.map f l)
  | StratHints (b, id) -> StratHints (b, id)
  | StratEval r -> StratEval (g r)
  | StratFold c -> StratFold (f c)

let pr_ustrategy = function
| Subterms -> str "subterms"
| Subterm -> str "subterm"
| Innermost -> str "innermost"
| Outermost -> str "outermost"
| Bottomup -> str "bottomup"
| Topdown -> str "topdown"
| Progress -> str "progress"
Try -> str "try"
| Any -> str "any"
| Repeat -> str "repeat"

let paren p = str "(" ++ p ++ str ")"

let rec pr_strategy prc prr = function
| StratId -> str "id"
| StratFail -> str "fail"
| StratRefl -> str "refl"
| StratUnary (s, str) ->
  pr_ustrategy s ++ spc () ++ paren (pr_strategy prc prr str)
| StratBinary (Choice, str1, str2) ->
--> --------------------

--> maximum size reached

--> --------------------

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.67Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤





Begriffe der Konzeptbildung
Was zu einem Entwurf gehört
Begriffe der Konzeptbildung
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik