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

open CErrors
open Util
open Pp
open Names
open Constr
open Libnames
open Globnames
open Mod_subst

(* usage qque peu general: utilise aussi dans record *)

(* A class is a type constructor, its type is an arity whose number of
   arguments is cl_param (0 for CL_SORT and CL_FUN) *)

type cl_typ =
  | CL_SORT
  | CL_FUN
  | CL_SECVAR of variable
  | CL_CONST of Constant.t
  | CL_IND of inductive
  | CL_PROJ of Projection.Repr.t

let cl_typ_ord t1 t2 = match t1, t2 with
  | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
  | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2
  | CL_PROJ c1, CL_PROJ c2 -> Projection.Repr.CanOrd.compare c1 c2
  | CL_IND i1, CL_IND i2 -> Ind.CanOrd.compare i1 i2
  | _ -> Stdlib.compare t1 t2 (** OK *)

let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0

module ClTyp = struct
  type t = cl_typ
  let compare = cl_typ_ord
end

module ClTypSet = Set.Make(ClTyp)
module ClTypMap = Map.Make(ClTyp)

type cl_info_typ = {
  (* The number of parameters of the coercion class. *)
  cl_param : int;
  (* The sets of coercion classes respectively reachable from and to the
     coercion class. *)
  cl_reachable_from : ClTypSet.t;
  cl_reachable_to : ClTypSet.t;
  (* The representative class of the strongly connected component. *)
  cl_repr : cl_typ;
}

type coe_typ = GlobRef.t

module CoeTypMap = GlobRef.Map_env

type coe_info_typ = {
  coe_value : GlobRef.t;
  coe_local : bool;
  coe_reversible : bool;
  coe_is_identity : bool;
  coe_is_projection : Projection.Repr.t option;
  coe_source : cl_typ;
  coe_target : cl_typ;
  coe_param : int;
}

type inheritance_path = coe_info_typ list

let init_class_tab =
  let open ClTypMap in
  let cl_info params cl =
    let cl_singleton = ClTypSet.singleton cl in
    { cl_param = params;
      cl_reachable_from = cl_singleton;
      cl_reachable_to = cl_singleton;
      cl_repr = cl }
  in
  add CL_FUN (cl_info 0 CL_FUN) (add CL_SORT (cl_info 0 CL_SORT) empty)

let class_tab =
  Summary.ref ~name:"class_tab" (init_class_tab : cl_info_typ ClTypMap.t)

let coercion_tab =
  Summary.ref ~name:"coercion_tab" (CoeTypMap.empty : coe_info_typ CoeTypMap.t)

let reachable_from cl =
  try (ClTypMap.find cl !class_tab).cl_reachable_from
  with Not_found -> ClTypSet.empty

module ClGraph :
sig
  type t
  val empty : t
  val add : cl_typ -> cl_typ -> inheritance_path -> t -> t
  val find : cl_typ -> cl_typ -> t -> inheritance_path
  val src : cl_typ -> t -> inheritance_path ClTypMap.t
  val dst : cl_typ -> t -> inheritance_path ClTypMap.t
  val bindings : t -> ((cl_typ * cl_typ) * inheritance_path) list
end =
struct
  type map = inheritance_path ClTypMap.t ClTypMap.t
  type t = map * map
  (* Doubly-indexed map in both directions *)
  let empty = ClTypMap.empty, ClTypMap.empty
  let add0 x y p m =
    let n = try ClTypMap.find x m with Not_found -> ClTypMap.empty in
    ClTypMap.add x (ClTypMap.add y p n) m
  let add x y p (ml, mr) = (add0 x y p ml, add0 y x p mr)
  let find x y (m, _) = ClTypMap.find y (ClTypMap.find x m)
  let src x (m, _) = try ClTypMap.find x m with Not_found -> ClTypMap.empty
  let dst x (_, m) = try ClTypMap.find x m with Not_found -> ClTypMap.empty

  let bindings (m, _) =
    let fold s n accu =
      let fold t p accu = ((s, t), p) :: accu in
      ClTypMap.fold fold n accu
    in
    List.rev (ClTypMap.fold fold m [])
end

let inheritance_graph =
  Summary.ref ~name:"inheritance_graph" ClGraph.empty

(* ajout de nouveaux "objets" *)

let add_new_class cl s =
  class_tab := ClTypMap.add cl s !class_tab

let add_coercion coe s =
  coercion_tab := CoeTypMap.add coe s !coercion_tab

let add_path (x, y) p =
  inheritance_graph := ClGraph.add x y p !inheritance_graph

(* class_info : cl_typ -> int * cl_info_typ *)

let class_info cl = ClTypMap.find cl !class_tab

let class_nparams cl = (class_info cl).cl_param

let class_exists cl = ClTypMap.mem cl !class_tab

let coercion_info coe = CoeTypMap.find coe !coercion_tab

let coercion_type env sigma (coe,u) =
  Retyping.get_type_of env sigma (EConstr.mkRef (coe.coe_value,u))

let coercion_exists coe = CoeTypMap.mem coe !coercion_tab

(* find_class_type : evar_map -> constr -> cl_typ * universe_list * constr list *)

let find_class_type env sigma t =
  let open EConstr in
  let t', args = Reductionops.whd_betaiotazeta_stack env sigma t in
  match EConstr.kind sigma t' with
    | Var id -> CL_SECVAR id, EInstance.empty, args
    | Const (sp,u) -> CL_CONST sp, u, args
    | Proj (p, _, c) when not (Projection.unfolded p) ->
      let revparams =
        let open Inductiveops in
        let t = Retyping.get_type_of env sigma c in
        let IndType (fam,_) = find_rectype env sigma t in
        let _, params = dest_ind_family fam in
        List.rev params
      in
      CL_PROJ (Projection.repr p), EInstance.empty, (List.rev_append revparams (c :: args))
    | Ind (ind_sp,u) -> CL_IND ind_sp, u, args
    | Prod _ -> CL_FUN, EInstance.empty, []
    | Sort _ -> CL_SORT, EInstance.empty, []
    |  _ -> raise Not_found

let class_of_global_reference = function
  | GlobRef.VarRef id -> CL_SECVAR id
  | GlobRef.ConstRef kn -> CL_CONST kn
  | GlobRef.IndRef ind -> CL_IND ind
  | GlobRef.ConstructRef _ -> raise Not_found

let find_class_glob_type c = match DAst.get c with
  | Glob_term.GRef (ref,_) -> class_of_global_reference ref
  | Glob_term.GProd _ -> CL_FUN
  | Glob_term.GSort _ -> CL_SORT
  |  _ -> raise Not_found

let subst_cl_typ env subst ct = match ct with
    CL_SORT
  | CL_FUN
  | CL_SECVAR _ -> ct
  | CL_PROJ c ->
    let c' = subst_proj_repr subst c in
      if c' == c then ct else CL_PROJ c'
  | CL_CONST c ->
      let c',t = subst_con subst c in
      if c' == c then ct else (match t with
          | None -> CL_CONST c'
          | Some t ->
            pi1 (find_class_type env Evd.empty (EConstr.of_constr t.UVars.univ_abstracted_value)))
  | CL_IND i ->
      let i' = subst_ind subst i in
        if i' == i then ct else CL_IND i'

(*CSC: here we should change the datatype for coercions: it should be possible
       to declare any term as a coercion *)
let subst_coe_typ subst t = subst_global_reference subst t

(* class_of : Term.constr -> int *)

let class_of env sigma t =
  let (t, n1, cl, u, args) =
    try
      let (cl, u, args) = find_class_type env sigma t in
      let { cl_param = n1 } = class_info cl in
      (t, n1, cl, u, args)
    with Not_found ->
      let t = Tacred.hnf_constr0 env sigma t in
      let (cl, u, args) = find_class_type env sigma t in
      let { cl_param = n1 } = class_info cl in
      (t, n1, cl, u, args)
  in
  if Int.equal (List.length args) n1 then t, cl else raise Not_found

let class_args_of env sigma c = pi3 (find_class_type env sigma c)

let string_of_class = function
  | CL_FUN -> "Funclass"
  | CL_SORT -> "Sortclass"
  | CL_CONST sp ->
    string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.ConstRef sp))
  | CL_PROJ sp ->
    let sp = Projection.Repr.constant sp in
    string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.ConstRef sp))
  | CL_IND sp ->
      string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.IndRef sp))
  | CL_SECVAR sp ->
      string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.VarRef sp))

let pr_class x = str (string_of_class x)

(* lookup paths *)

let lookup_path_between_class (s,t) =
  ClGraph.find s t !inheritance_graph

let lookup_path_to_fun_from_class s =
  lookup_path_between_class (s, CL_FUN)

let lookup_path_to_sort_from_class s =
  lookup_path_between_class (s, CL_SORT)

(* advanced path lookup *)

let apply_on_class_of env sigma t cont =
  try
    let (cl,u,args) = find_class_type env sigma t in
    let { cl_param = n1 } = class_info cl in
    if not (Int.equal (List.length args) n1) then raise Not_found;
    cont cl
  with Not_found ->
    (* Is it worth to be more incremental on the delta steps? *)
    let t = Tacred.hnf_constr0 env sigma t in
    let (cl, u, args) = find_class_type env sigma t in
    let { cl_param = n1 } = class_info cl in
    if not (Int.equal (List.length args) n1) then raise Not_found;
    cont cl

let lookup_path_between env sigma ~src:s ~tgt:t =
  apply_on_class_of env sigma s (fun i ->
      apply_on_class_of env sigma t (fun j ->
          lookup_path_between_class (i,j)))

let lookup_path_to_fun_from env sigma s =
  apply_on_class_of env sigma s lookup_path_to_fun_from_class

let lookup_path_to_sort_from env sigma s =
  apply_on_class_of env sigma s lookup_path_to_sort_from_class

let get_coercion_constructor env coe =
  let evd = Evd.from_env env in
  let evd, c = Evd.fresh_global env evd coe.coe_value in
  let c = fst (Reductionops.whd_all_stack env evd c) in
  match EConstr.kind evd c with
  | Constr.Construct (c, _) ->
    (* we don't return the modified evd as we drop the universes *)
    c, Inductiveops.constructor_nrealargs env c -1
  | _ -> raise Not_found

let lookup_pattern_path_between env (s,t) =
  List.map (get_coercion_constructor env)
    (ClGraph.find (CL_IND s) (CL_IND t) !inheritance_graph)

let path_is_reversible p =
  List.for_all (fun c -> c.coe_reversible) p

(* rajouter une coercion dans le graphe *)

let path_printer : ((cl_typ * cl_typ) * inheritance_path -> Pp.t) ref =
  ref (fun _ -> str "")

let install_path_printer f = path_printer := f

let print_path x = !path_printer x

let path_comparator :
  (Environ.env -> Evd.evar_map -> cl_typ -> inheritance_path -> inheritance_path -> bool) ref =
  ref (fun _ _ _ _ _ -> false)

let install_path_comparator f = path_comparator := f

let compare_path env sigma cl p q = !path_comparator env sigma cl p q

let warning_ambiguous_path = "ambiguous-paths"

let warn_ambiguous_path =
  CWarnings.create ~name:warning_ambiguous_path ~category:CWarnings.CoreCategories.coercions
    (fun l -> prlist_with_sep fnl (fun (c,p,q) ->
         str"New coercion path " ++ print_path (c,p) ++
         if List.is_empty q then
           str" is not definitionally an identity function."
         else
           str" is ambiguous with existing " ++ print_path (c, q) ++ str".") l)

(* add_coercion_in_graph : coe_index * cl_typ * cl_typ -> unit
                         coercion,source,target *)

let different_class_params env ci =
  if (class_info ci).cl_param > 0 then true
  else
    match ci with
    | CL_IND i -> Environ.is_polymorphic env (GlobRef.IndRef i)
    | CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c)
    | _ -> false

let add_coercion_in_graph env sigma ?(update=false) ic =
  let source = ic.coe_source in
  let target = ic.coe_target in
  let source_info = class_info source in
  let target_info = class_info target in
  let old_inheritance_graph = !inheritance_graph in
  let ambig_paths :
    ((cl_typ * cl_typ) * inheritance_path * inheritance_path) list ref =
    ref [] in
  let warn = match CWarnings.get_warning warning_ambiguous_path with
  | There w ->
    begin match CWarnings.warning_status w with
    | Disabled -> false
    | Enabled | AsError -> true
    end
  | NotThere | OtherType -> assert false
  in
  let check_coherence (i, j as ij) p q =
    if warn then
    let i_info = class_info i in
    let j_info = class_info j in
    let between_ij = ClTypSet.inter i_info.cl_reachable_from j_info.cl_reachable_to in
    if cl_typ_eq i_info.cl_repr i &&
       cl_typ_eq j_info.cl_repr j &&
       ClTypSet.is_empty
         (ClTypSet.diff (ClTypSet.inter between_ij source_info.cl_reachable_to)
            i_info.cl_reachable_to) &&
       ClTypSet.is_empty
         (ClTypSet.diff
            (ClTypSet.inter between_ij target_info.cl_reachable_from)
            j_info.cl_reachable_from) &&
       not (compare_path env sigma i p q)
    then
      ambig_paths := (ij, p, q) :: !ambig_paths
  in
  let try_add_new_path (i,j as ij) p =
    let () = if cl_typ_eq i j then check_coherence ij p [] in
    if not (cl_typ_eq i j) || different_class_params env i then
      if update then let () = add_path ij p in true else
        match lookup_path_between_class ij with
        | q -> (if not (cl_typ_eq i j) then check_coherence ij p q); false
        | exception Not_found -> add_path ij p; true
    else
      false
  in
  if try_add_new_path (source, target) [ic] then begin
    let rev = ClGraph.dst source old_inheritance_graph in
    let dir = ClGraph.src target old_inheritance_graph in
    let iter s p =
      if not (cl_typ_eq s source) then
        let _ = try_add_new_path (s, target) (p@[ic]) in
        let iter v q =
          if not (cl_typ_eq target v) then
            ignore (try_add_new_path (s,v) (p@[ic]@q))
        in
        ClTypMap.iter iter dir
    in
    let () = ClTypMap.iter iter rev in
    let iter t p =
      if not (cl_typ_eq t target) then
        ignore (try_add_new_path (source, t) (ic::p))
    in
    ClTypMap.iter iter dir
  end;
  class_tab := ClTypMap.mapi (fun k k_info ->
      let reachable_k_source = ClTypSet.mem k source_info.cl_reachable_to in
      let reachable_target_k = ClTypSet.mem k target_info.cl_reachable_from in
      { k_info with
        cl_reachable_from =
          if reachable_k_source then
            ClTypSet.union
              k_info.cl_reachable_from target_info.cl_reachable_from
          else
            k_info.cl_reachable_from;
        cl_reachable_to =
          if reachable_target_k then
            ClTypSet.union k_info.cl_reachable_to source_info.cl_reachable_to
          else
            k_info.cl_reachable_to;
        cl_repr =
          if reachable_k_source && reachable_target_k then
            target_info.cl_repr
          else
            k_info.cl_repr
      }) !class_tab;
  match !ambig_paths with [] -> () | _ -> warn_ambiguous_path !ambig_paths

let subst_coercion subst c =
  let env = Global.env () in
  let coe = subst_coe_typ subst c.coe_value in
  let cls = subst_cl_typ env subst c.coe_source in
  let clt = subst_cl_typ env subst c.coe_target in
  let clp = Option.Smart.map (subst_proj_repr subst) c.coe_is_projection in
  if c.coe_value == coe && c.coe_source == cls && c.coe_target == clt &&
     c.coe_is_projection == clp
  then c
  else { c with coe_value = coe; coe_source = cls; coe_target = clt;
                coe_is_projection = clp; }

(* Computation of the class arity *)

let reference_arity_length env sigma ref =
  let t, _ = Typeops.type_of_global_in_context env ref in
  List.length (fst (Reductionops.splay_arity env sigma (EConstr.of_constr t)))

let projection_arity_length env sigma p =
  reference_arity_length env sigma (GlobRef.ConstRef (Projection.Repr.constant p))

let class_params env sigma = function
  | CL_FUN | CL_SORT -> 0
  | CL_CONST sp -> reference_arity_length env sigma (GlobRef.ConstRef sp)
  | CL_PROJ sp -> projection_arity_length env sigma sp
  | CL_SECVAR sp -> reference_arity_length env sigma (GlobRef.VarRef sp)
  | CL_IND sp  -> reference_arity_length env sigma (GlobRef.IndRef sp)

(* add_class : cl_typ -> locality_flag option -> bool -> unit *)

let add_class env sigma cl =
  if not (class_exists cl) then
    let cl_singleton = ClTypSet.singleton cl in
    add_new_class cl {
      cl_param = class_params env sigma cl;
      cl_reachable_from = cl_singleton;
      cl_reachable_to = cl_singleton;
      cl_repr = cl }

let declare_coercion env sigma ?update c =
  let () = add_class env sigma c.coe_source in
  let () = add_class env sigma c.coe_target in
  let () = add_coercion c.coe_value c in
  add_coercion_in_graph env sigma ?update c

(* For printing purpose *)
let classes () =
  List.rev (ClTypMap.fold (fun x _ acc -> x :: acc) !class_tab [])
let coercions () =
  List.rev (CoeTypMap.fold (fun _ y acc -> y::acc) !coercion_tab [])

let inheritance_graph () =
  ClGraph.bindings !inheritance_graph

let coercion_of_reference r =
  let ref = Nametab.global r in
  if not (coercion_exists ref) then
    user_err
      (Nametab.pr_global_env Id.Set.empty ref ++ str" is not a coercion.");
  ref

module CoercionPrinting =
  struct
    type t = coe_typ
    module Set = GlobRef.Set
    let encode _env = coercion_of_reference
    let subst = subst_coe_typ

    let check_local local = let open GlobRef in function
      | ConstRef _ | ConstructRef _ | IndRef _ -> ()
      | VarRef x -> match local with
        | Libobject.Local -> ()
        | Export | SuperGlobal ->
          let local = if local = Export then "export" else "global" in
          CErrors.user_err
            Pp.(Id.print x ++ str " cannot be added with locality " ++ str local ++ str ".")

    let discharge = let open GlobRef in function
      | ConstRef _ | ConstructRef _ | IndRef _ as x -> x
      | VarRef _ as x -> assert (not (Global.is_in_section x)); x

    let printer x = Nametab.pr_global_env Id.Set.empty x
    let key = ["Printing";"Coercion"]
    let title = "Explicitly printed coercions: "
    let member_message x b =
      str "Explicit printing of coercion " ++ printer x ++
      str (if b then " is set" else " is unset")
  end

module PrintingCoercion  = Goptions.MakeRefTable(CoercionPrinting)

let hide_coercion coe =
  if not (PrintingCoercion.active coe) then
    let coe_info = coercion_info coe in
    Some coe_info.coe_param
  else None

quality97%

¤ Dauer der Verarbeitung: 0.15 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.