aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/pretty.ml6
-rwxr-xr-xpretyping/classops.ml156
-rwxr-xr-xpretyping/recordops.ml3
-rwxr-xr-xpretyping/recordops.mli6
-rw-r--r--toplevel/class.ml53
-rw-r--r--toplevel/discharge.ml8
6 files changed, 121 insertions, 111 deletions
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index d7d092685..eb6b20719 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -439,7 +439,7 @@ let string_of_strength = function
| NeverDischarge -> "(global)"
| DischargeAt sp -> "(disch@"^(string_of_dirpath sp)
-let print_coercion_value v = prterm v.cOE_VALUE.uj_val
+let print_coercion_value v = prterm (get_coercion_value v)
let print_index_coercion c =
let _,v = coercion_info_from_index c in
@@ -465,7 +465,7 @@ let print_classes () =
[< prlist_with_sep pr_spc
(fun (_,(cl,x)) ->
[< 'sTR (string_of_class cl)
- (*; 'sTR(string_of_strength x.cL_STRE) *) >])
+ (*; 'sTR(string_of_strength x.cl_strength) *) >])
(classes()) >]
let print_coercions () =
@@ -483,7 +483,7 @@ let cl_of_id id =
let index_cl_of_id id =
try
let cl = cl_of_id id in
- let i,_=class_info cl in
+ let i,_ = class_info cl in
i
with _ ->
errorlabstrm "index_cl_of_id"
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 2afe796d4..710a723e3 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -20,10 +20,10 @@ type cte_typ =
| NAM_Constructor of constructor_path
let cte_of_constr c = match kind_of_term c with
- | IsConst (sp,_) -> NAM_Constant sp
- | IsMutInd (ind_sp,_) -> NAM_Inductive ind_sp
- | IsMutConstruct (cstr_cp,_) -> NAM_Constructor cstr_cp
- | IsVar id -> NAM_Section_Variable (find_section_variable id)
+ | IsConst (sp,_) -> ConstRef sp
+ | IsMutInd (ind_sp,_) -> IndRef ind_sp
+ | IsMutConstruct (cstr_cp,_) -> ConstructRef cstr_cp
+ | IsVar id -> VarRef (find_section_variable id)
| _ -> raise Not_found
type cl_typ =
@@ -34,40 +34,41 @@ type cl_typ =
| CL_IND of inductive_path
type cl_info_typ = {
- cL_STRE : strength;
- cL_PARAM : int }
+ cl_strength : strength;
+ cl_param : int }
-type coe_typ = cte_typ
+type coe_typ = global_reference
type coe_info_typ = {
- cOE_VALUE : unsafe_judgment;
- cOE_STRE : strength;
- cOE_ISID : bool;
- cOE_PARAM : int }
+ coe_value : unsafe_judgment;
+ coe_strength : strength;
+ coe_is_identity : bool;
+ coe_param : int;
+ mutable coe_hide : bool }
-type inheritance_path = int list
+type cl_index = int
+type coe_index = int
+type inheritance_path = coe_index list
-(* table des classes, des coercions et graphe d'heritage *)
-
-let cLASSES = (ref [] : (int * (cl_typ * cl_info_typ)) list ref)
-
-let classes () = !cLASSES
-let cOERCIONS = (ref [] : (int * (coe_typ * coe_info_typ)) list ref)
+(* table des classes, des coercions et graphe d'heritage *)
-let coercions () = !cOERCIONS
+let class_tab =
+ (ref [] : (cl_index * (cl_typ * cl_info_typ)) list ref)
-let iNHERITANCE_GRAPH = (ref [] : ((int * int) * inheritance_path) list ref)
+let coercion_tab =
+ (ref [] : (coe_index * (coe_typ * coe_info_typ)) list ref)
-let inheritance_graph () = !iNHERITANCE_GRAPH
+let inheritance_graph =
+ (ref [] : ((cl_index * cl_index) * inheritance_path) list ref)
-let freeze () = (!cLASSES,!cOERCIONS, !iNHERITANCE_GRAPH)
+let freeze () = (!class_tab, !coercion_tab, !inheritance_graph)
let unfreeze (fcl,fco,fig) =
- cLASSES:=fcl;
- cOERCIONS:=fco;
- iNHERITANCE_GRAPH:=fig
+ class_tab:=fcl;
+ coercion_tab:=fco;
+ inheritance_graph:=fig
(* ajout de nouveaux "objets" *)
@@ -80,27 +81,27 @@ let newNum_coercion =
function () -> (num:=!num+1;!num)
let add_new_class_num (n,(cl,s)) =
- cLASSES := (n,(cl,s))::(!cLASSES)
+ class_tab := (n,(cl,s))::(!class_tab)
-let add_new_class1 (cl,s) =
+let add_new_class (cl,s) =
add_new_class_num (newNum_class(),(cl,s))
let add_new_coercion_num (n,(coe,s)) =
- cOERCIONS := (n,(coe,s))::(!cOERCIONS)
+ coercion_tab := (n,(coe,s))::(!coercion_tab)
let add_new_coercion (coe,s) =
let n = newNum_coercion() in
add_new_coercion_num (n,(coe,s));n
let add_new_path x =
- iNHERITANCE_GRAPH := x::(!iNHERITANCE_GRAPH)
+ inheritance_graph := x::!inheritance_graph
let init () =
- cLASSES:= [];
- add_new_class1 (CL_FUN, { cL_PARAM=0; cL_STRE=NeverDischarge });
- add_new_class1 (CL_SORT, { cL_PARAM=0; cL_STRE=NeverDischarge });
- cOERCIONS:= [];
- iNHERITANCE_GRAPH:= []
+ class_tab:= [];
+ add_new_class (CL_FUN, { cl_param = 0; cl_strength = NeverDischarge });
+ add_new_class (CL_SORT, { cl_param = 0; cl_strength = NeverDischarge });
+ coercion_tab:= [];
+ inheritance_graph:= []
let _ = init()
@@ -115,7 +116,7 @@ let search_info x l =
(* class_info : cl_typ -> int * cl_info_typ *)
-let class_info cl = search_info cl (!cLASSES)
+let class_info cl = search_info cl (!class_tab)
let class_exists cl =
try let _ = class_info cl in true
@@ -123,34 +124,33 @@ let class_exists cl =
(* class_info_from_index : int -> cl_typ * cl_info_typ *)
-let class_info_from_index i = List.assoc i (!cLASSES)
+let class_info_from_index i = List.assoc i !class_tab
(* coercion_info : coe_typ -> int * coe_info_typ *)
-let coercion_info coe = search_info coe (!cOERCIONS)
+let coercion_info coe = search_info coe !coercion_tab
let coercion_exists coe =
try let _ = coercion_info coe in true
with Not_found -> false
let coe_of_reference = function
- | ConstRef sp -> NAM_Constant sp
- | IndRef sp -> NAM_Inductive sp
- | ConstructRef sp -> NAM_Constructor sp
- | VarRef sp -> NAM_Section_Variable sp
| EvarRef _ -> raise Not_found
+ | x -> x
-let coercion_params r =
+let hide_coercion r =
let _,coe_info = coercion_info (coe_of_reference r) in
- coe_info.cOE_PARAM
+ if coe_info.coe_hide then None else Some coe_info.coe_param
+
+let coercion_params coe_info = coe_info.coe_param
(* coercion_info_from_index : int -> coe_typ * coe_info_typ *)
let coercion_info_from_index i =
- List.assoc i (!cOERCIONS)
+ List.assoc i !coercion_tab
let lookup_path_between (s,t) =
- List.assoc (s,t) (!iNHERITANCE_GRAPH)
+ List.assoc (s,t) !inheritance_graph
let lookup_path_to_fun_from s =
lookup_path_between (s,fst(class_info CL_FUN))
@@ -163,7 +163,7 @@ let lookup_path_to_sort_from s =
(*val inClass : (cl_typ * cl_info_typ) -> Libobject.object = <fun>
val outClass : Libobject.object -> (cl_typ * cl_info_typ) = <fun> *)
-let cache_class (_,x) = add_new_class1 x
+let cache_class (_,x) = add_new_class x
let (inClass,outClass) =
declare_object ("CLASS",
@@ -172,8 +172,8 @@ let (inClass,outClass) =
cache_function = cache_class;
export_function = (function x -> Some x) })
-let add_new_class (cl,stre,p) =
- Lib.add_anonymous_leaf (inClass ((cl,{cL_STRE=stre;cL_PARAM=p})))
+let declare_class (cl,stre,p) =
+ Lib.add_anonymous_leaf (inClass ((cl,{ cl_strength = stre; cl_param = p })))
let _ =
Summary.declare_summary "inh_graph"
@@ -206,19 +206,19 @@ let class_of env sigma t =
let t,n,n1,i =
(try
let (cl,n) = constructor_at_head t in
- let (i,{cL_PARAM=n1}) = class_info cl in
+ let (i,{cl_param=n1}) = class_info cl in
t,n,n1,i
with _ ->
let t = Tacred.hnf_constr env sigma t in
let (cl,n) = constructor_at_head t in
- let (i,{cL_PARAM=n1}) = class_info cl in
+ let (i,{cl_param=n1}) = class_info cl in
t,n,n1,i)
in
if n = n1 then t,i else raise Not_found
let class_args_of c = snd (decomp_app c)
-let stre_of_cl = function
+let strength_of_cl = function
| CL_CONST sp -> constant_or_parameter_strength sp
| CL_SECVAR sp -> variable_strength sp
| _ -> NeverDischarge
@@ -230,18 +230,12 @@ let string_of_class = function
| CL_IND sp -> string_of_qualid (Global.qualid_of_global (IndRef sp))
| CL_SECVAR sp -> string_of_qualid (Global.qualid_of_global (VarRef sp))
-(* coe_value : int -> Term.constr * bool *)
+(* coercion_value : int -> unsafe_judgment * bool *)
-let coe_value i =
- let (coe,{cOE_VALUE=_;cOE_ISID=b}) = coercion_info_from_index i in
+let coercion_value i =
+ let (coe,{ coe_is_identity = b }) = coercion_info_from_index i in
let env = Global.env () in
- let v = match coe with
- | NAM_Section_Variable sp -> constr_of_reference Evd.empty env (VarRef sp)
- | NAM_Constant sp -> constr_of_reference Evd.empty env (ConstRef sp)
- | NAM_Constructor ((sp,i),j) ->
- constr_of_reference Evd.empty env (ConstructRef ((sp,i),j))
- | NAM_Inductive (sp,i) ->
- constr_of_reference Evd.empty env (IndRef (sp,i)) in
+ let v = constr_of_reference Evd.empty env coe in
let j = Retyping.get_judgment_of env Evd.empty v in
(j,b)
@@ -259,16 +253,17 @@ let message_ambig l =
[< 'sTR"Ambiguous paths:"; 'sPC;
prlist_with_sep pr_fnl (fun ijp -> print_path ijp) l >]
-(* add_coercion_in_graph : int * int * int -> unit
+(* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
coercion,source,target *)
let add_coercion_in_graph (ic,source,target) =
- let old_iNHERITANCE_GRAPH = !iNHERITANCE_GRAPH in
- let ambig_paths = (ref []:((int * int) * inheritance_path) list ref) in
+ let old_inheritance_graph = !inheritance_graph in
+ let ambig_paths =
+ (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
let try_add_new_path (p,i,j) =
try
if i=j then begin
- if (snd (class_info_from_index i)).cL_PARAM > 0 then begin
+ if (snd (class_info_from_index i)).cl_param > 0 then begin
let _ = lookup_path_between (i,j) in
ambig_paths := ((i,j),p)::!ambig_paths
end
@@ -295,19 +290,19 @@ let add_coercion_in_graph (ic,source,target) =
(fun ((u,v),q) ->
if u<>v & (u = target) & (p <> q) then
try_add_new_path1 (p @ [ ic ] @ q,s,v))
- old_iNHERITANCE_GRAPH
+ old_inheritance_graph
end;
if s = target then try_add_new_path1 (ic::p,source,t)
end)
- old_iNHERITANCE_GRAPH
+ old_inheritance_graph
end;
if (!ambig_paths <> []) & is_mes_ambig() then
pPNL (message_ambig !ambig_paths)
-let add_new_coercion_in_graph ((coef,xf),cls,clt) =
+let cache_coercion (_,((coe,xf),cls,clt)) =
let is,_ = class_info cls in
let it,_ = class_info clt in
- let jf = add_new_coercion (coef,xf) in
+ let jf = add_new_coercion (coe,xf) in
add_coercion_in_graph (jf,is,it)
(* val inCoercion : (coe_typ * coe_info_typ) * cl_typ * cl_typ ->
@@ -315,11 +310,30 @@ let add_new_coercion_in_graph ((coef,xf),cls,clt) =
val outCoercion : Libobject.object -> (coe_typ * coe_info_typ)
* cl_typ * cl_typ *)
-let cache_coercion (_,x) = add_new_coercion_in_graph x
-
let (inCoercion,outCoercion) =
declare_object ("COERCION",
{ load_function = (fun _ -> ());
open_function = cache_coercion;
cache_function = cache_coercion;
export_function = (function x -> Some x) })
+
+let declare_coercion coef v stre isid cls clt ps =
+ Lib.add_anonymous_leaf
+ (inCoercion
+ ((coef,
+ { coe_value = v;
+ coe_strength = stre;
+ coe_is_identity = isid;
+ coe_param = ps;
+ coe_hide = true }),
+ cls, clt))
+
+let coercion_strength v = v.coe_strength
+(* For printing purpose *)
+let get_coercion_value v = v.coe_value.uj_val
+
+let classes () = !class_tab
+let coercions () = !coercion_tab
+let inheritance_graph () = !inheritance_graph
+
+
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index d02ca06db..6db3545ce 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -62,7 +62,8 @@ type obj_typ = {
o_TPARAMS : constr list; (* dans l'ordre *)
o_TCOMPS : constr list } (* dans l'ordre *)
-let oBJDEFS = (ref [] : ((cte_typ * cte_typ) * obj_typ) list ref)
+let oBJDEFS =
+ (ref [] : ((global_reference * global_reference) * obj_typ) list ref)
let add_new_objdef1 x = oBJDEFS:=x::(!oBJDEFS)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index f82e074ba..097eb25b8 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -34,9 +34,9 @@ type obj_typ = {
o_TPARAMS : constr list; (* dans l'ordre *)
o_TCOMPS : constr list } (* dans l'ordre *)
-val objdef_info : (cte_typ * cte_typ) -> obj_typ
+val objdef_info : (global_reference * global_reference) -> obj_typ
val add_new_objdef :
- (Classops.cte_typ * Classops.cte_typ) * Term.constr * Term.constr list *
+ (global_reference * global_reference) * Term.constr * Term.constr list *
Term.constr list * Term.constr list -> unit
@@ -45,4 +45,4 @@ val outStruc : obj -> inductive_path * struc_typ
val inObjDef1 : section_path -> obj
val outObjDef1 : obj -> section_path
-val add_new_objdef1 : ((cte_typ * cte_typ) * obj_typ) -> unit
+val add_new_objdef1 : ((global_reference * global_reference) * obj_typ) -> unit
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 40ecc11c3..022c75cb6 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -57,9 +57,10 @@ let rec stre_unif_cond = function
stre_max (stre1,stre2)
let stre_of_coe = function
- | NAM_Constant sp -> constant_or_parameter_strength sp
- | NAM_Section_Variable sp -> variable_strength sp
- | NAM_Inductive _ | NAM_Constructor _ -> NeverDischarge
+ | ConstRef sp -> constant_or_parameter_strength sp
+ | VarRef sp -> variable_strength sp
+ | IndRef _ | ConstructRef _ -> NeverDischarge
+ | EvarRef _ -> anomaly "Not a persistent reference"
(* verfications pour l'ajout d'une classe *)
@@ -81,12 +82,12 @@ let try_add_class v (cl,p) streopt check_exist =
if check_exist & class_exists cl then
errorlabstrm "try_add_new_class"
[< 'sTR (string_of_class cl) ; 'sTR " is already a class" >];
- let stre' = stre_of_cl cl in
+ let stre' = strength_of_cl cl in
let stre = match streopt with
| Some stre -> stre_max (stre,stre')
| None -> stre'
in
- add_new_class (cl,stre,p);
+ declare_class (cl,stre,p);
stre
(* try_add_new_class : Names.identifier -> unit *)
@@ -112,8 +113,8 @@ let try_add_new_class ref stre =
let check_class v cl p =
try
let _,clinfo = class_info cl in
- check_fully_applied cl p clinfo.cL_PARAM;
- clinfo.cL_STRE
+ check_fully_applied cl p clinfo.cl_param;
+ clinfo.cl_strength
with Not_found ->
let env = Global.env () in
let t = Retyping.get_type_of env Evd.empty v in
@@ -143,14 +144,14 @@ let check_target clt = function
(* t provient de global_reference donc pas de Cast, pas de App *)
let coe_of_reference t =
match kind_of_term t with
- | IsConst (sp,l) -> (Array.to_list l),NAM_Constant sp
- | IsMutInd (ind_sp,l) -> (Array.to_list l),NAM_Inductive ind_sp
- | IsMutConstruct (cstr_sp,l) -> (Array.to_list l),NAM_Constructor cstr_sp
+ | IsConst (sp,l) -> (Array.to_list l), ConstRef sp
+ | IsMutInd (ind_sp,l) -> (Array.to_list l), IndRef ind_sp
+ | IsMutConstruct (cstr_sp,l) -> (Array.to_list l), ConstructRef cstr_sp
| IsVar id ->
let sp =
try find_section_variable id
with Not_found -> anomaly "Not a reference"
- in [],NAM_Section_Variable sp
+ in [], VarRef sp
| _ -> anomaly "Not a reference"
let constructor_at_head1 t =
@@ -299,13 +300,6 @@ let build_id_coercion idf_opt source =
let sp = declare_constant idf (constr_entry,NeverDischarge,false) in
ConstRef sp
-let add_new_coercion_in_graph1 (coef,v,stre,isid,cls,clt) ps =
- add_anonymous_leaf
- (inCoercion
- ((coef,
- {cOE_VALUE=v;cOE_STRE=stre;cOE_ISID=isid;cOE_PARAM=ps}),
- cls,clt))
-
(*
nom de la fonction coercion
strength de f
@@ -369,7 +363,7 @@ let try_add_new_coercion_core idf stre source target isid =
'sTR" must be declared as a local coercion (its strength is ";
'sTR(string_of_strength stre');'sTR")" >] *)
let stre = stre_max (stre,stre') in
- add_new_coercion_in_graph1 (coef,vj,stre,isid,cls,clt) ps
+ declare_coercion coef vj stre isid cls clt ps
let try_add_new_coercion ref stre =
@@ -404,7 +398,7 @@ let count_extra_abstractions hyps ids_to_discard =
let defined_in_sec sp sec_sp = dirpath sp = sec_sp
let process_class sec_sp ids_to_discard x =
- let (cl,{cL_STRE=stre; cL_PARAM=p}) = x in
+ let (cl,{cl_strength=stre; cl_param=p}) = x in
(* let env = Global.env () in*)
match cl with
| CL_SECVAR _ -> x
@@ -419,7 +413,7 @@ let process_class sec_sp ids_to_discard x =
let t = Retyping.get_type_of env Evd.empty v in
let p = arity_sort t in
*)
- (CL_CONST newsp,{cL_STRE=stre;cL_PARAM=p+n})
+ (CL_CONST newsp,{cl_strength=stre;cl_param=p+n})
else
x
| CL_IND (sp,i) ->
@@ -433,7 +427,7 @@ let process_class sec_sp ids_to_discard x =
let t = Retyping.get_type_of env Evd.empty v in
let p = arity_sort t in
*)
- (CL_IND (newsp,i),{cL_STRE=stre;cL_PARAM=p+n})
+ (CL_IND (newsp,i),{cl_strength=stre;cl_param=p+n})
else
x
| _ -> anomaly "process_class"
@@ -463,25 +457,26 @@ let process_coercion sec_sp (((coe,coeinfo),s,t) as x) =
let s1= process_cl sec_sp s in
let t1 = process_cl sec_sp t in
match coe with
- | NAM_Section_Variable _ -> ((coe,coeinfo),s1,t1)
- | NAM_Constant sp ->
+ | VarRef _ -> ((coe,coeinfo),s1,t1)
+ | ConstRef sp ->
if defined_in_sec sp sec_sp then
let ((_,spid,spk)) = repr_path sp in
let newsp = Lib.make_path spid CCI in
- ((NAM_Constant newsp,coeinfo),s1,t1)
+ ((ConstRef newsp,coeinfo),s1,t1)
else
((coe,coeinfo),s1,t1)
- | NAM_Inductive (sp,i) ->
+ | IndRef (sp,i) ->
if defined_in_sec sp sec_sp then
let ((_,spid,spk)) = repr_path sp in
let newsp = Lib.make_path spid CCI in
- ((NAM_Inductive (newsp,i),coeinfo),s1,t1)
+ ((IndRef (newsp,i),coeinfo),s1,t1)
else
((coe,coeinfo),s1,t1)
- | NAM_Constructor ((sp,i),j) ->
+ | ConstructRef ((sp,i),j) ->
if defined_in_sec sp sec_sp then
let ((_,spid,spk)) = repr_path sp in
let newsp = Lib.make_path spid CCI in
- (((NAM_Constructor ((newsp,i),j)),coeinfo),s1,t1)
+ (((ConstructRef ((newsp,i),j)),coeinfo),s1,t1)
else
((coe,coeinfo),s1,t1)
+ | EvarRef _ -> anomaly "No Evar expected here as coercion"
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 8b8279a6a..a3c9586a4 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -216,7 +216,7 @@ let process_object oldenv dir sec_sp
| "CLASS" ->
let ((cl,clinfo) as x) = outClass lobj in
- if clinfo.cL_STRE = (DischargeAt sec_sp) then
+ if clinfo.cl_strength = (DischargeAt sec_sp) then
(ops,ids_to_discard,work_alist)
else
let (y1,y2) = process_class sec_sp ids_to_discard x in
@@ -224,7 +224,7 @@ let process_object oldenv dir sec_sp
| "COERCION" ->
let (((_,coeinfo),_,_)as x) = outCoercion lobj in
- if coeinfo.cOE_STRE = (DischargeAt sec_sp) then
+ if coercion_strength coeinfo = (DischargeAt sec_sp) then
(ops,ids_to_discard,work_alist)
else
let y = process_coercion sec_sp x in
@@ -298,8 +298,8 @@ let push_inductive_names ccitab sp mie =
(*s Operations performed at section closing. *)
let cache_end_section (_,(sp,mc)) =
- Nametab.push_module sp mc;
- Nametab.open_module_contents (qualid_of_sp sp)
+ Nametab.push_section sp mc;
+ Nametab.open_section_contents (qualid_of_sp sp)
let load_end_section (_,(sp,mc)) =
Nametab.push_module sp mc
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 05:47:54 +0000