Quelle coercion.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)         *)
(************************************************************************)

(* Created by Hugo Herbelin for Coq V7 by isolating the coercion
   mechanism out of the type inference algorithm in file trad.ml from
   Coq V6.3, Nov 1999; The coercion mechanism was implemented in
   trad.ml by Amokrane Saïbi, May 1996 *)
(* Addition of products and sorts in canonical structures by Pierre
   Corbineau, Feb 2008 *)
(* Turned into an abstract compilation unit by Matthieu Sozeau, March 2006 *)

open CErrors
open Util
open Names
open Term
open Constr
open Context
open Environ
open EConstr
open Vars
open Reductionops
open Pretype_errors
open Coercionops
open Evarutil
open Evarconv
open Evd
open Globnames

let { Goptions.get = get_use_typeclasses_for_conversion } =
  Goptions.declare_bool_option_and_ref
    ~key:["Typeclass"; "Resolution"; "For"; "Conversion"]
    ~value:true
    ()

(* Typing operations dealing with coercions *)
exception NoCoercion
exception NoCoercionNoUnifier of evar_map * unification_error

let apply_coercion_args env sigma isproj bo ty arg arg_ty nparams =
  let destProd sigma typ =
    match EConstr.kind sigma (whd_all env sigma typ) with
    | Prod (_, c1, c2) -> c1, c2
    | _ -> anomaly (Pp.str "apply_coercion_args.") in
  let rec apply_rec sigma acc typ nparams =
    if nparams <= 0 then sigma, List.rev acc, typ else
      let c1, c2 = destProd sigma typ in
      let typeclass_candidate = Typeclasses.is_maybe_class_type sigma c1 in
      let sigma, x = Evarutil.new_evar ~typeclass_candidate env sigma c1 in
      apply_rec sigma (x :: acc) (subst1 x c2) (nparams - 1) in
  let sigma, params, typ = apply_rec sigma [] ty nparams in
  let sigma, args, typ =
    let c1, c2 = destProd sigma typ in
    let sigma =
      let arg_ty = whd_zeta env sigma arg_ty in
      try Evarconv.unify_leq_delay env sigma arg_ty c1
      with Evarconv.UnableToUnify _ -> raise NoCoercion in
    sigma, params @ [arg], subst1 arg c2 in
  let bo, args =
    match isproj with
    | None -> bo, args
    | Some (p,r) ->
      let npars = Projection.Repr.npars p in
      let p = Projection.make p false in
      let args = List.skipn npars args in
      let hd, tl = match args with hd :: tl -> hd, tl | [] -> assert false in
      mkProj (p, r, hd), tl in
  sigma, applist (bo, args), params, typ

(* appliquer le chemin de coercions de patterns p *)
let apply_pattern_coercion ?loc pat p =
  List.fold_left
    (fun pat (co,n) ->
       let f i =
         if i<n then (DAst.make ?loc @@ Glob_term.PatVar Anonymous) else pat in
        DAst.make ?loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous))
    pat p

(* raise Not_found if no coercion found *)
let inh_pattern_coerce_to ?loc env pat ind1 ind2 =
  let p = lookup_pattern_path_between env (ind1,ind2) in
    apply_pattern_coercion ?loc pat p

(* Program coercions *)

open Program

let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env sigma c =
  let src = Loc.tag ?loc (Evar_kinds.QuestionMark {
      Evar_kinds.default_question_mark with
      Evar_kinds.qm_obligation=Evar_kinds.Define opaque;
      Evar_kinds.qm_name=na;
  }) in
  let typeclass_candidate = Typeclasses.is_maybe_class_type sigma c in
  let sigma, v = Evarutil.new_evar ~typeclass_candidate env sigma ~src c in
  let sigma = Evd.set_obligation_evar sigma (fst (destEvar sigma v)) in
  sigma, v

let app_opt env sigma f t =
  let sigma, t =
  match f with
  | None -> sigma, t
  | Some f -> f sigma t
  in
  sigma, whd_betaiota env sigma t

let pair_of_array a = (a.(0), a.(1))

let disc_subset env sigma x =
  match EConstr.kind sigma x with
  | App (c, l) ->
      (match EConstr.kind sigma c with
       Ind (i,_) ->
         let len = Array.length l in
         let sigty = delayed_force sig_typ in
           if Int.equal len 2 && QInd.equal env i (Globnames.destIndRef sigty)
           then
             let (a, b) = pair_of_array l in
               Some (a, b)
           else None
       | _ -> None)
  | _ -> None

exception NoSubtacCoercion

let hnf env sigma c = whd_all env sigma c
let hnf_nodelta env sigma c = whd_betaiota env sigma c

let has_undefined_head_evar sigma c =
  let rec hrec c = match kind sigma c with
    | Evar (evk,_)   -> true
    | Case (_, _, _, _, _, c, _) -> hrec c
    | App (c,_)      -> hrec c
    | Cast (c,_,_)   -> hrec c
    | Proj (_, _, c) -> hrec c
    | _ -> false
  in hrec c

let lift_args n sign =
  let rec liftrec k = function
    | t::sign -> liftn n k t :: (liftrec (k-1) sign)
    | [] -> []
  in
    liftrec (List.length sign) sign

let coerce ?loc env sigma (x : EConstr.constr) (y : EConstr.constr)
  : evar_map * (evar_map -> EConstr.constr -> evar_map * EConstr.constr) option
  =
  let open Context.Rel.Declaration in
  let rec coerce_unify env sigma x y =
    let x = hnf env sigma x and y = hnf env sigma y in
    try
      Evarconv.unify_leq_delay env sigma x y, None
    with
      Evarconv.UnableToUnify _ -> coerce' env sigma x y
  and coerce' env sigma x y : evar_map * (evar_map -> EConstr.constr -> evar_map * EConstr.constr) option =
    let subco sigma = subset_inferred env sigma x y in
    let whd_decompose_prod c =
      match Reductionops.whd_decompose_prod_n env sigma 1 c with
      | ([(na, t)], c) -> (na, t), c
      | _ -> raise NoSubtacCoercion (* should not happen: there are arguments to consume *)
    in
    let coerce_application sigma typ typ' c c' l l' =
      let len = Array.length l in
      let rec aux sigma tele typ typ' i co =
        if i < len then
          let hdx = l.(i) and hdy = l'.(i) in
          try
            let sigma = unify_leq_delay env sigma hdx hdy in
            let (n, eqT), restT = whd_decompose_prod typ in
            let (n', eqT'), restT' = whd_decompose_prod typ' in
            aux sigma (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co
          with UnableToUnify _ as exn ->
            let _, info = Exninfo.capture exn in
            let (n, eqT), restT = whd_decompose_prod typ in
            let (n', eqT'), restT' = whd_decompose_prod typ' in
            let sigma =
              try
                unify_leq_delay env sigma eqT eqT'
              with UnableToUnify _ ->
                let e, info = Exninfo.capture exn in
                Exninfo.iraise (NoSubtacCoercion,info)
            in
            (* Disallow equalities on arities *)
            if Reductionops.is_arity env sigma eqT then
              Exninfo.iraise (NoSubtacCoercion,info);
            let restargs = lift_args 1
                (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i)))))
            in
            let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in
            let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in
            let sigma, eq = papp env sigma coq_eq_ind [| eqT; hdx; hdy |] in
            let sigma, evar = make_existential ?loc n.binder_name env sigma eq in
            let eq_app sigma x = papp env sigma coq_eq_rect
                [| eqT; hdx; pred; x; hdy; evar|]
            in
            aux sigma (hdy :: tele) (subst1 hdx restT)
              (subst1 hdy restT') (succ i) (fun sigma x -> let sigma, x = co sigma x in eq_app sigma x)
        else
          sigma, Some (fun sigma x ->
              let sigma, term = co sigma x in
              let sigma, term = Typing.solve_evars env sigma term in
              sigma, term)
      in
      if isEvar sigma c || isEvar sigma c' || not (Program.is_program_generalized_coercion ()) then
        (* Second-order unification needed. *)
        raise NoSubtacCoercion;
      aux sigma [] typ typ' 0 (fun sigma x -> sigma, x)
    in
    match (EConstr.kind sigma x, EConstr.kind sigma y) with
    | Sort s, Sort s' ->
      (match ESorts.kind sigma s, ESorts.kind sigma s' with
       | Prop, Prop | Set, Set -> sigma, None
       | (Prop | Set), Type _ -> sigma, None
       | Type x, Type y when Univ.Universe.equal x y -> sigma, None (* false *)
       | _ -> subco sigma)
    | Prod (name, a, b), Prod (name', a', b') ->
      let name' =
        {name' with
         binder_name =
           Name (Namegen.next_ident_away
                   Namegen.default_dependent_ident (Termops.vars_of_env env))}
      in
      let env' = push_rel (LocalAssum (name', a')) env in
      let sigma, c1 = coerce_unify env' sigma (lift 1 a') (lift 1 a) in
      (* env, x : a' |- c1 : lift 1 a' > lift 1 a *)
      let sigma, coec1 = app_opt env' sigma c1 (mkRel 1) in
      (* env, x : a' |- c1[x] : lift 1 a *)
      let sigma, c2 = coerce_unify env' sigma (subst1 coec1 (liftn 1 2 b)) b' in
      (* env, x : a' |- c2 : b[c1[x]/x]] > b' *)
      (match c1, c2 with
       | None, None -> sigma, None
       | _, _ ->
         sigma,
         Some (fun sigma f ->
             let sigma, t = app_opt env' sigma c2
                 (mkApp (lift 1 f, [| coec1 |])) in
             sigma, mkLambda (name', a', t)))

    | App (c, l), App (c', l') ->
      (match EConstr.kind sigma c, EConstr.kind sigma c' with
         Ind (i, u), Ind (i', u') -> (* Inductive types *)
         let len = Array.length l in
         let sigT = delayed_force sigT_typ in
         let prod = delayed_force prod_typ in
         (* Sigma types *)
         if Int.equal len (Array.length l') && Int.equal len 2 && QInd.equal env i i'
            && (QInd.equal env i (destIndRef sigT) || QInd.equal env i (destIndRef prod))
         then
           if QInd.equal env i (destIndRef sigT)
           then
             begin
               let (a, pb), (a', pb') =
                 pair_of_array l, pair_of_array l'
               in
               let sigma, c1 = coerce_unify env sigma a a' in
               let remove_head sigma a c =
                 match EConstr.kind sigma c with
                 | Lambda (n, t, t') -> sigma, (c, t')
                 | Evar (k, args) ->
                   let (sigma, t) = Evardefine.define_evar_as_lambda env sigma (k,args) in
                   let (n, dom, rng) = destLambda sigma t in
                   let sigma =
                     if isEvar sigma dom then
                       let (domk, args) = destEvar sigma dom in
                       define domk a sigma
                     else sigma
                   in
                   sigma, (t, rng)
                 | _ -> raise NoSubtacCoercion
               in
               let sigma, (pb, b) = remove_head sigma a pb in
               let sigma, (pb', b') = remove_head sigma a' pb' in
               let ra = Retyping.relevance_of_type env sigma a in
               let env' = push_rel
                   (LocalAssum (make_annot (Name Namegen.default_dependent_ident) ra, a))
                   env
               in
               let sigma, c2 = coerce_unify env' sigma b b' in
               match c1, c2 with
               | None, None -> sigma, None
               | _, _ ->
                 sigma,
                 Some (fun sigma x ->
                     let sigma, t1 = papp env sigma sigT_proj1 [| a; pb; x |] in
                     let sigma, t2 = papp env sigma sigT_proj2 [| a; pb; x |] in
                     let sigma, x =  app_opt env' sigma c1 t1 in
                     let sigma, y = app_opt env' sigma c2 t2 in
                     papp env sigma sigT_intro [| a'; pb'; x ; y |])
             end
           else
             begin
               let (a, b), (a', b') =
                 pair_of_array l, pair_of_array l'
               in
               let sigma, c1 = coerce_unify env sigma a a' in
               let sigma, c2 = coerce_unify env sigma b b' in
               match c1, c2 with
               | None, None -> sigma, None
               | _, _ ->
                 sigma,
                 Some (fun sigma x ->
                     let sigma, t1 = papp env sigma prod_proj1 [| a; b; x |] in
                     let sigma, t2 = papp env sigma prod_proj2 [| a; b; x |] in
                     let sigma, x = app_opt env sigma c1 t1 in
                     let sigma, y = app_opt env sigma c2 t2 in
                     papp env sigma prod_intro [| a'; b'; x ; y |])
             end
         else
         if QInd.equal env i i' && Int.equal len (Array.length l') then
           (try subco sigma
            with NoSubtacCoercion ->
              let sigma, typ = Typing.type_of env sigma c in
              let sigma, typ' = Typing.type_of env sigma c' in
              coerce_application sigma typ typ' c c' l l')
         else
           subco sigma
       | x, y when EConstr.eq_constr sigma c c' ->
         if Int.equal (Array.length l) (Array.length l') then
           let sigma, lam_type = Typing.type_of env sigma c in
           let sigma, lam_type' = Typing.type_of env sigma c' in
           coerce_application sigma lam_type lam_type' c c' l l'
         else subco sigma
       | _ -> subco sigma)
    | _, _ ->  subco sigma

  and subset_inferred env sigma x y =
    match disc_subset env sigma x with
      Some (u, p) ->
      let sigma, c = coerce_unify env sigma u y in
      let f sigma x =
        let sigma, t = papp env sigma sig_proj1 [| u; p; x |] in
        app_opt env sigma c t
      in sigma, Some f
    | None ->
      match disc_subset env sigma y with
        Some (u, p) ->
        let sigma, c = coerce_unify env sigma x u in
        sigma, Some
          (fun sigma x ->
             let sigma, cx = app_opt env sigma c x in
             let sigma, evar = make_existential ?loc Anonymous env sigma (mkApp (p, [| cx |]))
             in
             (papp env sigma sig_intro [| u; p; cx; evar |]))
      | None ->
        raise NoSubtacCoercion
  in coerce_unify env sigma x y

let app_coercion env sigma coercion v =
  match coercion with
  | None -> sigma, v
  | Some f ->
    let sigma, v' = f sigma v in
    let sigma, v' = Typing.solve_evars env sigma v' in
    sigma, whd_betaiota env sigma v'

let coerce_itf ?loc env sigma v t c1 =
  let sigma, coercion = coerce ?loc env sigma t c1 in
  app_coercion env sigma coercion v

let saturate_evd env sigma =
  Typeclasses.resolve_typeclasses
    ~filter:Typeclasses.no_goals ~fail:false env sigma

type coercion_trace =
  | IdCoe
  | PrimProjCoe of {
      proj : Projection.Repr.t;
      relevance : ERelevance.t;
      args : econstr list;
      previous : coercion_trace;
    }
  | Coe of {
      head : econstr;
      args : econstr list;
      previous : coercion_trace;
    }
  | ProdCoe of { na : Name.t binder_annot; ty : econstr; dom : coercion_trace; body : coercion_trace }
  | ReplaceCoe of econstr

let empty_coercion_trace = IdCoe

(* similar to iterated apply_coercion_args *)
let rec reapply_coercions sigma trace c = match trace with
  | IdCoe -> c
  | ReplaceCoe c -> c
  | PrimProjCoe { proj; relevance; args; previous } ->
    let c = reapply_coercions sigma previous c in
    let args = args@[c] in
    let head, args = match args with [] -> assert false | hd :: tl -> hd, tl in
    applist (mkProj (Projection.make proj false, relevance, head), args)
  | Coe {head; args; previous} ->
    let c = reapply_coercions sigma previous c in
    let args = args@[c] in
    applist (head, args)
  | ProdCoe { na; ty; dom; body } ->
    let x = reapply_coercions sigma dom (mkRel 1) in
    let c = beta_applist sigma (lift 1 c, [x]) in
    let c = reapply_coercions sigma body c in
    mkLambda (na, ty, c)

let instance_of_global_constr sigma c =
  match kind sigma c with
  | Const (_,u) | Ind (_,u) | Construct (_,u) -> u
  | _ -> EInstance.empty

(* Apply coercion path from p to h of type hty; raise NoCoercion if not applicable *)
let apply_coercion env sigma p h hty =
  let j, jty, trace, sigma =
    List.fold_left
      (fun (j,jty,trace,sigma) i ->
         let isid = i.coe_is_identity in
         let isproj = i.coe_is_projection in
         let sigma, c = Evd.fresh_global env sigma i.coe_value in
         let u = instance_of_global_constr sigma c in
         let isproj = Option.map (fun p ->
             p, Retyping.relevance_of_projection_repr env (p,u))
             isproj
         in
         let typ = Coercionops.coercion_type env sigma (i,u) in
         let sigma, j', args, jty =
           apply_coercion_args env sigma isproj c typ j jty i.coe_param in
         let trace =
           if isid then trace
           else match isproj with
           | None -> Coe {head=c;args;previous=trace}
           | Some (proj,relevance) ->
             let args = List.skipn (Projection.Repr.npars proj) args in
             PrimProjCoe {proj; args; relevance; previous=trace } in
         (if isid then j else j'), jty, trace, sigma)
      (h, hty, IdCoe, sigma) p
  in sigma, j, jty, trace

let remove_subset env sigma t =
  let rec aux v =
    let v' = hnf env sigma v in
    match disc_subset env sigma v' with
    | Some (u, p) ->
      aux u
    | None -> v
  in
  aux t

let mu env sigma t =
  let rec aux v =
    let v' = hnf env sigma v in
      match disc_subset env sigma v' with
      | Some (u, p) ->
        let sigma, (f, ct, trace) = aux u in
        let p = hnf_nodelta env sigma p in
        let p1 = delayed_force sig_proj1 in
        let sigma, p1 = Evd.fresh_global env sigma p1 in
        sigma,
          (Some (fun sigma x ->
                   app_opt env sigma
                     f (mkApp (p1, [| u; p; x |]))),
           ct,
           Coe {head=p1; args=[u;p]; previous=trace})
      | None -> sigma, (None, v, IdCoe)
  in aux t

let unify_product env sigma typ =
  let t = whd_all env sigma typ in
  match EConstr.kind sigma t with
  | Prod _ -> Inl sigma
  | Evar ev ->
    let sigma, _ = Evardefine.define_evar_as_product env sigma ev in
    Inl sigma
  | _ ->
    let sigma, (domain_hole, s) = Evarutil.new_type_evar env sigma Evd.univ_flexible in
    let r = ESorts.relevance_of_sort s in
    let na = make_annot Anonymous r in
    let env' = push_rel Context.(Rel.Declaration.LocalAssum (na, domain_hole)) env in
    let sigma, (codomain_hole, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in
    let prod = mkProd (na, domain_hole, codomain_hole) in
    (* NB: unification needs the un-reduced type to do heuristics like canonical structures *)
    try Inl (Evarconv.unify env sigma Conversion.CUMUL typ prod)
    with PretypeError _ -> Inr t (* return the reduced type to avoid double reducing *)

(* Invariant: if [proj] is [Some] then [args_len < npars]
     (and always [args_len = length rev_args + length args in head]) *)
type delayed_app_body = {
  mutable head : constr;
  mutable rev_args : constr list;
  args_len : int;
  proj : (Projection.Repr.t * ERelevance.t) option
}

let force_app_body ({head;rev_args} as body) =
  let head = mkApp (head, Array.rev_of_list rev_args) in
  body.head <- head;
  body.rev_args <- [];
  head

let push_arg {head;rev_args;args_len;proj} arg =
  match proj with
  | None ->
    {
      head;
      rev_args=arg::rev_args;
      args_len=args_len+1;
      proj=None;
    }
  | Some (p,r) ->
    let npars = Projection.Repr.npars p in
    if Int.equal args_len npars then
      {
        head = mkProj (Projection.make p false, r, arg);
        rev_args=[];
        args_len=0;
        proj=None;
      }
    else
      {
        head;
        rev_args=arg::rev_args;
        args_len=args_len+1;
        proj;
      }

let start_app_body sigma head =
  let proj = match EConstr.kind sigma head with
    | Const (p,u) ->
      Structures.PrimitiveProjections.find_opt_with_relevance (p,u)
    | _ -> None
  in
  {head; rev_args=[]; args_len=0; proj}

let reapply_coercions_body sigma trace body =
  match trace with
  | IdCoe -> body
  | _ ->
    let body = force_app_body body in
    let body = reapply_coercions sigma trace body in
    start_app_body sigma body

type expected = Type of types | Sort | Product

type hook = env -> evar_map -> flags:Evarconv.unify_flags -> constr ->
  inferred:types -> expected:expected -> (evar_map * constr * constr) option

let all_hooks = ref (CString.Map.empty : hook CString.Map.t)

let register_hook ~name ?(override=false) h =
  if not override && CString.Map.mem name !all_hooks then
    CErrors.anomaly ~label:"Coercion.register_hook"
      Pp.(str "Hook already registered: \"" ++ str name ++ str "\".");
  all_hooks := CString.Map.add name h !all_hooks

let active_hooks = Summary.ref ~name:"coercion_hooks" ([] : string list)

let deactivate_hook ~name =
  active_hooks := List.filter (fun s -> not (String.equal s name)) !active_hooks

let activate_hook ~name =
  assert (CString.Map.mem name !all_hooks);
  deactivate_hook ~name;
  active_hooks := name :: !active_hooks

let apply_hooks env sigma ~flags body ~inferred ~expected =
  List.find_map (fun name -> CString.Map.get name !all_hooks env sigma ~flags body ~inferred ~expected) !active_hooks

let default_flags_of env =
  default_flags_of TransparentState.full

(* Try to coerce to a funclass; raise NoCoercion if not possible *)
let inh_app_fun_core ~program_mode ?(use_coercions=true) env sigma body typ =
  match unify_product env sigma typ with
  | Inl sigma -> sigma, body, typ, IdCoe
  | Inr t ->
    try
      if not use_coercions then raise NoCoercion;
      let p = lookup_path_to_fun_from env sigma typ in
      let body = force_app_body body in
      let sigma, body, typ, trace = apply_coercion env sigma p body typ in
      sigma, start_app_body sigma body, typ, trace
    with (Not_found | NoCoercion) as exn ->
      let _, info = Exninfo.capture exn in
      if program_mode then
        try
          let sigma, (coercef, t, trace) = mu env sigma t in
          let j = {uj_val=force_app_body body; uj_type = typ} in
          let sigma, uj_val = app_opt env sigma coercef j.uj_val in
          (sigma, start_app_body sigma uj_val, t, trace)
        with NoSubtacCoercion | NoCoercion ->
          (sigma,body,typ,IdCoe)
      else Exninfo.iraise (NoCoercion,info)

(* Try to coerce to a funclass; returns [j] if no coercion is applicable *)
let inh_app_fun ~program_mode ~resolve_tc ?use_coercions env sigma ?(flags=default_flags_of env) body typ =
  try
    try inh_app_fun_core ~program_mode ?use_coercions env sigma body typ
    with
    | NoCoercion when resolve_tc
      && (get_use_typeclasses_for_conversion ()) ->
        inh_app_fun_core ~program_mode ?use_coercions env (saturate_evd env sigma) body typ
  with
  | NoCoercion -> match apply_hooks env sigma ~flags (force_app_body body) ~inferred:typ ~expected:Product with
    | Some (sigma, r, typ) -> (sigma, start_app_body sigma r, typ, ReplaceCoe r)
    | None -> (sigma, body, typ, IdCoe)

let type_judgment env sigma j =
  match EConstr.kind sigma (whd_all env sigma j.uj_type) with
    | Sort s -> {utj_val = j.uj_val; utj_type = s }
    | _ -> error_not_a_type env sigma j

let inh_tosort_force ?loc env sigma ?(flags=default_flags_of env) ({ uj_val; uj_type } as j) =
  try
    let p = lookup_path_to_sort_from env sigma uj_type in
    let sigma, uj_val, uj_type,_trace = apply_coercion env sigma p uj_val uj_type in
    let j2 = Environ.on_judgment_type (whd_evar sigma) { uj_val ; uj_type } in
      (sigma, type_judgment env sigma j2)
  with Not_found | NoCoercion -> match apply_hooks env sigma ~flags uj_val ~inferred:uj_type ~expected:Sort with
    | Some (sigma, r, typ) -> let j2 = Environ.on_judgment_type (whd_evar sigma) { uj_val = r ; uj_type = typ } in
      (sigma, type_judgment env sigma j2)
    | None -> error_not_a_type ?loc env sigma j

let inh_coerce_to_sort ?loc ?(use_coercions=true) env sigma j =
  let typ = whd_all env sigma j.uj_type in
    match EConstr.kind sigma typ with
    | Sort s -> (sigma,{ utj_val = j.uj_val; utj_type = s })
    | Evar ev ->
        let (sigma,s) = Evardefine.define_evar_as_sort env sigma ev in
          (sigma,{ utj_val = j.uj_val; utj_type = s })
    | _ ->
        if use_coercions then inh_tosort_force ?loc env sigma j
        else error_not_a_type ?loc env sigma j

let inh_coerce_to_base ?loc ~program_mode env sigma j =
  if program_mode then
    let sigma, (ct, typ', _trace) = mu env sigma j.uj_type in
    let sigma, uj_val = app_coercion env sigma ct j.uj_val in
    let res = { uj_val; uj_type = typ' } in
    sigma, res
  else (sigma, j)

let class_has_args = function
  | CL_FUN
  | CL_SORT -> false
  | _ -> true
let lookup_path_between_class_reflexive (c1,c2) =
  if c1 = c2 then []
  else lookup_path_between_class (c1,c2)

(* We find a path to a common class such that the path from src_expected is
   reversible (the casted term is unknown but inferrable via unification,
   eg CS inference) *)
let lookup_reversible_path_to_common_point env sigma ~src_expected ~src_inferred =
  let _, c_expected = class_of env sigma src_expected in
  let _, c_inferred = class_of env sigma src_inferred in
  let reachable_from_expected = reachable_from c_expected in
  let reachable_from_inferred = reachable_from c_inferred in
  let r = ClTypSet.(elements (inter reachable_from_expected reachable_from_inferred)) in
  (* XXX this order relation is not total ... *)
  let r = List.sort (fun c1 c2 -> if ClTypSet.mem c1 (reachable_from c2) then 1 else -1) r in
  let r = (if ClTypSet.mem c_inferred reachable_from_expected then [c_inferred] else []) @ r in
  (* This is unneeded since there is a dedicated case in inh_coerce_to_fail:
     let r = (if ClTypSet.mem c_expected reachable_from_inferred then [c_expected] else []) @ r in *)
  let rec aux = function
  | [] -> raise Not_found
  | c :: cs ->
      let reversible = lookup_path_between_class_reflexive (c_expected,c) in
      if path_is_reversible reversible then
        let direct = lookup_path_between_class_reflexive (c_inferred,c) in
        class_has_args c_expected, class_has_args c_inferred, reversible, direct
      else
        aux cs
  in
    aux r

let add_reverse_coercion env sigma v'_ty v_ty v' v =
  match Rocqlib.lib_ref_opt "core.coercion.reverse_coercion" with
  | None -> sigma, v'
  | Some reverse_coercion ->
     let sigma, v'_ty =
       Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible
         (Some false) env sigma v'_ty in
     let sigma, v_ty =
       Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible
         (Some false) env sigma v_ty in
     let sigma, reverse_coercion = Evd.fresh_global env sigma reverse_coercion in
     Typing.checked_appvect env sigma reverse_coercion [| v'_ty; v_ty; v'; v |]

let inh_coerce_to_fail ?(use_coercions=true) flags env sigma rigidonly v v_ty target_type =
  if not use_coercions || (rigidonly && not (Heads.is_rigid env sigma target_type && Heads.is_rigid env sigma v_ty))
  then
    raise NoCoercion
  else
    try
      let sigma, v', v'_ty, trace =
        try
          (* 1 path c of direct coercions *)
          let c = lookup_path_between env sigma ~src:v_ty ~tgt:target_type in
          apply_coercion env sigma c v v_ty
        with Not_found ->
          (* 2 paths: one of direct coercions, one of reversible coercions *)
          let target_type_has_args, v_ty_has_args, reversible, direct =
            lookup_reversible_path_to_common_point env sigma ~src_expected:target_type ~src_inferred:v_ty in
          if not (v_ty_has_args || target_type_has_args) then raise Not_found;
          let typeclass_candidate = Typeclasses.is_maybe_class_type sigma target_type in
          let sigma, x = Evarutil.new_evar ~typeclass_candidate env sigma target_type in
          let sigma, rev_x, _, _ = apply_coercion env sigma reversible x target_type in
          let sigma, direct_v, _, _ = apply_coercion env sigma direct v v_ty in
          let sigma = unify_leq_delay ~flags env sigma direct_v rev_x in
          if has_undefined_head_evar sigma x then raise Not_found;
          let sigma, rev_x = add_reverse_coercion env sigma target_type v_ty x v in
          sigma, rev_x, target_type, ReplaceCoe rev_x
      in
      unify_leq_delay ~flags env sigma v'_ty target_type, v', trace
    with (Evarconv.UnableToUnify _ | Not_found) as exn ->
      let _, info = Exninfo.capture exn in
      (* 3 if none of the above works, try hook *)
      match apply_hooks env sigma ~flags v ~inferred:v_ty ~expected:(Type target_type) with
      | Some (sigma, r, _) -> (sigma, r, ReplaceCoe r)
      | None -> Exninfo.iraise (NoCoercion,info)

let rec inh_conv_coerce_to_fail ?loc ?use_coercions env sigma ?(flags=default_flags_of env) rigidonly v t c1 =
  try (unify_leq_delay ~flags env sigma t c1, v, IdCoe)
  with UnableToUnify (best_failed_sigma,e) as exn ->
    let _, info = Exninfo.capture exn in
    try inh_coerce_to_fail ?use_coercions flags env sigma rigidonly v t c1
    with NoCoercion ->
      match
      EConstr.kind sigma (whd_all env sigma t),
      EConstr.kind sigma (whd_all env sigma c1)
      with
      | Prod (name,t1,t2), Prod (_,u1,u2) ->
          (* Conversion did not work, we may succeed with a coercion. *)
          (* We eta-expand (hence possibly modifying the original term!) *)
          (* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *)
          (* has type forall (x:u1), u2 (with v' recursively obtained) *)
          (* Note: we retype the term because template polymorphism may have *)
          (* weakened its type *)
          let name = map_annot (function
            | Anonymous -> Name Namegen.default_dependent_ident
            | na -> na) name in
          let open Context.Rel.Declaration in
          let env1 = push_rel (LocalAssum (name,u1)) env in
          let (sigma, v1, trace1) =
            inh_conv_coerce_to_fail ?loc ?use_coercions env1 sigma rigidonly
              (mkRel 1) (lift 1 u1) (lift 1 t1) in
          let v2 = beta_applist sigma (lift 1 v,[v1]) in
          let t2 = Retyping.get_type_of env1 sigma v2 in
          let (sigma,v2',trace2) = inh_conv_coerce_to_fail ?loc ?use_coercions env1 sigma rigidonly v2 t2 u2 in
          let trace = ProdCoe { na=name; ty=u1; dom=trace1; body=trace2 } in
          (sigma, mkLambda (name, u1, v2'), trace)
      | _ ->
        Exninfo.iraise (NoCoercionNoUnifier (best_failed_sigma,e), info)

let allow_all_but_patvars sigma =
  let p evk =
    try
      let EvarInfo evi = Evd.find sigma evk in
      match snd (Evd.evar_source evi) with Evar_kinds.MatchingVar _ -> false | _ -> true
    with Not_found -> true
  in
  Evarsolve.AllowedEvars.from_pred p

let default_flags_of_patvars env sigma ~patvars_abstract =
  let flags = default_flags_of env in
  if patvars_abstract then { flags with allowed_evars = allow_all_but_patvars sigma } else flags

(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
let inh_conv_coerce_to_gen ?loc ~program_mode ~resolve_tc ?use_coercions ?(patvars_abstract=false) rigidonly env sigma ?(flags=default_flags_of_patvars env sigma ~patvars_abstract) cj t =
  let (sigma, val', otrace) =
    try
      let (sigma, val', trace) = inh_conv_coerce_to_fail ?loc ?use_coercions env sigma ~flags rigidonly cj.uj_val cj.uj_type t in
      (sigma, val', Some trace)
    with NoCoercionNoUnifier (best_failed_sigma,e) as exn ->
      let _, info = Exninfo.capture exn in
      try
        if program_mode then
          let (sigma, val') = coerce_itf ?loc env sigma cj.uj_val cj.uj_type t in
          (sigma, val', None)
        else Exninfo.iraise (NoSubtacCoercion,info)
      with
      | NoSubtacCoercion as exn when not resolve_tc || not (get_use_typeclasses_for_conversion ()) ->
        let _, info = Exninfo.capture exn in
        error_actual_type ?loc ~info env best_failed_sigma cj t e
      | NoSubtacCoercion as exn ->
        let _, info = Exninfo.capture exn in
        let sigma' = saturate_evd env sigma in
          try
            if sigma' == sigma then
              error_actual_type ?loc ~info env best_failed_sigma cj t e
            else
              let sigma = sigma' in
              let (sigma, val', trace) = inh_conv_coerce_to_fail ?loc ?use_coercions env sigma rigidonly cj.uj_val cj.uj_type t in
              (sigma, val', Some trace)
          with NoCoercionNoUnifier (_sigma,_error) as exn ->
            let _, info = Exninfo.capture exn in
            error_actual_type ?loc ~info env best_failed_sigma cj t e
  in
  (sigma,{ uj_val = val'; uj_type = t },otrace)

let inh_conv_coerce_to_gen ?loc ~program_mode ~resolve_tc ?use_coercions ?patvars_abstract rigidonly env sigma ?flags cj t =
  try inh_conv_coerce_to_gen ?loc ~program_mode ~resolve_tc ?use_coercions ?patvars_abstract rigidonly env sigma ?flags cj t
  with e when Option.has_some loc ->
    let _, info as iexn = Exninfo.capture e in
    match Loc.get_loc info with
    | Some _ -> Exninfo.iraise iexn
    | None -> Exninfo.iraise (e, Loc.add_loc info (Option.get loc))

let inh_conv_coerce_to ?loc ~program_mode ~resolve_tc ?use_coercions ?patvars_abstract env sigma ?flags =
  inh_conv_coerce_to_gen ?loc ~program_mode ~resolve_tc ?use_coercions ?patvars_abstract false ?flags env sigma
let inh_conv_coerce_rigid_to ?loc ~program_mode ~resolve_tc ?use_coercions ?patvars_abstract env sigma ?flags =
  inh_conv_coerce_to_gen ?loc ~program_mode ~resolve_tc ?use_coercions ?patvars_abstract true ?flags env sigma

quality100%

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

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.