summaryrefslogtreecommitdiff
path: root/contrib/xml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/xml')
-rw-r--r--contrib/xml/cic2Xml.ml17
-rw-r--r--contrib/xml/cic2acic.ml99
-rw-r--r--contrib/xml/doubleTypeInference.ml34
-rw-r--r--contrib/xml/doubleTypeInference.mli2
-rw-r--r--contrib/xml/proof2aproof.ml40
-rw-r--r--contrib/xml/proofTree2Xml.ml423
-rw-r--r--contrib/xml/xml.ml419
-rw-r--r--contrib/xml/xml.mli4
-rw-r--r--contrib/xml/xmlcommand.ml85
-rw-r--r--contrib/xml/xmlcommand.mli2
-rw-r--r--contrib/xml/xmlentries.ml42
11 files changed, 192 insertions, 135 deletions
diff --git a/contrib/xml/cic2Xml.ml b/contrib/xml/cic2Xml.ml
new file mode 100644
index 00000000..f04a03f9
--- /dev/null
+++ b/contrib/xml/cic2Xml.ml
@@ -0,0 +1,17 @@
+let print_xml_term ch env sigma cic =
+ let ids_to_terms = Hashtbl.create 503 in
+ let constr_to_ids = Acic.CicHash.create 503 in
+ let ids_to_father_ids = Hashtbl.create 503 in
+ let ids_to_inner_sorts = Hashtbl.create 503 in
+ let ids_to_inner_types = Hashtbl.create 503 in
+ let seed = ref 0 in
+ let acic =
+ Cic2acic.acic_of_cic_context' true seed ids_to_terms constr_to_ids
+ ids_to_father_ids ids_to_inner_sorts ids_to_inner_types []
+ env [] sigma (Unshare.unshare cic) None in
+ let xml = Acic2Xml.print_term ids_to_inner_sorts acic in
+ Xml.pp_ch xml ch
+;;
+
+Tacinterp.declare_xml_printer print_xml_term
+;;
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index d820f9e5..bac7ad7c 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 =
@@ -229,10 +242,10 @@ let typeur sigma metamap =
| T.Const c ->
let cb = Environ.lookup_constant c env in
T.body_of_type cb.Declarations.const_type
- | T.Evar ev -> Instantiate.existential_type sigma ev
- | T.Ind ind -> T.body_of_type (Inductive.type_of_inductive env ind)
+ | T.Evar ev -> Evd.existential_type sigma ev
+ | T.Ind ind -> T.body_of_type (Inductiveops.type_of_inductive env ind)
| T.Construct cstr ->
- T.body_of_type (Inductive.type_of_constructor env cstr)
+ T.body_of_type (Inductiveops.type_of_constructor env cstr)
| T.Case (_,p,c,lf) ->
let Inductiveops.IndType(_,realargs) =
try Inductiveops.find_rectype env sigma (type_of env c)
@@ -250,7 +263,7 @@ let typeur sigma metamap =
| T.App(f,args)->
T.strip_outer_cast
(subst_type env sigma (type_of env f) (Array.to_list args))
- | T.Cast (c,t) -> t
+ | T.Cast (c,_, t) -> t
| T.Sort _ | T.Prod _ ->
match sort_of env cstr with
Coq_sort T.InProp -> T.mkProp
@@ -260,7 +273,7 @@ let typeur sigma metamap =
and sort_of env t =
match Term.kind_of_term t with
- | T.Cast (c,s) when T.isSort s -> family_of_term s
+ | T.Cast (c,_, s) when T.isSort s -> family_of_term s
| T.Sort (T.Prop c) -> Coq_sort T.InType
| T.Sort (T.Type u) -> Coq_sort T.InType
| T.Prod (name,t,c2) ->
@@ -270,7 +283,7 @@ let typeur sigma metamap =
| Coq_sort T.InSet, (Coq_sort T.InSet as s) -> s
| Coq_sort T.InType, (Coq_sort T.InSet as s)
| CProp, (Coq_sort T.InSet as s) when
- Environ.engagement env = Some Environ.ImpredicativeSet -> s
+ Environ.engagement env = Some Declarations.ImpredicativeSet -> s
| Coq_sort T.InType, Coq_sort T.InSet
| CProp, Coq_sort T.InSet -> Coq_sort T.InType
| _, (Coq_sort T.InType as s) -> s (*Type Univ.dummy_univ*)
@@ -282,7 +295,7 @@ let typeur sigma metamap =
and sort_family_of env t =
match T.kind_of_term t with
- | T.Cast (c,s) when T.isSort s -> family_of_term s
+ | T.Cast (c,_, s) when T.isSort s -> family_of_term s
| T.Sort (T.Prop c) -> Coq_sort T.InType
| T.Sort (T.Type u) -> Coq_sort T.InType
| T.Prod (name,t,c2) -> sort_family_of (Environ.push_rel (name,None,t) env) c2
@@ -375,7 +388,7 @@ try
Acic.CicHash.find terms_to_types tt
with _ ->
(*CSC: Warning: it really happens, for example in Ring_theory!!! *)
-Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.prterm tt)) ; assert false
+Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.pr_lconstr tt)) ; assert false
else
(* We are already in an inner-type and Coscoy's double *)
(* type inference algorithm has not been applied. *)
@@ -384,19 +397,33 @@ Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-ty
{D.synthesized =
Reductionops.nf_beta
(CPropRetyping.get_type_of env evar_map
- (Evarutil.refresh_universes tt)) ;
+ (Termops.refresh_universes tt)) ;
D.expected = None}
in
(* Debugging only:
print_endline "TERMINE:" ; flush stdout ;
-Pp.ppnl (Printer.prterm tt) ; flush stdout ;
+Pp.ppnl (Printer.pr_lconstr tt) ; flush stdout ;
print_endline "TIPO:" ; flush stdout ;
-Pp.ppnl (Printer.prterm synthesized) ; flush stdout ;
+Pp.ppnl (Printer.pr_lconstr synthesized) ; flush stdout ;
print_endline "ENVIRONMENT:" ; flush stdout ;
Pp.ppnl (Printer.pr_context_of env) ; flush stdout ;
print_endline "FINE_ENVIRONMENT" ; flush stdout ;
*)
- let innersort = get_sort_family_of env evar_map synthesized in
+ let innersort =
+ let synthesized_innersort =
+ get_sort_family_of env evar_map synthesized
+ in
+ match expected with
+ None -> synthesized_innersort
+ | Some ty ->
+ let expected_innersort =
+ get_sort_family_of env evar_map ty
+ in
+ match expected_innersort, synthesized_innersort with
+ CProp, _
+ | _, CProp -> CProp
+ | _, _ -> expected_innersort
+ in
(* Debugging only:
print_endline "PASSATO" ; flush stdout ;
*)
@@ -441,7 +468,7 @@ print_endline "PASSATO" ; flush stdout ;
let subst,residual_args,uninst_vars =
let variables,basedir =
try
- let g = Libnames.reference_of_constr h in
+ let g = Libnames.global_of_constr h in
let sp =
match g with
Libnames.ConstructRef ((induri,_),_)
@@ -533,7 +560,7 @@ print_endline "PASSATO" ; flush stdout ;
(fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l))
| T.Meta _ -> Util.anomaly "Meta met during exporting to XML"
| T.Sort s -> A.ASort (fresh_id'', s)
- | T.Cast (v,t) ->
+ | T.Cast (v,_, t) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if is_a_Prop innersort then
add_inner_type fresh_id'' ;
@@ -670,7 +697,7 @@ print_endline "PASSATO" ; flush stdout ;
let
compute_result_if_eta_expansion_not_required subst residual_args
=
- let residual_args_not_empty = List.length residual_args > 0 in
+ let residual_args_not_empty = residual_args <> [] in
let h' =
if residual_args_not_empty then
aux' env idrefs ~subst:(None,subst) h
@@ -695,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 []
@@ -703,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 []
@@ -715,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 []
@@ -729,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 f0e3f5e3..518f6c11 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 [])
@@ -40,13 +40,13 @@ let whd_betadeltaiotacprop env evar_map ty =
Conv_oracle.set_opaque_const cprop;
prerr_endline "###whd_betadeltaiotacprop:" ;
let xxx =
-(*Pp.msgerr (Printer.prterm_env env ty);*)
+(*Pp.msgerr (Printer.pr_lconstr_env env ty);*)
prerr_endline "";
- Tacred.reduction_of_redexp red_exp env evar_map ty
+ (fst (Redexpr.reduction_of_red_expr red_exp)) env evar_map ty
in
prerr_endline "###FINE" ;
(*
-Pp.msgerr (Printer.prterm_env env xxx);
+Pp.msgerr (Printer.pr_lconstr_env env xxx);
*)
prerr_endline "";
Conv_oracle.set_transparent_const cprop;
@@ -89,10 +89,11 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
"DoubleTypeInference.double_type_of: found a non-instanciated goal"
| T.Evar ((n,l) as ev) ->
- let ty = Unshare.unshare (Instantiate.existential_type sigma ev) in
+ let ty = Unshare.unshare (Evd.existential_type sigma ev) in
let jty = execute env sigma ty None in
let jty = assumption_of_judgment env sigma jty in
- let evar_context = (Evd.map sigma n).Evd.evar_hyps in
+ let evar_context =
+ E.named_context_of_val (Evd.map sigma n).Evd.evar_hyps in
let rec iter actual_args evar_context =
match actual_args,evar_context with
[],[] -> ()
@@ -124,10 +125,10 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
E.make_judge cstr (E.constant_type env c)
| T.Ind ind ->
- E.make_judge cstr (Inductive.type_of_inductive env ind)
+ E.make_judge cstr (Inductiveops.type_of_inductive env ind)
| T.Construct cstruct ->
- E.make_judge cstr (Inductive.type_of_constructor env cstruct)
+ E.make_judge cstr (Inductiveops.type_of_constructor env cstruct)
| T.Case (ci,p,c,lf) ->
let expectedtype =
@@ -230,11 +231,11 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
let j3 = execute env1 sigma c3 None in
Typeops.judge_of_letin env name j1 j2 j3
- | T.Cast (c,t) ->
+ | T.Cast (c,k,t) ->
let cj = execute env sigma c (Some (Reductionops.nf_beta t)) in
let tj = execute env sigma t None in
let tj = type_judgment env sigma tj in
- let j, _ = Typeops.judge_of_cast env cj tj in
+ let j, _ = Typeops.judge_of_cast env cj k tj in
j
in
let synthesized = E.j_type judgement in
@@ -244,19 +245,20 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
None ->
(* No expected type *)
{synthesized = synthesized' ; expected = None}, synthesized
- (*CSC: in HELM we did not considered Casts to be irrelevant. *)
- (*CSC: does it really matter? (eq_constr is up to casts) *)
| Some ty when Term.eq_constr synthesized' ty ->
- (* The expected type is synthactically equal to *)
- (* the synthesized type. Let's forget it. *)
- {synthesized = synthesized' ; expected = None}, synthesized
+ (* The expected type is synthactically equal to the *)
+ (* synthesized type. Let's forget it. *)
+ (* Note: since eq_constr is up to casts, it is better *)
+ (* to keep the expected type, since it can bears casts *)
+ (* that change the innersort to CProp *)
+ {synthesized = ty ; expected = None}, ty
| Some expectedty' ->
{synthesized = synthesized' ; expected = Some expectedty'},
expectedty'
in
(*CSC: debugging stuff to be removed *)
if Acic.CicHash.mem subterms_to_types cstr then
- (Pp.ppnl (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.prterm cstr)) ; flush stdout ) ;
+ (Pp.ppnl (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.pr_lconstr cstr)) ; flush stdout ) ;
Acic.CicHash.add subterms_to_types cstr types ;
E.make_judge cstr res
diff --git a/contrib/xml/doubleTypeInference.mli b/contrib/xml/doubleTypeInference.mli
index 33d3e5cd..2e14b558 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/proof2aproof.ml b/contrib/xml/proof2aproof.ml
index 165a456d..dff546c9 100644
--- a/contrib/xml/proof2aproof.ml
+++ b/contrib/xml/proof2aproof.ml
@@ -32,7 +32,7 @@ let nf_evar sigma ~preserve =
match T.kind_of_term t with
| T.Rel _ | T.Meta _ | T.Var _ | T.Sort _ | T.Const _ | T.Ind _
| T.Construct _ -> t
- | T.Cast (c1,c2) -> T.mkCast (aux c1, aux c2)
+ | T.Cast (c1,k,c2) -> T.mkCast (aux c1, k, aux c2)
| T.Prod (na,c1,c2) -> T.mkProd (na, aux c1, aux c2)
| T.Lambda (na,t,c) -> T.mkLambda (na, aux t, aux c)
| T.LetIn (na,b,t,c) -> T.mkLetIn (na, aux b, aux t, aux c)
@@ -41,14 +41,14 @@ let nf_evar sigma ~preserve =
let l' = Array.map aux l in
(match T.kind_of_term c' with
T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l')
- | T.Cast (he,_) ->
+ | T.Cast (he,_,_) ->
(match T.kind_of_term he with
T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l')
| _ -> T.mkApp (c', l')
)
| _ -> T.mkApp (c', l'))
| T.Evar (e,l) when Evd.in_dom sigma e & Evd.is_defined sigma e ->
- aux (Instantiate.existential_value sigma (e,l))
+ aux (Evd.existential_value sigma (e,l))
| T.Evar (e,l) -> T.mkEvar (e, Array.map aux l)
| T.Case (ci,p,c,bl) -> T.mkCase (ci, aux p, aux c, Array.map aux bl)
| T.Fix (ln,(lna,tl,bl)) ->
@@ -93,7 +93,7 @@ module ProofTreeHash =
let extract_open_proof sigma pf =
let module PT = Proof_type in
let module L = Logic in
- let sigma = ref sigma in
+ let evd = ref (Evd.create_evar_defs sigma) in
let proof_tree_to_constr = ProofTreeHash.create 503 in
let proof_tree_to_flattened_proof_tree = ProofTreeHash.create 503 in
let unshared_constrs = ref S.empty in
@@ -117,34 +117,39 @@ let extract_open_proof sigma pf =
(fun id ->
(* Section variables are in the [id] list but are not *)
(* lambda abstracted in the term [vl] *)
- try let n = Util.list_index id vl in (n,id)
+ try let n = Logic.proof_variable_index id vl in (n,id)
with Not_found -> failwith "caught")
(*CSC: the above function must be modified such that when it is found *)
(*CSC: it becomes a Rel; otherwise a Var. Then it can be already used *)
(*CSC: as the evar_instance. Ordering the instance becomes useless (it *)
(*CSC: will already be ordered. *)
- (Termops.ids_of_named_context goal.Evd.evar_hyps) in
+ (Termops.ids_of_named_context
+ (Environ.named_context_of_val goal.Evd.evar_hyps)) in
let sorted_rels =
Sort.list (fun (n1,_) (n2,_) -> n1 < n2 ) visible_rels in
let context =
- List.map
- (fun (_,id) -> Sign.lookup_named id goal.Evd.evar_hyps)
- sorted_rels
+ let l =
+ List.map
+ (fun (_,id) -> Sign.lookup_named id
+ (Environ.named_context_of_val goal.Evd.evar_hyps))
+ sorted_rels in
+ Environ.val_of_named_context l
in
(*CSC: the section variables in the right order must be added too *)
let evar_instance = List.map (fun (n,_) -> Term.mkRel n) sorted_rels in
- let env = Global.env_of_context context in
- let sigma',evar =
- Evarutil.new_isevar_sign env !sigma goal.Evd.evar_concl evar_instance
- in
- sigma := sigma' ;
+ (* let env = Global.env_of_context context in *)
+ let evd',evar =
+ Evarutil.new_evar_instance context !evd goal.Evd.evar_concl
+ evar_instance in
+ evd := evd' ;
evar
| _ -> Util.anomaly "Bug : a case has been forgotten in proof_extractor"
in
let unsharedconstr =
let evar_nf_constr =
- nf_evar !sigma ~preserve:(function e -> S.mem e !unshared_constrs) constr
+ nf_evar (Evd.evars_of !evd)
+ ~preserve:(function e -> S.mem e !unshared_constrs) constr
in
Unshare.unshare
~already_unshared:(function e -> S.mem e !unshared_constrs)
@@ -152,14 +157,15 @@ let extract_open_proof sigma pf =
in
(*CSC: debugging stuff to be removed *)
if ProofTreeHash.mem proof_tree_to_constr node then
- Pp.ppnl (Pp.(++) (Pp.str "#DUPLICATE INSERTION: ") (Refiner.print_proof !sigma [] node)) ;
+ Pp.ppnl (Pp.(++) (Pp.str "#DUPLICATE INSERTION: ")
+ (Tactic_printer.print_proof (Evd.evars_of !evd) [] node)) ;
ProofTreeHash.add proof_tree_to_constr node unsharedconstr ;
unshared_constrs := S.add unsharedconstr !unshared_constrs ;
unsharedconstr
in
let unshared_pf = unshare_proof_tree pf in
let pfterm = proof_extractor [] unshared_pf in
- (pfterm, !sigma, proof_tree_to_constr, proof_tree_to_flattened_proof_tree,
+ (pfterm, Evd.evars_of !evd, proof_tree_to_constr, proof_tree_to_flattened_proof_tree,
unshared_pf)
;;
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index b9b66774..578c1ed2 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -46,7 +46,8 @@ let constr_to_xml obj sigma env =
let rel_context = Sign.push_named_to_rel_context named_context' [] in
let rel_env =
Environ.push_rel_context rel_context
- (Environ.reset_with_named_context real_named_context env) in
+ (Environ.reset_with_named_context
+ (Environ.val_of_named_context real_named_context) env) in
let obj' =
Term.subst_vars (List.map (function (i,_,_) -> i) named_context') obj in
let seed = ref 0 in
@@ -66,9 +67,9 @@ Pp.ppnl (Pp.str "Problem during the conversion of constr into XML") ;
Pp.ppnl (Pp.str "ENVIRONMENT:") ;
Pp.ppnl (Printer.pr_context_of rel_env) ;
Pp.ppnl (Pp.str "TERM:") ;
-Pp.ppnl (Printer.prterm_env rel_env obj') ;
+Pp.ppnl (Printer.pr_lconstr_env rel_env obj') ;
Pp.ppnl (Pp.str "RAW-TERM:") ;
-Pp.ppnl (Printer.prterm obj') ;
+Pp.ppnl (Printer.pr_lconstr obj') ;
Xml.xml_empty "MISSING TERM" [] (*; raise e*)
*)
;;
@@ -95,7 +96,7 @@ let string_of_prim_rule x = match x with
let
- print_proof_tree curi sigma0 pf proof_tree_to_constr
+ print_proof_tree curi sigma pf proof_tree_to_constr
proof_tree_to_flattened_proof_tree constr_to_ids
=
let module PT = Proof_type in
@@ -119,7 +120,7 @@ in
with _ ->
Pp.ppnl (Pp.(++) (Pp.str
"The_generated_term_is_not_a_subterm_of_the_final_lambda_term")
-(Printer.prterm constr)) ;
+(Printer.pr_lconstr constr)) ;
None
in
let rec aux node old_hyps =
@@ -155,7 +156,7 @@ Pp.ppnl (Pp.(++) (Pp.str
aux flat_proof old_hyps
| _ ->
(****** la tactique employee *)
- let prtac = if !Options.v7 then Pptactic.pr_tactic else Pptacticnew.pr_tactic (Global.env()) in
+ let prtac = Pptactic.pr_tactic (Global.env()) in
let tac = std_ppcmds_to_string (prtac tactic_expr) in
let tacname= first_word tac in
let of_attribute = ("name",tacname)::("script",tac)::of_attribute in
@@ -164,10 +165,7 @@ Pp.ppnl (Pp.(++) (Pp.str
let {Evd.evar_concl=concl;
Evd.evar_hyps=hyps}=goal in
- let rc = (Proof_trees.rc_of_gc sigma0 goal) in
- let sigma = Proof_trees.get_gc rc in
- let hyps = Proof_trees.get_hyps rc in
- let env= Proof_trees.get_env rc in
+ let env = Global.env_of_context hyps in
let xgoal =
X.xml_nempty "Goal" [] (constr_to_xml concl sigma env) in
@@ -183,11 +181,12 @@ Pp.ppnl (Pp.(++) (Pp.str
(constr_to_xml tid sigma env))
>] in
let old_names = List.map (fun (id,c,tid)->id) old_hyps in
+ let nhyps = Environ.named_context_of_val hyps in
let new_hyps =
- List.filter (fun (id,c,tid)-> not (List.mem id old_names)) hyps in
+ List.filter (fun (id,c,tid)-> not (List.mem id old_names)) nhyps in
X.xml_nempty "Tactic" of_attribute
- [<(build_hyps new_hyps) ; (aux flat_proof hyps)>]
+ [<(build_hyps new_hyps) ; (aux flat_proof nhyps)>]
end
| {PT.ref=Some(PT.Change_evars,nodes)} ->
diff --git a/contrib/xml/xml.ml4 b/contrib/xml/xml.ml4
index d0c64f30..e2d04cb7 100644
--- a/contrib/xml/xml.ml4
+++ b/contrib/xml/xml.ml4
@@ -31,8 +31,7 @@ let xml_cdata str = [< 'Str str >]
(* Usage: *)
(* pp tokens None pretty prints the output on stdout *)
(* pp tokens (Some filename) pretty prints the output on the file filename *)
-let pp strm fn =
- let channel = ref stdout in
+let pp_ch strm channel =
let rec pp_r m =
parser
[< 'Str a ; s >] ->
@@ -58,16 +57,22 @@ let pp strm fn =
and print_spaces m =
for i = 1 to m do fprint_string " " done
and fprint_string str =
- output_string !channel str
+ output_string channel str
in
+ pp_r 0 strm
+;;
+
+
+let pp strm fn =
match fn with
Some filename ->
let filename = filename ^ ".xml" in
- channel := open_out filename ;
- pp_r 0 strm ;
- close_out !channel ;
+ let ch = open_out filename in
+ pp_ch strm ch;
+ close_out ch ;
print_string ("\nWriting on file \"" ^ filename ^ "\" was succesful\n");
flush stdout
| None ->
- pp_r 0 strm
+ pp_ch strm stdout
;;
+
diff --git a/contrib/xml/xml.mli b/contrib/xml/xml.mli
index e65e6c81..38a4e01c 100644
--- a/contrib/xml/xml.mli
+++ b/contrib/xml/xml.mli
@@ -12,7 +12,7 @@
(* http://helm.cs.unibo.it *)
(************************************************************************)
-(*i $Id: xml.mli,v 1.5.2.2 2004/07/16 19:30:15 herbelin Exp $ i*)
+(*i $Id: xml.mli 6681 2005-02-04 18:20:16Z herbelin $ i*)
(* Tokens for XML cdata, empty elements and not-empty elements *)
(* Usage: *)
@@ -31,6 +31,8 @@ val xml_nempty :
string -> (string * string) list -> token Stream.t -> token Stream.t
val xml_cdata : string -> token Stream.t
+val pp_ch : token Stream.t -> out_channel -> unit
+
(* The pretty printer for streams of token *)
(* Usage: *)
(* pp tokens None pretty prints the output on stdout *)
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 9fba5474..871a7f15 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -38,6 +38,8 @@ let print_if_verbose s = if !verbose then print_string s;;
(* Next exception is used only inside print_coq_object and tag_of_string_tag *)
exception Uninteresting;;
+(* NOT USED anymore, we back to the V6 point of view with global parameters
+
(* Internally, for Coq V7, params of inductive types are associated *)
(* not to the whole block of mutual inductive (as it was in V6) but to *)
(* each member of the block; but externally, all params are required *)
@@ -60,6 +62,8 @@ let extract_nparams pack =
done;
nparams0
+*)
+
(* could_have_namesakes sp = true iff o is an object that could be cooked and *)
(* than that could exists in cooked form with the same name in a super *)
(* section of the actual section *)
@@ -177,12 +181,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)
;;
@@ -210,7 +214,6 @@ let theory_filename xml_library_root =
None -> None (* stdout *)
| Some xml_library_root' ->
let toks = List.map N.string_of_id (N.repr_dirpath (Lib.library_dp ())) in
- let hd = List.hd toks in
(* theory from A/B/C/F.v goes into A/B/C/F.theory *)
let alltoks = List.rev toks in
Some (join_dirs xml_library_root' alltoks ^ ".theory")
@@ -286,7 +289,7 @@ let find_hyps t =
| T.Meta _
| T.Evar _
| T.Sort _ -> l
- | T.Cast (te,ty) -> aux (aux l te) ty
+ | T.Cast (te,_, ty) -> aux (aux l te) ty
| T.Prod (_,s,t) -> aux (aux l s) t
| T.Lambda (_,s,t) -> aux (aux l s) t
| T.LetIn (_,s,_,t) -> aux (aux l s) t
@@ -355,11 +358,11 @@ let mk_current_proof_obj is_a_variable id bo ty evar_map env =
(* t will not be exported to XML. Thus no unsharing performed *)
final_var_ids,(n, Acic.Def (Unshare.unshare b',t))::tl'
in
- aux [] (List.rev evar_hyps)
+ aux [] (List.rev (Environ.named_context_of_val evar_hyps))
in
(* We map the named context to a rel context and every Var to a Rel *)
(n,context,Unshare.unshare (Term.subst_vars final_var_ids evar_concl))
- ) (Evd.non_instantiated evar_map)
+ ) (Evarutil.non_instantiated evar_map)
in
let id' = Names.string_of_id id in
if metasenv = [] then
@@ -392,11 +395,11 @@ let mk_constant_obj id bo ty variables hyps =
ty,params)
;;
-let mk_inductive_obj sp packs variables hyps finite =
+let mk_inductive_obj sp packs variables nparams hyps finite =
let module D = Declarations in
let hyps = string_list_of_named_context_list hyps in
let params = filter_params variables hyps in
- let nparams = extract_nparams packs in
+(* let nparams = extract_nparams packs in *)
let tys =
let tyno = ref (Array.length packs) in
Array.fold_right
@@ -406,7 +409,7 @@ let mk_inductive_obj sp packs variables hyps finite =
D.mind_typename=typename ;
D.mind_nf_arity=arity} = p
in
- let lc = Inductive.arities_of_constructors (Global.env ()) (sp,!tyno) in
+ let lc = Inductiveops.arities_of_constructors (Global.env ()) (sp,!tyno) in
let cons =
(Array.fold_right (fun (name,lc) i -> (name,lc)::i)
(Array.mapi
@@ -430,16 +433,10 @@ let theory_output_string ?(do_not_quote = false) s =
Buffer.add_string theory_buffer s
;;
-let kind_of_theorem = function
- | Decl_kinds.Theorem -> "Theorem"
- | Decl_kinds.Lemma -> "Lemma"
- | Decl_kinds.Fact -> "Fact"
- | Decl_kinds.Remark -> "Remark"
-
let kind_of_global_goal = function
- | Decl_kinds.IsGlobal Decl_kinds.DefinitionBody -> "DEFINITION","InteractiveDefinition"
- | Decl_kinds.IsGlobal (Decl_kinds.Proof k) -> "THEOREM",kind_of_theorem k
- | Decl_kinds.IsLocal -> assert false
+ | Decl_kinds.Global, Decl_kinds.DefinitionBody _ -> "DEFINITION","InteractiveDefinition"
+ | Decl_kinds.Global, (Decl_kinds.Proof k) -> "THEOREM",Decl_kinds.string_of_theorem_kind k
+ | Decl_kinds.Local, _ -> assert false
let kind_of_inductive isrecord kn =
"DEFINITION",
@@ -454,9 +451,9 @@ let kind_of_variable id =
| DK.IsAssumption DK.Definitional -> "VARIABLE","Assumption"
| DK.IsAssumption DK.Logical -> "VARIABLE","Hypothesis"
| DK.IsAssumption DK.Conjectural -> "VARIABLE","Conjecture"
- | DK.IsDefinition -> "VARIABLE","LocalDefinition"
- | DK.IsConjecture -> "VARIABLE","Conjecture"
- | DK.IsProof DK.LocalStatement -> "VARIABLE","LocalFact"
+ | DK.IsDefinition DK.Definition -> "VARIABLE","LocalDefinition"
+ | DK.IsProof _ -> "VARIABLE","LocalFact"
+ | _ -> Util.anomaly "Unsupported variable kind"
;;
let kind_of_constant kn =
@@ -465,9 +462,10 @@ let kind_of_constant kn =
| DK.IsAssumption DK.Definitional -> "AXIOM","Declaration"
| DK.IsAssumption DK.Logical -> "AXIOM","Axiom"
| DK.IsAssumption DK.Conjectural -> "AXIOM","Conjecture"
- | DK.IsDefinition -> "DEFINITION","Definition"
- | DK.IsConjecture -> "THEOREM","Conjecture"
- | DK.IsProof thm -> "THEOREM",kind_of_theorem thm
+ | DK.IsDefinition DK.Definition -> "DEFINITION","Definition"
+ | DK.IsDefinition DK.Example -> "DEFINITION","Example"
+ | DK.IsDefinition _ -> Util.anomaly "Unsupported constant kind"
+ | DK.IsProof thm -> "THEOREM",DK.string_of_theorem_kind thm
;;
let kind_of_global r =
@@ -476,7 +474,7 @@ let kind_of_global r =
match r with
| Ln.IndRef kn | Ln.ConstructRef (kn,_) ->
let isrecord =
- try let _ = Recordops.find_structure kn in true
+ try let _ = Recordops.lookup_structure kn in true
with Not_found -> false in
kind_of_inductive isrecord (fst kn)
| Ln.VarRef id -> kind_of_variable id
@@ -509,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
@@ -519,23 +517,23 @@ 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 ;
+ let {D.mind_nparams=nparams;
+ 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 nparams 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
;;
@@ -558,18 +556,19 @@ let show_pftreestate internal fn (kind,pftst) id =
let kn = Lib.make_kn id in
let env = Global.env () in
let obj =
- mk_current_proof_obj (kind = Decl_kinds.IsLocal) id val0 typ evar_map env in
+ mk_current_proof_obj (fst kind = Decl_kinds.Local) id val0 typ evar_map env in
let uri =
match kind with
- Decl_kinds.IsLocal ->
+ Decl_kinds.Local, _ ->
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
+ | Decl_kinds.Global, _ ->
+ 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
@@ -610,7 +609,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)
@@ -618,9 +617,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)
;;
@@ -675,7 +674,7 @@ let _ =
let dot = if fn.[0]='/' then "." else "" in
command ("mv "^dir^"/"^dot^"*.html "^fn^".xml ");
command ("rm "^fn^".v");
- print_string("\nWriting on file \"" ^ fn ^ ".xml\" was succesful\n"))
+ print_string("\nWriting on file \"" ^ fn ^ ".xml\" was successful\n"))
ofn)
;;
diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli
index 9a7464bd..7c0d31a1 100644
--- a/contrib/xml/xmlcommand.mli
+++ b/contrib/xml/xmlcommand.mli
@@ -12,7 +12,7 @@
(* http://helm.cs.unibo.it *)
(************************************************************************)
-(*i $Id: xmlcommand.mli,v 1.18.2.2 2004/07/16 19:30:15 herbelin Exp $ i*)
+(*i $Id: xmlcommand.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
(* print_global qid fn *)
(* where qid is a long name denoting a definition/theorem or *)
diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4
index 2bc686f7..496debe1 100644
--- a/contrib/xml/xmlentries.ml4
+++ b/contrib/xml/xmlentries.ml4
@@ -14,7 +14,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: xmlentries.ml4,v 1.12.2.2 2004/07/16 19:30:15 herbelin Exp $ *)
+(* $Id: xmlentries.ml4 5920 2004-07-16 20:01:26Z herbelin $ *)
open Util;;
open Vernacinterp;;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 01:48:37 +0000