From 13d6baa55139729871604c0c3f70a70077ba85ca Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 22 Nov 2005 12:57:06 +0000 Subject: [PATCH] bugfix: return unshared sequent when applying cic -> mathml transformations so that paste work again --- helm/matita/matitaMathView.ml | 59 +++++++++++-------- helm/ocaml/cic_omdoc/cic2acic.ml | 9 +-- helm/ocaml/cic_omdoc/cic2acic.mli | 27 +++++---- .../applyTransformation.ml | 9 +-- .../applyTransformation.mli | 1 + 5 files changed, 60 insertions(+), 45 deletions(-) diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index f9c617385..710efdf02 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -270,13 +270,18 @@ object (self) method update_font_size = self#set_font_size !current_font_size - method private get_term_by_id context cic_info id = - let ids_to_terms, ids_to_hypotheses, _, _, _ = cic_info in + method private get_term_by_id cic_info id = + let unsh_item, ids_to_terms, ids_to_hypotheses, _, _, _ = cic_info in try `Term (Hashtbl.find ids_to_terms id) with Not_found -> try let hyp = Hashtbl.find ids_to_hypotheses id in + let _, context, _ = + match unsh_item with + | Some seq -> seq + | None -> assert false + in let context' = MatitaMisc.list_tl_at hyp context in `Hyp context' with Not_found -> assert false @@ -284,8 +289,8 @@ object (self) method private find_obj_conclusion id = match self#cic_info with | None - | Some (_, _, _, _, None) -> assert false - | Some (ids_to_terms, _, ids_to_father_ids, ids_to_inner_types, Some annobj) -> + | Some (_, _, _, _, _, None) -> assert false + | Some (_, ids_to_terms, _, ids_to_father_ids, ids_to_inner_types, Some annobj) -> let id = find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types in @@ -305,16 +310,11 @@ object (self) in let id = get_id node in let script = MatitaScript.current () in - let metasenv = script#proofMetasenv in - let context = script#proofContext in - let metasenv, context, conclusion = + let metasenv = if script#onGoingProof () then - script#proofMetasenv, script#proofContext, script#proofConclusion + script#proofMetasenv else - [], [], - let t = self#find_obj_conclusion id in - MatitaLog.debug (CicPp.ppterm t); - t + [] in (* TODO: code for patterns let conclusion = (MatitaScript.instance ())#proofConclusion in @@ -323,7 +323,7 @@ object (self) in *) let string_of_cic_sequent cic_sequent = - let acic_sequent, _, _, ids_to_inner_sorts, _ = + let _, (acic_sequent, _, _, ids_to_inner_sorts, _) = Cic2acic.asequent_of_sequent metasenv cic_sequent in let _, _, _, annterm = acic_sequent in @@ -334,19 +334,27 @@ object (self) let markup = CicNotationPres.render ids_to_uris pped_ast in BoxPp.render_to_string text_width markup in - let cic_info = - match self#cic_info with Some info -> info | None -> assert false + let cic_info, unsh_sequent = + match self#cic_info with + | Some ((Some unsh_sequent, _, _, _, _, _) as info) -> + info, unsh_sequent + | Some ((None, _, _, _, _, _) as info) -> + (* building a dummy sequent for obj *) + let t = self#find_obj_conclusion id in + MatitaLog.debug (CicPp.ppterm t); + info, (~-1, [], t) + | None -> assert false in let cic_sequent = - match self#get_term_by_id context cic_info id with + match self#get_term_by_id cic_info id with | `Term t -> let context' = - match - ProofEngineHelpers.locate_in_conjecture t - (~-1, context, conclusion) - with + match ProofEngineHelpers.locate_in_conjecture t unsh_sequent with [context,_] -> context - | _ -> assert false (* since it uses physical equality *) + | _ -> +(* prerr_endline (sprintf "%d\nt=%s\ncontext=%s" + (List.length l) (CicPp.ppterm t) (CicPp.ppcontext context)); *) + assert false (* since it uses physical equality *) in ~-1, context', t | `Hyp context -> ~-1, context, Cic.Rel 1 @@ -379,11 +387,14 @@ object (self) method load_sequent metasenv metano = let sequent = CicUtil.lookup_meta metano metasenv in - let (mathml, (_, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_ ))) = + let (mathml, unsh_sequent, + (_, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_ ))) + = ApplyTransformation.mml_of_cic_sequent metasenv sequent in self#set_cic_info - (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, + (Some (Some unsh_sequent, + ids_to_terms, ids_to_hypotheses, ids_to_father_ids, Hashtbl.create 1, None)); let name = "sequent_viewer.xml" in MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name); @@ -398,7 +409,7 @@ object (self) ApplyTransformation.mml_of_cic_object obj in self#set_cic_info - (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj)); + (Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj)); (match current_mathml with | Some current_mathml when use_diff -> self#freeze; diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index 4c7b955c9..81cfaaf09 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -408,7 +408,7 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) = let ids_to_hypotheses = Hashtbl.create 23 in let hypotheses_seed = ref 0 in let seed = ref 1 in (* 'i0' is used for the whole sequent *) - let sequent = + let unsh_sequent = let i,canonical_context,term = sequent in let canonical_context' = List.fold_right @@ -432,9 +432,10 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) = let (metano,acontext,agoal) = aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed - metasenv sequent in - ("i0",metano,acontext,agoal), - ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses + metasenv unsh_sequent in + (unsh_sequent, + (("i0",metano,acontext,agoal), + ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses)) ;; let acic_object_of_cic_object ?(eta_fix=true) obj = diff --git a/helm/ocaml/cic_omdoc/cic2acic.mli b/helm/ocaml/cic_omdoc/cic2acic.mli index b5a194951..e6379283d 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.mli +++ b/helm/ocaml/cic_omdoc/cic2acic.mli @@ -40,21 +40,22 @@ val sort_of_sort: Cic.sort -> sort_kind val acic_object_of_cic_object : ?eta_fix: bool -> (* perform eta_fixing; default: true*) Cic.obj -> (* object *) - Cic.annobj * (* annotated object *) - (Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *) - (Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *) - (Cic.id, sort_kind) Hashtbl.t * (* ids_to_inner_sorts *) - (Cic.id, anntypes) Hashtbl.t * (* ids_to_inner_types *) - (Cic.id, Cic.conjecture) Hashtbl.t * (* ids_to_conjectures *) - (Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *) + Cic.annobj * (* annotated object *) + (Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *) + (Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *) + (Cic.id, sort_kind) Hashtbl.t * (* ids_to_inner_sorts *) + (Cic.id, anntypes) Hashtbl.t * (* ids_to_inner_types *) + (Cic.id, Cic.conjecture) Hashtbl.t * (* ids_to_conjectures *) + (Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *) val asequent_of_sequent : Cic.metasenv -> (* metasenv *) - Cic.conjecture -> (* conjecture *) - Cic.annconjecture * (* annotated conjecture *) - (Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *) - (Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *) - (Cic.id, sort_kind) Hashtbl.t * (* ids_to_inner_sorts *) - (Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *) + Cic.conjecture -> (* sequent *) + Cic.conjecture * (* unshared sequent *) + (Cic.annconjecture * (* annotated sequent *) + (Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *) + (Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *) + (Cic.id, sort_kind) Hashtbl.t * (* ids_to_inner_sorts *) + (Cic.id, Cic.hypothesis) Hashtbl.t) (* ids_to_hypotheses *) val plain_acic_object_of_cic_object : Cic.obj -> Cic.annobj diff --git a/helm/ocaml/cic_transformations/applyTransformation.ml b/helm/ocaml/cic_transformations/applyTransformation.ml index b6aa36987..54402e0bc 100644 --- a/helm/ocaml/cic_transformations/applyTransformation.ml +++ b/helm/ocaml/cic_transformations/applyTransformation.ml @@ -37,8 +37,8 @@ let mpres_document pres_box = Xml.add_xml_declaration (CicNotationPres.print_box pres_box) let mml_of_cic_sequent metasenv sequent = - let asequent,ids_to_terms, - ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses + let unsh_sequent,(asequent,ids_to_terms, + ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses) = Cic2acic.asequent_of_sequent metasenv sequent in @@ -47,9 +47,10 @@ let mml_of_cic_sequent metasenv sequent = (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) in let xmlpres = mpres_document pres_sequent in - Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres, + (Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres, + unsh_sequent, (asequent, - (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)) + (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts))) let mml_of_cic_object obj = let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, diff --git a/helm/ocaml/cic_transformations/applyTransformation.mli b/helm/ocaml/cic_transformations/applyTransformation.mli index 4642cc67d..8e023aea6 100644 --- a/helm/ocaml/cic_transformations/applyTransformation.mli +++ b/helm/ocaml/cic_transformations/applyTransformation.mli @@ -37,6 +37,7 @@ val mml_of_cic_sequent: Cic.metasenv -> (* metasenv *) Cic.conjecture -> (* sequent *) Gdome.document * (* Math ML *) + Cic.conjecture * (* unshared sequent *) (Cic.annconjecture * (* annsequent *) ((Cic.id, Cic.term) Hashtbl.t * (* id -> term *) (Cic.id, Cic.id option) Hashtbl.t * (* id -> father id *) -- 2.39.2