aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/termast.ml12
-rwxr-xr-xpretyping/classops.ml14
-rw-r--r--pretyping/classops.mli113
-rw-r--r--toplevel/vernacentries.ml64
4 files changed, 143 insertions, 60 deletions
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 8e7cc12af2..3d72f4adcd 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -155,11 +155,13 @@ let rec skip_coercion dest_ref (f,args as app) =
try
match dest_ref f with
| Some r ->
- let n = Classops.coercion_params r in
- if n >= List.length args then app
- else (* We skip a coercion *)
- let _,fargs = list_chop n args in
- skip_coercion dest_ref (List.hd fargs,List.tl fargs)
+ (match Classops.hide_coercion r with
+ | Some n ->
+ if n >= List.length args then app
+ else (* We skip a coercion *)
+ let _,fargs = list_chop n args in
+ skip_coercion dest_ref (List.hd fargs,List.tl fargs)
+ | None -> app)
| None -> app
with Not_found -> app
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 710a723e36..0b190db0e8 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -138,9 +138,17 @@ let coe_of_reference = function
| EvarRef _ -> raise Not_found
| x -> x
-let hide_coercion r =
- let _,coe_info = coercion_info (coe_of_reference r) in
- if coe_info.coe_hide then None else Some coe_info.coe_param
+let hide_coercion coe =
+ let _,coe_info = coercion_info coe in
+ if coe_info.coe_hide then Some coe_info.coe_param else None
+
+let set_coercion_visibility b coe =
+ let _,coe_info = coercion_info coe in
+ coe_info.coe_hide <- not b
+
+let is_coercion_visible coe =
+ let _,coe_info = coercion_info coe in
+ not coe_info.coe_hide
let coercion_params coe_info = coe_info.coe_param
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index fec858a590..4ccf02b1f5 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -2,16 +2,14 @@
(*i $Id$ i*)
(*i*)
-open Pp
open Names
open Term
open Evd
open Environ
-open Libobject
open Declare
-open Rawterm
(*i*)
+(*s This is the type of class kinds *)
type cl_typ =
| CL_SORT
| CL_FUN
@@ -19,64 +17,91 @@ type cl_typ =
| CL_CONST of constant_path
| CL_IND of inductive_path
+(* This is the type of infos for declared classes *)
type cl_info_typ = {
- cL_STRE : strength;
- cL_PARAM : int }
+ cl_strength : strength;
+ cl_param : int }
-type cte_typ =
- | NAM_Section_Variable of variable_path
- | NAM_Constant of constant_path
- | NAM_Inductive of inductive_path
- | NAM_Constructor of constructor_path
+(* This is the type of coercion kinds *)
+type coe_typ = global_reference
-type coe_typ = cte_typ
+(* This is the type of infos for declared coercions *)
+type coe_info_typ
+(* [cl_index] is the type of class keys *)
+type cl_index
-type coe_info_typ = {
- cOE_VALUE : unsafe_judgment;
- cOE_STRE : strength;
- cOE_ISID : bool;
- cOE_PARAM : int }
+(* [coe_index] is the type of coercion keys *)
+type coe_index
-type inheritance_path = int list
+(* This is the type of paths from a class to another *)
+type inheritance_path = coe_index list
-val inheritance_graph : unit -> ((int * int) * inheritance_path) list
-val classes : unit -> (int * (cl_typ * cl_info_typ)) list
-val coercions : unit -> (int * (coe_typ * coe_info_typ)) list
+val cte_of_constr : constr -> global_reference
+val coe_of_reference : global_reference -> coe_typ
-val cte_of_constr : constr -> cte_typ
-val class_info : cl_typ -> (int * cl_info_typ)
-val class_exists : cl_typ -> bool
-val class_info_from_index : int -> cl_typ * cl_info_typ
-val coercion_exists : coe_typ -> bool
-val coercion_info : coe_typ -> (int * coe_info_typ)
-val coercion_info_from_index : int -> coe_typ * coe_info_typ
+(*s [declare_class] adds a class to the set of declared classes *)
+val declare_class : cl_typ * strength * int -> unit
-(* [coercion_params] raises [Not_found] if not a coercion *)
-val coercion_params : global_reference -> int
+(*s Access to classes infos *)
+val class_info : cl_typ -> (cl_index * cl_info_typ)
+val class_exists : cl_typ -> bool
+val class_info_from_index : cl_index -> cl_typ * cl_info_typ
+(* [constructor_at_head c] returns the head reference of c and its
+ number of arguments *)
val constructor_at_head : constr -> cl_typ * int
(* raises [Not_found] if not convertible to a class *)
-val class_of : env -> 'c evar_map -> constr -> constr * int
+val class_of : env -> 'c evar_map -> constr -> constr * cl_index
val class_args_of : constr -> constr list
-val inClass : (cl_typ * cl_info_typ) -> obj
-val outClass : obj -> (cl_typ * cl_info_typ)
-val inCoercion : (coe_typ * coe_info_typ) * cl_typ * cl_typ -> obj
-val outCoercion : obj -> (coe_typ * coe_info_typ) * cl_typ * cl_typ
-val lookup_path_between : (int * int) -> inheritance_path
-val lookup_path_to_fun_from : int -> inheritance_path
-val lookup_path_to_sort_from : int -> inheritance_path
-val coe_value : int -> (unsafe_judgment * bool)
-val stre_of_cl : cl_typ -> strength
-val add_new_class : cl_typ * strength * int -> unit
-val add_new_coercion_in_graph :
- (coe_typ * coe_info_typ) * cl_typ * cl_typ -> unit
-val add_coercion_in_graph : int * int * int -> unit
+val strength_of_cl : cl_typ -> strength
+
+(*s [declare_coercion] adds a coercion in the graph of coercion paths *)
+val declare_coercion :
+ coe_typ -> value:unsafe_judgment -> strength:strength -> isid:bool ->
+ src:cl_typ -> target:cl_typ -> params:int -> unit
+
+(*s Access to coercions infos *)
+val coercion_exists : coe_typ -> bool
+val coercion_info_from_index : coe_index -> coe_typ * coe_info_typ
+
+val coercion_value : coe_index -> (unsafe_judgment * bool)
+
+(*s This is for printing purpose *)
+
+(* [hide_coercion] returns the number of params to skip if the coercion must
+ be hidden, [None] otherwise; it raises [Not_found] if not a coercion *)
+val hide_coercion : coe_typ -> int option
+
+val set_coercion_visibility : bool -> coe_typ -> unit
+val is_coercion_visible : coe_typ -> bool
+
+(*s Lookup functions for coercion paths *)
+val lookup_path_between : (cl_index * cl_index) -> inheritance_path
+val lookup_path_to_fun_from : cl_index -> inheritance_path
+val lookup_path_to_sort_from : cl_index -> inheritance_path
+
+(*i Pour le discharge *)
+open Libobject
+val inClass : (cl_typ * cl_info_typ) -> Libobject.obj
+val outClass : Libobject.obj -> (cl_typ * cl_info_typ)
+val inCoercion : (coe_typ * coe_info_typ) * cl_typ * cl_typ -> Libobject.obj
+val outCoercion : Libobject.obj -> (coe_typ * coe_info_typ) * cl_typ * cl_typ
+val coercion_strength : coe_info_typ -> strength
+(*i*)
+
+(*i Crade *)
+open Pp
val install_path_printer :
- ((int * int) * inheritance_path -> std_ppcmds) -> unit
+ ((cl_index * cl_index) * inheritance_path -> std_ppcmds) -> unit
+(*i*)
(* This is for printing purpose *)
val string_of_class : cl_typ -> string
+val get_coercion_value : coe_info_typ -> constr
+val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
+val classes : unit -> (int * (cl_typ * cl_info_typ)) list
+val coercions : unit -> (int * (coe_typ * coe_info_typ)) list
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 96fbd375d8..d8389ac05a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -472,29 +472,77 @@ let _ =
message "Implicit arguments mode is unset")
| _ -> bad_vernac_args "IMPLICIT_ARGS_OFF")
-let _ =
+let coercion_of_qualid loc qid =
+ let ref = global loc qid in
+ let coe = Classops.coe_of_reference ref in
+ if not (Classops.coercion_exists coe) then
+ errorlabstrm "try_add_coercion"
+ [< Printer.pr_global ref; 'sTR" is not a coercion" >];
+ coe
+
+let _ =
add "PRINTING_COERCIONS_ON"
(function
| [] -> (fun () -> Termast.print_coercions := true)
- | _ -> bad_vernac_args "PRINTING_COERCIONS_ON")
+ | l ->
+ let ql =
+ List.map
+ (function
+ | VARG_QUALID qid -> qid
+ | _ -> bad_vernac_args "PRINTING_COERCIONS_ON") l in
+ (fun () ->
+ List.iter
+ (fun qid ->
+ Classops.set_coercion_visibility true
+ (coercion_of_qualid dummy_loc qid))
+ ql))
let _ =
add "PRINTING_COERCIONS_OFF"
(function
| [] -> (fun () -> Termast.print_coercions := false)
- | _ -> bad_vernac_args "PRINTING_COERCIONS_OFF")
+ | l ->
+ let ql =
+ List.map
+ (function
+ | VARG_QUALID qid -> qid
+ | _ -> bad_vernac_args "PRINTING_COERCIONS_OFF") l in
+ (fun () ->
+ List.iter
+ (fun qid ->
+ Classops.set_coercion_visibility false
+ (coercion_of_qualid dummy_loc qid))
+ ql))
let _ =
add "TEST_PRINTING_COERCIONS"
(function
| [] ->
- (fun () ->
- if !(Termast.print_coercions) = true then
+ (fun () ->
+ if !(Termast.print_coercions) = true then
message "Printing of coercions is set"
- else
+ else
message "Printing of coercions is unset")
- | _ -> bad_vernac_args "TEST_PRINTING_COERCIONS")
-
+ | l ->
+ let ql =
+ List.map
+ (function
+ | VARG_QUALID qid -> qid
+ | _ -> bad_vernac_args "TEST_PRINTING_COERCIONS") l in
+ (fun () ->
+ List.iter
+ (fun qid ->
+ let coe = coercion_of_qualid dummy_loc qid in
+ if Classops.is_coercion_visible coe then
+ message
+ ("Printing of coercion "^(string_of_qualid qid)^
+ " is set")
+ else
+ message
+ ("Printing of coercion "^(string_of_qualid qid)^
+ " is unset"))
+ ql))
+
let number_list =
List.map (function VARG_NUMBER n -> n | _ -> bad_vernac_args "Number list")
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:44:15 +0000