aboutsummaryrefslogtreecommitdiff
path: root/contrib/xml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/xml')
-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
4 files changed, 51 insertions, 38 deletions
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-02-28 01:31:24 +0000