aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/extraction/common.ml8
-rw-r--r--contrib/extraction/extract_env.ml37
-rw-r--r--contrib/extraction/extraction.ml12
-rw-r--r--contrib/extraction/extraction.mli6
-rw-r--r--contrib/extraction/mlutil.ml11
-rw-r--r--contrib/extraction/mlutil.mli2
-rw-r--r--contrib/extraction/modutil.ml36
-rw-r--r--contrib/extraction/table.ml50
-rw-r--r--contrib/extraction/table.mli15
-rw-r--r--contrib/first-order/ground.ml6
-rw-r--r--contrib/fourier/fourierR.ml2
-rw-r--r--contrib/funind/tacinvutils.ml2
-rw-r--r--contrib/interface/centaur.ml42
-rw-r--r--contrib/interface/name_to_ast.ml6
-rw-r--r--contrib/ring/ring.ml2
-rw-r--r--contrib/xml/cic2acic.ml55
-rw-r--r--contrib/xml/doubleTypeInference.ml2
-rw-r--r--contrib/xml/doubleTypeInference.mli2
-rw-r--r--contrib/xml/xmlcommand.ml30
19 files changed, 163 insertions, 123 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 0af215f252..359257c886 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -143,7 +143,7 @@ let create_modular_renamings struc =
in
(* 1) creates renamings of objects *)
let add upper r =
- let mp = modpath (kn_of_r r) in
+ let mp = modpath_of_r r in
let l = mp_create_modular_renamings mp in
let s = modular_rename upper (id_of_global r) in
global_ids := Idset.add (id_of_string s) !global_ids;
@@ -184,7 +184,7 @@ let create_modular_renamings struc =
List.iter contents_first_level used_modules;
let used_modules' = List.rev used_modules in
let needs_qualify r =
- let mp = modpath (kn_of_r r) in
+ let mp = modpath_of_r r in
if (is_modfile mp) && mp <> current_module &&
(clash mp [] (List.hd (get_renamings r)) used_modules')
then to_qualify := Refset.add r !to_qualify
@@ -239,7 +239,7 @@ let rec mp_create_mono_renamings mp =
let create_mono_renamings struc =
let { up = u ; down = d } = struct_get_references_list struc in
let add upper r =
- let mp = modpath (kn_of_r r) in
+ let mp = modpath_of_r r in
let l = mp_create_mono_renamings mp in
let mycase = if upper then uppercase_id else lowercase_id in
let id =
@@ -278,7 +278,7 @@ module StdParams = struct
let pp_global mpl r =
let ls = get_renamings r in
let s = List.hd ls in
- let mp = modpath (kn_of_r r) in
+ let mp = modpath_of_r r in
let ls =
if mp = List.hd mpl then [s] (* simpliest situation *)
else
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index f9be3d9b03..78fb578e99 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -28,7 +28,7 @@ let toplevel_env () =
| (_,kn), Lib.Leaf o ->
let mp,_,l = repr_kn kn in
let seb = match Libobject.object_tag o with
- | "CONSTANT" -> SEBconst (Global.lookup_constant kn)
+ | "CONSTANT" -> SEBconst (Global.lookup_constant (constant_of_kn kn))
| "INDUCTIVE" -> SEBmind (Global.lookup_mind kn)
| "MODULE" -> SEBmodule (Global.lookup_module (MPdot (mp,l)))
| "MODULE TYPE" -> SEBmodtype (Global.lookup_modtype kn)
@@ -52,14 +52,16 @@ let environment_until dir_opt =
| _ -> assert false
in parse (Library.loaded_libraries ())
-type visit = { mutable kn : KNset.t; mutable mp : MPset.t }
+type visit =
+ { mutable kn : KNset.t; mutable ref : Refset.t; mutable mp : MPset.t }
let in_kn v kn = KNset.mem kn v.kn
+let in_ref v ref = Refset.mem ref v.ref
let in_mp v mp = MPset.mem mp v.mp
let visit_mp v mp = v.mp <- MPset.union (prefixes_mp mp) v.mp
let visit_kn v kn = v.kn <- KNset.add kn v.kn; visit_mp v (modpath kn)
-let visit_ref v r = visit_kn v (kn_of_r r)
+let visit_ref v r = v.ref <- Refset.add r v.ref; visit_mp v (modpath_of_r r)
exception Impossible
@@ -102,7 +104,7 @@ let get_spec_references v s =
let rec extract_msig env v mp = function
| [] -> []
| (l,SPBconst cb) :: msig ->
- let kn = make_kn mp empty_dirpath l in
+ let kn = make_con mp empty_dirpath l in
let s = extract_constant_spec env kn cb in
if logical_spec s then extract_msig env v mp msig
else begin
@@ -143,9 +145,9 @@ let rec extract_msb env v mp all = function
| (l,SEBconst cb) :: msb ->
(try
let vl,recd,msb = factor_fix env l cb msb in
- let vkn = Array.map (fun id -> make_kn mp empty_dirpath id) vl in
+ let vkn = Array.map (fun id -> make_con mp empty_dirpath id) vl in
let ms = extract_msb env v mp all msb in
- let b = array_exists (in_kn v) vkn in
+ let b = array_exists (fun con -> in_ref v (ConstRef con)) vkn in
if all || b then
let d = extract_fixpoint env vkn recd in
if (not b) && (logical_decl d) then ms
@@ -153,8 +155,8 @@ let rec extract_msb env v mp all = function
else ms
with Impossible ->
let ms = extract_msb env v mp all msb in
- let kn = make_kn mp empty_dirpath l in
- let b = in_kn v kn in
+ let kn = make_con mp empty_dirpath l in
+ let b = in_ref v (ConstRef kn) in
if all || b then
let d = extract_constant env kn cb in
if (not b) && (logical_decl d) then ms
@@ -163,7 +165,7 @@ let rec extract_msb env v mp all = function
| (l,SEBmind mib) :: msb ->
let ms = extract_msb env v mp all msb in
let kn = make_kn mp empty_dirpath l in
- let b = in_kn v kn in
+ let b = in_ref v (IndRef (kn,0)) in (* 0 is dummy *)
if all || b then
let d = Dind (kn, extract_inductive env kn) in
if (not b) && (logical_decl d) then ms
@@ -217,12 +219,12 @@ let unpack = function MEstruct (_,sel) -> sel | _ -> assert false
let mono_environment refs mpl =
let l = environment_until None in
let v =
- let add_kn r = KNset.add (kn_of_r r) in
- let kns = List.fold_right add_kn refs KNset.empty in
+ let add_ref r = Refset.add r in
+ let refs = List.fold_right add_ref refs Refset.empty in
let add_mp mp = MPset.union (prefixes_mp mp) in
let mps = List.fold_right add_mp mpl MPset.empty in
- let mps = KNset.fold (fun k -> add_mp (modpath k)) kns mps in
- { kn = kns; mp = mps }
+ let mps = Refset.fold (fun k -> add_mp (modpath_of_r k)) refs mps in
+ { kn = KNset.empty; ref = refs; mp = mps }
in
let env = Global.env () in
List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env v (Some mp) false m))
@@ -270,10 +272,9 @@ let extraction qid =
else begin
let prm =
{ modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in
- let kn = kn_of_r r in
let struc = optimize_struct prm None (mono_environment [r] []) in
let d = get_decl_in_structure r struc in
- print_one_decl struc (modpath kn) d;
+ print_one_decl struc (modpath_of_r r) d;
reset_tables ()
end
@@ -315,7 +316,7 @@ let extraction_module m =
let b = is_modfile mp in
let prm = {modular=b; mod_name = id_of_string ""; to_appear= []} in
let l = environment_until None in
- let v = { kn = KNset.empty ; mp = prefixes_mp mp } in
+ let v={ kn = KNset.empty ; ref = Refset.empty; mp = prefixes_mp mp } in
let env = Global.env () in
let struc =
List.rev_map
@@ -350,7 +351,9 @@ let extraction_library is_rec m =
| Scheme -> error_scheme ()
| _ ->
let dir_m = dir_module_of_id m in
- let v = { kn = KNset.empty; mp = MPset.singleton (MPfile dir_m) } in
+ let v =
+ { kn = KNset.empty; ref = Refset.empty;
+ mp = MPset.singleton (MPfile dir_m) } in
let l = environment_until (Some dir_m) in
let struc =
let env = Global.env () in
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 0bf5d6bcde..52ff05439e 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -358,16 +358,16 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
let field_names =
list_skipn mip0.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
assert (List.length field_names = List.length typ);
- let projs = ref KNset.empty in
+ let projs = ref Cset.empty in
let mp,d,_ = repr_kn kn in
let rec select_fields l typs = match l,typs with
| [],[] -> []
| (Name id)::l, typ::typs ->
if type_eq (mlt_env env) Tdummy typ then select_fields l typs
else
- let knp = make_kn mp d (label_of_id id) in
+ let knp = make_con mp d (label_of_id id) in
if not (List.mem false (type_to_sign (mlt_env env) typ)) then
- projs := KNset.add knp !projs;
+ projs := Cset.add knp !projs;
(ConstRef knp) :: (select_fields l typs)
| Anonymous::l, typ::typs ->
if type_eq (mlt_env env) Tdummy typ then select_fields l typs
@@ -382,7 +382,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
let n = nb_default_params env mip0.mind_nf_arity in
List.iter
(option_iter
- (fun kn -> if KNset.mem kn !projs then add_projection n kn))
+ (fun kn -> if Cset.mem kn !projs then add_projection n kn))
(find_structure ip).s_PROJ
with Not_found -> ()
end;
@@ -417,7 +417,7 @@ and extract_type_cons env db dbmap c i =
and mlt_env env r = match r with
| ConstRef kn ->
(try
- if not (visible_kn kn) then raise Not_found;
+ if not (visible_con kn) then raise Not_found;
match lookup_term kn with
| Dtype (_,vl,mlt) -> Some mlt
| _ -> None
@@ -446,7 +446,7 @@ let type_expunge env = type_expunge (mlt_env env)
let record_constant_type env kn opt_typ =
try
- if not (visible_kn kn) then raise Not_found;
+ if not (visible_con kn) then raise Not_found;
lookup_type kn
with Not_found ->
let typ = match opt_typ with
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 31fdd0580c..b26a577e2d 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -17,12 +17,12 @@ open Environ
open Libnames
open Miniml
-val extract_constant : env -> kernel_name -> constant_body -> ml_decl
+val extract_constant : env -> constant -> constant_body -> ml_decl
-val extract_constant_spec : env -> kernel_name -> constant_body -> ml_spec
+val extract_constant_spec : env -> constant -> constant_body -> ml_spec
val extract_fixpoint :
- env -> kernel_name array -> (constr, types) prec_declaration -> ml_decl
+ env -> constant array -> (constr, types) prec_declaration -> ml_decl
val extract_inductive : env -> kernel_name -> ml_ind
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 3d4ab11a67..b8764d85d0 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -210,7 +210,7 @@ end
let rec type_mem_kn kn = function
| Tmeta _ -> assert false
- | Tglob (r,l) -> (kn_of_r r) = kn || List.exists (type_mem_kn kn) l
+ | Tglob (r,l) -> occur_kn_in_ref kn r || List.exists (type_mem_kn kn) l
| Tarr (a,b) -> (type_mem_kn kn a) || (type_mem_kn kn b)
| _ -> false
@@ -594,11 +594,12 @@ let rec linear_beta_red a t = match a,t with
linear beta reductions at modified positions. *)
let rec ast_glob_subst s t = match t with
- | MLapp ((MLglob (ConstRef kn)) as f, a) ->
+ | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) ->
let a = List.map (ast_glob_subst s) a in
- (try linear_beta_red a (KNmap.find kn s)
+ (try linear_beta_red a (Refmap.find refe s)
with Not_found -> MLapp (f, a))
- | MLglob (ConstRef kn) -> (try KNmap.find kn s with Not_found -> t)
+ | MLglob ((ConstRef kn) as refe) ->
+ (try Refmap.find refe s with Not_found -> t)
| _ -> ast_map (ast_glob_subst s) t
@@ -1117,7 +1118,7 @@ let inline_test t =
let manual_inline_list =
let mp = MPfile (dirpath_of_string "Coq.Init.Wf") in
- List.map (fun s -> (make_kn mp empty_dirpath (mk_label s)))
+ List.map (fun s -> (make_con mp empty_dirpath (mk_label s)))
[ "well_founded_induction_type"; "well_founded_induction";
"Acc_rect"; "Acc_rec" ; "Acc_iter" ]
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index bc4de489d3..05e773c5d8 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -101,7 +101,7 @@ val ast_lift : int -> ml_ast -> ml_ast
val ast_pop : ml_ast -> ml_ast
val ast_subst : ml_ast -> ml_ast -> ml_ast
-val ast_glob_subst : ml_ast KNmap.t -> ml_ast -> ml_ast
+val ast_glob_subst : ml_ast Refmap.t -> ml_ast -> ml_ast
val normalize : ml_ast -> ml_ast
val optimize_fix : ml_ast -> ml_ast
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index caa72b34f4..1a40a83307 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -25,8 +25,9 @@ open Mlutil
let add_structure mp msb env =
let add_one env (l,elem) =
let kn = make_kn mp empty_dirpath l in
+ let con = make_con mp empty_dirpath l in
match elem with
- | SEBconst cb -> Environ.add_constant kn cb env
+ | SEBconst cb -> Environ.add_constant con cb env
| SEBmind mib -> Environ.add_mind kn mib env
| SEBmodule mb -> Modops.add_module (MPdot (mp,l)) mb env
| SEBmodtype mtb -> Environ.add_modtype kn mtb env
@@ -116,8 +117,15 @@ let rec parse_labels ll = function
let labels_of_mp mp = parse_labels [] mp
-let labels_of_kn kn =
- let mp,_,l = repr_kn kn in parse_labels [l] mp
+let labels_of_ref r =
+ let mp,_,l =
+ match r with
+ ConstRef con -> repr_con con
+ | IndRef (kn,_)
+ | ConstructRef ((kn,_),_) -> repr_kn kn
+ | VarRef _ -> assert false
+ in
+ parse_labels [l] mp
let rec add_labels_mp mp = function
| [] -> mp
@@ -307,8 +315,7 @@ let signature_of_structure s =
let get_decl_in_structure r struc =
try
- let kn = kn_of_r r in
- let base_mp,ll = labels_of_kn kn in
+ let base_mp,ll = labels_of_ref r in
if not (at_toplevel base_mp) then error_not_visible r;
let sel = List.assoc base_mp struc in
let rec go ll sel = match ll with
@@ -336,16 +343,16 @@ let get_decl_in_structure r struc =
let dfix_to_mlfix rv av i =
let rec make_subst n s =
if n < 0 then s
- else make_subst (n-1) (KNmap.add (kn_of_r rv.(n)) (n+1) s)
+ else make_subst (n-1) (Refmap.add rv.(n) (n+1) s)
in
- let s = make_subst (Array.length rv - 1) KNmap.empty
+ let s = make_subst (Array.length rv - 1) Refmap.empty
in
let rec subst n t = match t with
- | MLglob (ConstRef kn) ->
- (try MLrel (n + (KNmap.find kn s)) with Not_found -> t)
+ | MLglob ((ConstRef kn) as refe) ->
+ (try MLrel (n + (Refmap.find refe s)) with Not_found -> t)
| _ -> ast_map_lift subst n t
in
- let ids = Array.map (fun r -> id_of_label (label (kn_of_r r))) rv in
+ let ids = Array.map (fun r -> id_of_label (label_of_r r)) rv in
let c = Array.map (subst 0) av
in MLfix(i, ids, c)
@@ -356,7 +363,7 @@ let rec optim prm s = function
| Dterm (r,t,typ) :: l ->
let t = normalize (ast_glob_subst !s t) in
let i = inline r t in
- if i then s := KNmap.add (kn_of_r r) t !s;
+ if i then s := Refmap.add r t !s;
if not i || prm.modular || List.mem r prm.to_appear
then
let d = match optimize_fix t with
@@ -370,10 +377,9 @@ let rec optim prm s = function
let rec optim_se top prm s = function
| [] -> []
| (l,SEdecl (Dterm (r,a,t))) :: lse ->
- let kn = kn_of_r r in
let a = normalize (ast_glob_subst !s a) in
let i = inline r a in
- if i then s := KNmap.add kn a !s;
+ if i then s := Refmap.add r a !s;
if top && i && not prm.modular && not (List.mem r prm.to_appear)
then optim_se top prm s lse
else
@@ -389,7 +395,7 @@ let rec optim_se top prm s = function
let fake_body = MLfix (0,[||],[||]) in
for i = 0 to Array.length rv - 1 do
if inline rv.(i) fake_body
- then s := KNmap.add (kn_of_r rv.(i)) (dfix_to_mlfix rv av i) !s
+ then s := Refmap.add rv.(i) (dfix_to_mlfix rv av i) !s
else all := false
done;
if !all && top && not prm.modular
@@ -408,6 +414,6 @@ and optim_me prm s = function
| MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me prm s me)
let optimize_struct prm before struc =
- let subst = ref (KNmap.empty : ml_ast KNmap.t) in
+ let subst = ref (Refmap.empty : ml_ast Refmap.t) in
option_iter (fun l -> ignore (optim prm subst l)) before;
List.map (fun (mp,lse) -> (mp, optim_se true prm subst lse)) struc
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 17628698da..7c010ab4f0 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -22,10 +22,23 @@ open Miniml
(*S Utilities concerning [module_path] and [kernel_names] *)
-let kn_of_r r = match r with
- | ConstRef kn -> kn
- | IndRef (kn,_) -> kn
- | ConstructRef ((kn,_),_) -> kn
+let occur_kn_in_ref kn =
+ function
+ | IndRef (kn',_)
+ | ConstructRef ((kn',_),_) -> kn = kn'
+ | ConstRef _ -> false
+ | VarRef _ -> assert false
+
+let modpath_of_r r = match r with
+ | ConstRef kn -> con_modpath kn
+ | IndRef (kn,_)
+ | ConstructRef ((kn,_),_) -> modpath kn
+ | VarRef _ -> assert false
+
+let label_of_r r = match r with
+ | ConstRef kn -> con_label kn
+ | IndRef (kn,_)
+ | ConstructRef ((kn,_),_) -> label kn
| VarRef _ -> assert false
let current_toplevel () = fst (Lib.current_prefix ())
@@ -45,21 +58,22 @@ let at_toplevel mp =
is_modfile mp || is_toplevel mp
let visible_kn kn = at_toplevel (base_mp (modpath kn))
+let visible_con kn = at_toplevel (base_mp (con_modpath kn))
(*S The main tables: constants, inductives, records, ... *)
(*s Constants tables. *)
-let terms = ref (KNmap.empty : ml_decl KNmap.t)
-let init_terms () = terms := KNmap.empty
-let add_term kn d = terms := KNmap.add kn d !terms
-let lookup_term kn = KNmap.find kn !terms
+let terms = ref (Cmap.empty : ml_decl Cmap.t)
+let init_terms () = terms := Cmap.empty
+let add_term kn d = terms := Cmap.add kn d !terms
+let lookup_term kn = Cmap.find kn !terms
-let types = ref (KNmap.empty : ml_schema KNmap.t)
-let init_types () = types := KNmap.empty
-let add_type kn s = types := KNmap.add kn s !types
-let lookup_type kn = KNmap.find kn !types
+let types = ref (Cmap.empty : ml_schema Cmap.t)
+let init_types () = types := Cmap.empty
+let add_type kn s = types := Cmap.add kn s !types
+let lookup_type kn = Cmap.find kn !types
(*s Inductives table. *)
@@ -70,22 +84,22 @@ let lookup_ind kn = KNmap.find kn !inductives
(*s Recursors table. *)
-let recursors = ref KNset.empty
-let init_recursors () = recursors := KNset.empty
+let recursors = ref Cset.empty
+let init_recursors () = recursors := Cset.empty
let add_recursors env kn =
- let make_kn id = make_kn (modpath kn) empty_dirpath (label_of_id id) in
+ let make_kn id = make_con (modpath kn) empty_dirpath (label_of_id id) in
let mib = Environ.lookup_mind kn env in
Array.iter
(fun mip ->
let id = mip.mind_typename in
let kn_rec = make_kn (Nameops.add_suffix id "_rec")
and kn_rect = make_kn (Nameops.add_suffix id "_rect") in
- recursors := KNset.add kn_rec (KNset.add kn_rect !recursors))
+ recursors := Cset.add kn_rec (Cset.add kn_rect !recursors))
mib.mind_packets
let is_recursor = function
- | ConstRef kn -> KNset.mem kn !recursors
+ | ConstRef kn -> Cset.mem kn !recursors
| _ -> false
(*s Record tables. *)
@@ -109,7 +123,7 @@ let reset_tables () =
done before. *)
let id_of_global = function
- | ConstRef kn -> let _,_,l = repr_kn kn in id_of_label l
+ | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
| IndRef (kn,i) -> (lookup_ind kn).ind_packets.(i).ip_typename
| ConstructRef ((kn,i),j) -> (lookup_ind kn).ind_packets.(i).ip_consnames.(j-1)
| _ -> assert false
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index d2fcf67d7e..0b69a74120 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -35,7 +35,9 @@ val check_inside_section : unit -> unit
(*s utilities concerning [module_path]. *)
-val kn_of_r : global_reference -> kernel_name
+val occur_kn_in_ref : kernel_name -> global_reference -> bool
+val modpath_of_r : global_reference -> module_path
+val label_of_r : global_reference -> label
val current_toplevel : unit -> module_path
val base_mp : module_path -> module_path
@@ -43,14 +45,15 @@ val is_modfile : module_path -> bool
val is_toplevel : module_path -> bool
val at_toplevel : module_path -> bool
val visible_kn : kernel_name -> bool
+val visible_con : constant -> bool
(*s Some table-related operations *)
-val add_term : kernel_name -> ml_decl -> unit
-val lookup_term : kernel_name -> ml_decl
+val add_term : constant -> ml_decl -> unit
+val lookup_term : constant -> ml_decl
-val add_type : kernel_name -> ml_schema -> unit
-val lookup_type : kernel_name -> ml_schema
+val add_type : constant -> ml_schema -> unit
+val lookup_type : constant -> ml_schema
val add_ind : kernel_name -> ml_ind -> unit
val lookup_ind : kernel_name -> ml_ind
@@ -58,7 +61,7 @@ val lookup_ind : kernel_name -> ml_ind
val add_recursors : Environ.env -> kernel_name -> unit
val is_recursor : global_reference -> bool
-val add_projection : int -> kernel_name -> unit
+val add_projection : int -> constant -> unit
val is_projection : global_reference -> bool
val projection_arity : global_reference -> int
diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml
index 418e6ce831..00a2260c6f 100644
--- a/contrib/first-order/ground.ml
+++ b/contrib/first-order/ground.ml
@@ -45,17 +45,17 @@ let update_flags ()=
*)
let update_flags ()=
- let predref=ref Names.KNpred.empty in
+ let predref=ref Names.Cpred.empty in
let f coe=
try
let kn=destConst (Classops.get_coercion_value coe) in
- predref:=Names.KNpred.add kn !predref
+ predref:=Names.Cpred.add kn !predref
with Invalid_argument "destConst"-> () in
List.iter f (Classops.coercions ());
red_flags:=
Closure.RedFlags.red_add_transparent
Closure.betaiotazeta
- (Names.Idpred.full,Names.KNpred.complement !predref)
+ (Names.Idpred.full,Names.Cpred.complement !predref)
let ground_tac solver startseq gl=
update_flags ();
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index de7d0b1339..33d6faad17 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -76,7 +76,7 @@ open Vernacexpr
type ineq = Rlt | Rle | Rgt | Rge
let string_of_R_constant kn =
- match Names.repr_kn kn with
+ match Names.repr_con kn with
| MPfile dir, sec_dir, id when
sec_dir = empty_dirpath &&
string_of_dirpath dir = "Coq.Reals.Rdefinitions"
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index 758071bac2..5797ec639b 100644
--- a/contrib/funind/tacinvutils.ml
+++ b/contrib/funind/tacinvutils.ml
@@ -263,7 +263,7 @@ let def_of_const t =
(* nom d'une constante. Must be a constante. x*)
let name_of_const t =
match (kind_of_term t) with
- Const cst -> Names.string_of_label (Names.label cst)
+ Const cst -> Names.string_of_label (Names.con_label cst)
|_ -> assert false
;;
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 3cc5390639..ef3561a708 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -413,7 +413,7 @@ let inspect n =
let (_, _, v) = get_variable (basename sp) in
add_search2 (Nametab.locate (qualid_of_sp sp)) v
| (sp,kn), "CONSTANT" ->
- let {const_type=typ} = Global.lookup_constant kn in
+ let {const_type=typ} = Global.lookup_constant (constant_of_kn kn) in
add_search2 (Nametab.locate (qualid_of_sp sp)) typ
| (sp,kn), "MUTUALINDUCTIVE" ->
add_search2 (Nametab.locate (qualid_of_sp sp))
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index a08f2cd6fc..0add95076a 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -173,9 +173,9 @@ let constant_to_ast_list kn =
let l = implicits_of_global (ConstRef kn) in
(match c with
None ->
- make_variable_ast (id_of_label (label kn)) typ l
+ make_variable_ast (id_of_label (con_label kn)) typ l
| Some c1 ->
- make_definition_ast (id_of_label (label kn)) (Declarations.force c1) typ l)
+ make_definition_ast (id_of_label (con_label kn)) (Declarations.force c1) typ l)
let variable_to_ast_list sp =
let (id, c, v) = get_variable sp in
@@ -198,7 +198,7 @@ let leaf_entry_to_ast_list ((sp,kn),lobj) =
let tag = object_tag lobj in
match tag with
| "VARIABLE" -> variable_to_ast_list (basename sp)
- | "CONSTANT" -> constant_to_ast_list kn
+ | "CONSTANT" -> constant_to_ast_list (constant_of_kn kn)
| "INDUCTIVE" -> inductive_to_ast_list kn
| s ->
errorlabstrm
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 2f42af6b71..bf45397983 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -724,7 +724,7 @@ let constants_to_unfold =
let transform s =
let sp = path_of_string s in
let dir, id = repr_path sp in
- Libnames.encode_kn dir id
+ Libnames.encode_con dir id
in
List.map transform
[ "Coq.ring.Ring_normalize.interp_cs";
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index d379c55694..dca5963f9a 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -83,16 +83,28 @@ let get_uri_of_var v pvars =
;;
type tag =
- Constant
- | Inductive
- | Variable
+ Constant of Names.constant
+ | Inductive of Names.kernel_name
+ | Variable of Names.kernel_name
;;
+type etag =
+ TConstant
+ | TInductive
+ | TVariable
+;;
+
+let etag_of_tag =
+ function
+ Constant _ -> TConstant
+ | Inductive _ -> TInductive
+ | Variable _ -> TVariable
+
let ext_of_tag =
function
- Constant -> "con"
- | Inductive -> "ind"
- | Variable -> "var"
+ TConstant -> "con"
+ | TInductive -> "ind"
+ | TVariable -> "var"
;;
exception FunctorsXMLExportationNotImplementedYet;;
@@ -147,23 +159,24 @@ let token_list_of_path dir id tag =
List.rev_map N.string_of_id (N.repr_dirpath dirpath) in
token_list_of_dirpath dir @ [N.string_of_id id ^ "." ^ (ext_of_tag tag)]
-let token_list_of_kernel_name kn tag =
+let token_list_of_kernel_name tag =
let module N = Names in
let module LN = Libnames in
- let dir = match tag with
- | Variable ->
- Lib.cwd ()
- | Constant ->
- Lib.library_part (LN.ConstRef kn)
- | Inductive ->
+ let id,dir = match tag with
+ | Variable kn ->
+ N.id_of_label (N.label kn), Lib.cwd ()
+ | Constant con ->
+ N.id_of_label (N.con_label con),
+ Lib.library_part (LN.ConstRef con)
+ | Inductive kn ->
+ N.id_of_label (N.label kn),
Lib.library_part (LN.IndRef (kn,0))
in
- let id = N.id_of_label (N.label kn) in
- token_list_of_path dir id tag
+ token_list_of_path dir id (etag_of_tag tag)
;;
-let uri_of_kernel_name kn tag =
- let tokens = token_list_of_kernel_name kn tag in
+let uri_of_kernel_name tag =
+ let tokens = token_list_of_kernel_name tag in
"cic:/" ^ String.concat "/" tokens
let uri_of_declaration id tag =
@@ -709,7 +722,7 @@ print_endline "PASSATO" ; flush stdout ;
if is_a_Prop innersort && expected_available then
add_inner_type fresh_id'' ;
let compute_result_if_eta_expansion_not_required _ _ =
- A.AConst (fresh_id'', subst, (uri_of_kernel_name kn Constant))
+ A.AConst (fresh_id'', subst, (uri_of_kernel_name (Constant kn)))
in
let (_,subst') = subst in
explicit_substitute_and_eta_expand_if_required tt []
@@ -717,7 +730,7 @@ print_endline "PASSATO" ; flush stdout ;
compute_result_if_eta_expansion_not_required
| T.Ind (kn,i) ->
let compute_result_if_eta_expansion_not_required _ _ =
- A.AInd (fresh_id'', subst, (uri_of_kernel_name kn Inductive), i)
+ A.AInd (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i)
in
let (_,subst') = subst in
explicit_substitute_and_eta_expand_if_required tt []
@@ -729,7 +742,7 @@ print_endline "PASSATO" ; flush stdout ;
add_inner_type fresh_id'' ;
let compute_result_if_eta_expansion_not_required _ _ =
A.AConstruct
- (fresh_id'', subst, (uri_of_kernel_name kn Inductive), i, j)
+ (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i, j)
in
let (_,subst') = subst in
explicit_substitute_and_eta_expand_if_required tt []
@@ -743,7 +756,7 @@ print_endline "PASSATO" ; flush stdout ;
Array.fold_right (fun x i -> (aux' env idrefs x)::i) a []
in
A.ACase
- (fresh_id'', (uri_of_kernel_name kn Inductive), i,
+ (fresh_id'', (uri_of_kernel_name (Inductive kn)), i,
aux' env idrefs ty, aux' env idrefs term, a')
| T.Fix ((ai,i),(f,t,b)) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index 46165871ac..cf975b4372 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -19,7 +19,7 @@ let prerr_endline _ = ();;
let cprop =
let module N = Names in
- N.make_kn
+ N.make_con
(N.MPfile
(Libnames.dirpath_of_string "CoRN.algebra.CLogic"))
(N.make_dirpath [])
diff --git a/contrib/xml/doubleTypeInference.mli b/contrib/xml/doubleTypeInference.mli
index 33d3e5cd03..2e14b5580b 100644
--- a/contrib/xml/doubleTypeInference.mli
+++ b/contrib/xml/doubleTypeInference.mli
@@ -14,7 +14,7 @@
type types = { synthesized : Term.types; expected : Term.types option; }
-val cprop : Names.kernel_name
+val cprop : Names.constant
val whd_betadeltaiotacprop :
Environ.env -> Evd.evar_map -> Term.constr -> Term.constr
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index ba9e87e0ba..b9d8ac42b1 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -177,12 +177,12 @@ let rec join_dirs cwd =
join_dirs newcwd tail
;;
-let filename_of_path xml_library_root kn tag =
+let filename_of_path xml_library_root tag =
let module N = Names in
match xml_library_root with
None -> None (* stdout *)
| Some xml_library_root' ->
- let tokens = Cic2acic.token_list_of_kernel_name kn tag in
+ let tokens = Cic2acic.token_list_of_kernel_name tag in
Some (join_dirs xml_library_root' tokens)
;;
@@ -507,7 +507,7 @@ let print internal glob_ref kind xml_library_root =
let module Ln = Libnames in
(* Variables are the identifiers of the variables in scope *)
let variables = search_variables () in
- let kn,tag,obj =
+ let tag,obj =
match glob_ref with
Ln.VarRef id ->
let sp = Declare.find_section_variable id in
@@ -517,23 +517,22 @@ let print internal glob_ref kind xml_library_root =
N.make_kn mod_path dir_path (N.label_of_id (Ln.basename sp))
in
let (_,body,typ) = G.lookup_named id in
- kn,Cic2acic.Variable,mk_variable_obj id body typ
+ Cic2acic.Variable kn,mk_variable_obj id body typ
| Ln.ConstRef kn ->
- let id = N.id_of_label (N.label kn) in
+ let id = N.id_of_label (N.con_label kn) in
let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
G.lookup_constant kn in
- kn,Cic2acic.Constant,mk_constant_obj id val0 typ variables hyps
+ Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps
| Ln.IndRef (kn,_) ->
let {D.mind_packets=packs ;
D.mind_hyps=hyps;
D.mind_finite=finite} = G.lookup_mind kn in
- kn,Cic2acic.Inductive,
- mk_inductive_obj kn packs variables hyps finite
+ Cic2acic.Inductive kn,mk_inductive_obj kn packs variables hyps finite
| Ln.ConstructRef _ ->
Util.anomaly ("print: this should not happen")
in
- let fn = filename_of_path xml_library_root kn tag in
- let uri = Cic2acic.uri_of_kernel_name kn tag in
+ let fn = filename_of_path xml_library_root tag in
+ let uri = Cic2acic.uri_of_kernel_name tag in
if not internal then print_object_kind uri kind;
print_object uri obj Evd.empty None fn
;;
@@ -562,12 +561,13 @@ let show_pftreestate internal fn (kind,pftst) id =
Decl_kinds.IsLocal ->
let uri =
"cic:/" ^ String.concat "/"
- (Cic2acic.token_list_of_path (Lib.cwd ()) id Cic2acic.Variable) in
+ (Cic2acic.token_list_of_path (Lib.cwd ()) id Cic2acic.TVariable)
+ in
let kind_of_var = "VARIABLE","LocalFact" in
if not internal then print_object_kind uri kind_of_var;
uri
| Decl_kinds.IsGlobal _ ->
- let uri = Cic2acic.uri_of_declaration id Cic2acic.Constant in
+ let uri = Cic2acic.uri_of_declaration id Cic2acic.TConstant in
if not internal then print_object_kind uri (kind_of_global_goal kind);
uri
in
@@ -608,7 +608,7 @@ let _ =
let _ =
Declare.set_xml_declare_constant
- (function (internal,(sp,kn)) ->
+ (function (internal,kn) ->
match !proof_to_export with
None ->
print internal (Libnames.ConstRef kn) (kind_of_constant kn)
@@ -616,9 +616,9 @@ let _ =
| Some pftreestate ->
(* It is a proof. Let's export it starting from the proof-tree *)
(* I saved in the Pfedit.set_xml_cook_proof callback. *)
- let fn = filename_of_path xml_library_root kn Cic2acic.Constant in
+ let fn = filename_of_path xml_library_root (Cic2acic.Constant kn) in
show_pftreestate internal fn pftreestate
- (Names.id_of_label (Names.label kn)) ;
+ (Names.id_of_label (Names.con_label kn)) ;
proof_to_export := None)
;;
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-25 18:22:55 +0000