diff options
Diffstat (limited to 'contrib/xml')
-rw-r--r-- | contrib/xml/cic2Xml.ml | 17 | ||||
-rw-r--r-- | contrib/xml/cic2acic.ml | 99 | ||||
-rw-r--r-- | contrib/xml/doubleTypeInference.ml | 34 | ||||
-rw-r--r-- | contrib/xml/doubleTypeInference.mli | 2 | ||||
-rw-r--r-- | contrib/xml/proof2aproof.ml | 40 | ||||
-rw-r--r-- | contrib/xml/proofTree2Xml.ml4 | 23 | ||||
-rw-r--r-- | contrib/xml/xml.ml4 | 19 | ||||
-rw-r--r-- | contrib/xml/xml.mli | 4 | ||||
-rw-r--r-- | contrib/xml/xmlcommand.ml | 85 | ||||
-rw-r--r-- | contrib/xml/xmlcommand.mli | 2 | ||||
-rw-r--r-- | contrib/xml/xmlentries.ml4 | 2 |
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;; |