From: Enrico Tassi Date: Fri, 21 Jan 2005 11:52:24 +0000 (+0000) Subject: - sync with the new ApplyTransformation API X-Git-Tag: V_0_1_0~99 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=18bd1d094e9227822ea8c0fa4f9668cd8752236f;p=helm.git - sync with the new ApplyTransformation API --- diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index d1cda56b3..8bc736bea 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -13,8 +13,6 @@ termEditor.cmo: disambiguatingParser.cmi termEditor.cmi termEditor.cmx: disambiguatingParser.cmx termEditor.cmi texTermEditor.cmo: disambiguatingParser.cmi texTermEditor.cmi texTermEditor.cmx: disambiguatingParser.cmx texTermEditor.cmi -chosenTransformer.cmo: chosenTransformer.cmi -chosenTransformer.cmx: chosenTransformer.cmi termViewer.cmo: logicalOperations.cmi termViewer.cmi termViewer.cmx: logicalOperations.cmx termViewer.cmi invokeTactics.cmo: logicalOperations.cmi proofEngine.cmi termEditor.cmi \ @@ -27,12 +25,12 @@ chosenTermEditor.cmo: termEditor.cmi chosenTermEditor.cmi chosenTermEditor.cmx: termEditor.cmx chosenTermEditor.cmi helmGtkLogger.cmo: helmGtkLogger.cmi helmGtkLogger.cmx: helmGtkLogger.cmi -gTopLevel.cmo: chosenTermEditor.cmi chosenTransformer.cmi \ - disambiguatingParser.cmi hbugs.cmi helmGtkLogger.cmi invokeTactics.cmi \ - logicalOperations.cmi proofEngine.cmi termEditor.cmi termViewer.cmi -gTopLevel.cmx: chosenTermEditor.cmx chosenTransformer.cmx \ - disambiguatingParser.cmx hbugs.cmx helmGtkLogger.cmx invokeTactics.cmx \ - logicalOperations.cmx proofEngine.cmx termEditor.cmx termViewer.cmx +gTopLevel.cmo: chosenTermEditor.cmi disambiguatingParser.cmi hbugs.cmi \ + helmGtkLogger.cmi invokeTactics.cmi logicalOperations.cmi proofEngine.cmi \ + termEditor.cmi termViewer.cmi +gTopLevel.cmx: chosenTermEditor.cmx disambiguatingParser.cmx hbugs.cmx \ + helmGtkLogger.cmx invokeTactics.cmx logicalOperations.cmx proofEngine.cmx \ + termEditor.cmx termViewer.cmx regtest.cmo: batchParser.cmi disambiguatingParser.cmi regtest.cmx: batchParser.cmx disambiguatingParser.cmx testlibrary.cmo: batchParser.cmi diff --git a/helm/gTopLevel/configure.ac b/helm/gTopLevel/configure.ac index 2cddc9dbe..27d1ac8df 100644 --- a/helm/gTopLevel/configure.ac +++ b/helm/gTopLevel/configure.ac @@ -60,20 +60,6 @@ else fi fi -AC_ARG_WITH(transformer, - AS_HELP_STRING([--with-transformer=(xslt|ocaml)], - [choose mathml transformer (default is ocaml)]), - [TRANSFORMER=$withval], [TRANSFORMER=ocaml]) -if test $TRANSFORMER = "xslt"; then - CHOSEN_TRANSFORMER="include ApplyStylesheets" -else - if test $TRANSFORMER = "ocaml"; then - CHOSEN_TRANSFORMER="include ApplyTransformation" - else - AC_MSG_ERROR(unknwon transformer $TRANSFORMER) - fi -fi - if test $TERM_EDITOR = "tex"; then CHOSEN_TERM_EDITOR="include TexTermEditor" else @@ -87,10 +73,8 @@ fi AC_SUBST(OCAMLFIND) AC_SUBST(CHOSEN_TERM_EDITOR) AC_SUBST(CHOSEN_TERM_PARSER) -AC_SUBST(CHOSEN_TRANSFORMER) AC_OUTPUT([ - chosenTransformer.ml chosenTermEditor.ml disambiguatingParser.ml Makefile diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 5eba45750..f7d502066 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -144,7 +144,7 @@ let check_window uris = lazy (let mmlwidget = TermViewer.sequent_viewer - ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent ~packing:scrolled_window#add ~width:400 ~height:280 () in let expr = let term = CicUtil.term_of_uri uri in @@ -448,7 +448,8 @@ let qed () = begin (*CSC: Wrong: [] is just plainly wrong *) let proof = - Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in + Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[],[]) + in let (acic,ids_to_inner_types,ids_to_inner_sorts) = (rendering_window ())#output#load_proof uri proof in @@ -458,7 +459,8 @@ let qed () = pathname_of_annuri (UriManager.buri_of_uri uri) in let list_of_universes = - CicUnivUtils.universes_of_obj uri (Cic.Constant ("",None,ty,[])) + CicUnivUtils.universes_of_obj uri + (Cic.Constant ("",None,ty,[],[])) in let u1_clean = CicUniv.clean_ugraph u1 list_of_universes in let u2 = CicUniv.fill_empty_nodes_with_uri u1_clean uri in @@ -474,7 +476,7 @@ let qed () = (* add the object to the env *) CicEnvironment.add_type_checked_term uri (( Cic.Constant ((UriManager.name_of_uri uri), - (Some bo),ty,[])),u2); + (Some bo),ty,[],[])),u2); (* FIXME: the variable list!! *) prerr_endline "-------------> FINE"; end @@ -560,7 +562,7 @@ let refresh_proof (output : TermViewer.proof_viewer) = (*CSC: Wrong: [] is just plainly wrong *) let uri = match uri with Some uri -> uri | _ -> assert false in (uri, - Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])) + Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[])) in ignore (output#load_proof uri currentproof) with @@ -568,7 +570,8 @@ let refresh_proof (output : TermViewer.proof_viewer) = match ProofEngine.get_proof () with None -> assert false | Some (uri,metasenv,bo,ty) -> - debug_print ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))); + debug_print ("Offending proof: " ^ + CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[],[]))); raise (InvokeTactics.RefreshProofException e) let set_proof_engine_goal g = @@ -684,7 +687,7 @@ let load_unfinished_proof () = let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in let proof_file = Helm_registry.get "gtoplevel.proof_file" in match CicParser.obj_of_xml proof_file_type (Some proof_file) with - Cic.CurrentProof (_,metasenv,bo,ty,_) -> + Cic.CurrentProof (_,metasenv,bo,ty,_,_) -> typecheck_loaded_proof metasenv bo ty ; ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)); refresh_proof output ; @@ -859,15 +862,9 @@ let let href = Gdome.domString "href" in let show_in_show_window_obj uri obj = try - let - (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, - ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) - = - Cic2acic.acic_object_of_cic_object obj - in - let mml = - ChosenTransformer.mml_of_cic_object - ~explode_all:false uri acic ids_to_inner_sorts ids_to_inner_types + let mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_conjectures, + ids_to_hypotheses,_,_)) = + ApplyTransformation.mml_of_cic_object uri obj in window#set_title (UriManager.string_of_uri uri) ; window#misc#hide () ; window#show () ; @@ -1376,7 +1373,7 @@ let new_inductive () = (*CSC: Da finire *) let params = [] in let tys = !get_types_and_cons () in - let obj = Cic.InductiveDefinition(tys,params,!paramsno) in + let obj = Cic.InductiveDefinition(tys,params,!paramsno,[]) in let u = begin try @@ -1592,8 +1589,8 @@ let open_ () = (* TASSI: typecheck mette la uri nell'env... cosa fa la open_ ?*) let metasenv,bo,ty = match fst(CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri ) with - Cic.Constant (_,Some bo,ty,_) -> [],bo,ty - | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty + Cic.Constant (_,Some bo,ty,_,_) -> [],bo,ty + | Cic.CurrentProof (_,metasenv,bo,ty,_,_) -> metasenv,bo,ty | Cic.Constant _ | Cic.Variable _ | Cic.InductiveDefinition _ -> raise NotADefinition @@ -2264,7 +2261,7 @@ class scratch_window = ~packing:(vbox#pack ~expand:true ~padding:5) () in let sequent_viewer = TermViewer.sequent_viewer - ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent ~packing:(scrolled_window#add) ~width:400 ~height:280 () in object(self) val mutable term = Cic.Rel 1 (* dummy value *) @@ -2346,7 +2343,7 @@ object(self) ~packing:(vbox1#pack ~expand:true ~padding:5) () in let proofw = TermViewer.sequent_viewer - ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in let _ = proofw_ref <- Some proofw in let hbox3 = @@ -2527,7 +2524,7 @@ class empty_page = ~packing:(vbox1#pack ~expand:true ~padding:5) () in let proofw = TermViewer.sequent_viewer - ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in object(self) method proofw = (assert false : TermViewer.sequent_viewer) @@ -2763,7 +2760,6 @@ class rendering_window output (notebook : notebook) = factory3#add_item "Reload Stylesheets" ~callback: (function _ -> - ChosenTransformer.reload_stylesheets () ; if ProofEngine.get_proof () <> None then try refresh_goals notebook ; @@ -2847,7 +2843,7 @@ end let initialize_everything () = let output = TermViewer.proof_viewer - ~mml_of_cic_object:ChosenTransformer.mml_of_cic_object + ~mml_of_cic_object:ApplyTransformation.mml_of_cic_object ~width:350 ~height:280 () in let notebook = new notebook in diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 9292ece0b..0cfd8f07c 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -41,7 +41,7 @@ let get_current_status_as_xml () = let uri = match uri with Some uri -> uri | None -> assert false in let currentproof = (*CSC: Wrong: [] is just plainly wrong *) - Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[]) + Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[]) in let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) = Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml index 97fa7536a..23d7543d3 100644 --- a/helm/gTopLevel/termViewer.ml +++ b/helm/gTopLevel/termViewer.ml @@ -38,18 +38,26 @@ let debug_print s = if debug then prerr_endline s type mml_of_cic_sequent = Cic.metasenv -> int * Cic.context * Cic.term -> - Gdome.document * + Gdome.document * + (Cic.annconjecture * ((Cic.id, Cic.term) Hashtbl.t * (Cic.id, Cic.id option) Hashtbl.t * - (string, Cic.hypothesis) Hashtbl.t) + (string, Cic.hypothesis) Hashtbl.t * + (Cic.id, string) Hashtbl.t)) + type mml_of_cic_object = - explode_all:bool -> UriManager.uri -> - Cic.annobj -> - (string, string) Hashtbl.t -> - (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document - + Cic.obj -> + Gdome.document * + (Cic.annobj * + ((Cic.id, Cic.term) Hashtbl.t * + (Cic.id, Cic.id option) Hashtbl.t * + (Cic.id, Cic.conjecture) Hashtbl.t * + (Cic.id, Cic.hypothesis) Hashtbl.t * + (Cic.id, string) Hashtbl.t * + (Cic.id, Cic2acic.anntypes) Hashtbl.t)) + (* List utility functions *) exception Skip;; @@ -124,7 +132,7 @@ class sequent_viewer ~(mml_of_cic_sequent:mml_of_cic_sequent) obj = method load_sequent metasenv sequent = (**** SIAM QUI ****) - let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) = + let sequent_mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)) = mml_of_cic_sequent metasenv sequent in self#load_root ~root:sequent_mml#get_documentElement ; @@ -222,14 +230,11 @@ class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) obj = | None -> assert false (* "ERROR: No selection!!!" *) method load_proof uri currentproof = - let - (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, - ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) - = Cic2acic.acic_object_of_cic_object currentproof - in - let mml = - mml_of_cic_object - ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types + let mml, + (acic, + (ids_to_terms,ids_to_father_ids,ids_to_conjectures, + ids_to_hypotheses,ids_to_inner_sorts,ids_to_inner_types)) = + mml_of_cic_object uri currentproof in current_infos <- Some diff --git a/helm/gTopLevel/termViewer.mli b/helm/gTopLevel/termViewer.mli index 71ab63bc0..5a8ff7253 100644 --- a/helm/gTopLevel/termViewer.mli +++ b/helm/gTopLevel/termViewer.mli @@ -36,17 +36,25 @@ type mml_of_cic_sequent = Cic.metasenv -> int * Cic.context * Cic.term -> - Gdome.document * + Gdome.document * + (Cic.annconjecture * ((Cic.id, Cic.term) Hashtbl.t * (Cic.id, Cic.id option) Hashtbl.t * - (string, Cic.hypothesis) Hashtbl.t) + (string, Cic.hypothesis) Hashtbl.t * + (Cic.id, string) Hashtbl.t)) + type mml_of_cic_object = - explode_all:bool -> UriManager.uri -> - Cic.annobj -> - (string, string) Hashtbl.t -> - (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document + Cic.obj -> + Gdome.document * + (Cic.annobj * + ((Cic.id, Cic.term) Hashtbl.t * + (Cic.id, Cic.id option) Hashtbl.t * + (Cic.id, Cic.conjecture) Hashtbl.t * + (Cic.id, Cic.hypothesis) Hashtbl.t * + (Cic.id, string) Hashtbl.t * + (Cic.id, Cic2acic.anntypes) Hashtbl.t)) (** A widget to render sequents **) diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 03803c2b9..1086d5a66 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -105,8 +105,8 @@ class proof_viewer obj = method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) = let uri = unopt_uri uri_opt in let obj = cicCurrentProof proof in - let (mathml, (ids_to_terms, ids_to_father_ids, ids_to_conjectures, - ids_to_hypotheses)) = + let (mathml, (_,(ids_to_terms, ids_to_father_ids, ids_to_conjectures, + ids_to_hypotheses,_,_))) = ApplyTransformation.mml_of_cic_object uri obj in current_infos <- Some (ids_to_terms, ids_to_father_ids, @@ -176,7 +176,7 @@ class sequent_viewer obj = in *) let sequent = CicUtil.lookup_meta metano metasenv in - let (mathml, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses)) = + let (mathml,(_,(ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_))) = ApplyTransformation.mml_of_cic_sequent metasenv sequent in current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);