From: Claudio Sacerdoti Coen Date: Fri, 23 Jan 2004 17:45:29 +0000 (+0000) Subject: Eureka! X-Git-Tag: V_0_2_3~155 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=63f211d673ba5a9eb05b0bdad2585e2b251f2baa;p=helm.git Eureka! It is now possible to choose independently: - the widget for the term editor - the disambiguating parser, i.e. * the parsing component * the disambiguating component --- diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 9ff1f45de..8bfe05a39 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -1,4 +1,5 @@ termEditor.cmi: disambiguatingParser.cmi +texTermEditor.cmi: oldDisambiguate.cmi invokeTactics.cmi: termEditor.cmi termViewer.cmi hbugs.cmi: invokeTactics.cmi chosenTermEditor.cmi: disambiguatingParser.cmi @@ -8,10 +9,12 @@ logicalOperations.cmo: proofEngine.cmi logicalOperations.cmi logicalOperations.cmx: proofEngine.cmx logicalOperations.cmi oldDisambiguate.cmo: oldDisambiguate.cmi oldDisambiguate.cmx: oldDisambiguate.cmi -disambiguatingParser.cmo: disambiguatingParser.cmi -disambiguatingParser.cmx: disambiguatingParser.cmi +disambiguatingParser.cmo: oldDisambiguate.cmi disambiguatingParser.cmi +disambiguatingParser.cmx: oldDisambiguate.cmx disambiguatingParser.cmi termEditor.cmo: disambiguatingParser.cmi termEditor.cmi termEditor.cmx: disambiguatingParser.cmx termEditor.cmi +texTermEditor.cmo: oldDisambiguate.cmi texTermEditor.cmi +texTermEditor.cmx: oldDisambiguate.cmx texTermEditor.cmi xmlDiff.cmo: xmlDiff.cmi xmlDiff.cmx: xmlDiff.cmi chosenTransformer.cmo: chosenTransformer.cmi @@ -26,8 +29,8 @@ invokeTactics.cmx: logicalOperations.cmx proofEngine.cmx termEditor.cmx \ termViewer.cmx invokeTactics.cmi hbugs.cmo: invokeTactics.cmi proofEngine.cmi hbugs.cmi hbugs.cmx: invokeTactics.cmx proofEngine.cmx hbugs.cmi -chosenTermEditor.cmo: termEditor.cmi chosenTermEditor.cmi -chosenTermEditor.cmx: termEditor.cmx chosenTermEditor.cmi +chosenTermEditor.cmo: texTermEditor.cmi chosenTermEditor.cmi +chosenTermEditor.cmx: texTermEditor.cmx chosenTermEditor.cmi gTopLevel.cmo: chosenTermEditor.cmi chosenTransformer.cmi \ disambiguatingParser.cmi hbugs.cmi invokeTactics.cmi \ logicalOperations.cmi proofEngine.cmi termEditor.cmi termViewer.cmi diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index bcf0b74ff..3904c6d22 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -23,9 +23,9 @@ stop: INTERFACE_FILES = \ proofEngine.mli logicalOperations.mli oldDisambiguate.mli \ - disambiguatingParser.mli termEditor.mli xmlDiff.mli chosenTransformer.mli \ - termViewer.mli invokeTactics.mli hbugs.mli chosenTermEditor.mli -# texTermEditor.mli + disambiguatingParser.mli termEditor.mli texTermEditor.mli xmlDiff.mli \ + chosenTransformer.mli termViewer.mli invokeTactics.mli hbugs.mli \ + chosenTermEditor.mli DEPOBJS = $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) gTopLevel.ml diff --git a/helm/gTopLevel/chosenTermEditor.ml b/helm/gTopLevel/chosenTermEditor.ml index f6a7b0380..25dcfd2e5 100644 --- a/helm/gTopLevel/chosenTermEditor.ml +++ b/helm/gTopLevel/chosenTermEditor.ml @@ -1,7 +1,4 @@ +include TermEditor (* -module ChosenTermEditor = TexTermEditor;; +include TexTermEditor *) -module ChosenTermEditor = TermEditor;; - -module Make = ChosenTermEditor.Make;; -class type term_editor = ChosenTermEditor.term_editor;; diff --git a/helm/gTopLevel/disambiguatingParser.ml b/helm/gTopLevel/disambiguatingParser.ml index 580e09bb2..eb89b1170 100644 --- a/helm/gTopLevel/disambiguatingParser.ml +++ b/helm/gTopLevel/disambiguatingParser.ml @@ -25,14 +25,81 @@ exception NoWellTypedInterpretation -module EnvironmentP3 = DisambiguateTypes.EnvironmentP3 +module AndreaAndZackDisambiguatingParser = + struct + module EnvironmentP3 = DisambiguateTypes.EnvironmentP3 + + module Make (C : DisambiguateTypes.Callbacks) = + struct + let + disambiguate_term mqi_handle context metasenv term_as_string environment + = + let module Disambiguate' = Disambiguate.Make (C) in + let term = + CicTextualParser2.parse_term (Stream.of_string term_as_string) + in + Disambiguate'.disambiguate_term + mqi_handle context metasenv term environment + end + end + + +module CSCTextualDisambiguatingParser = + struct + module EnvironmentP3 = OldDisambiguate.EnvironmentP3 + + module Make (C : DisambiguateTypes.Callbacks) = + struct + let + disambiguate_term mqi_handle context metasenv term_as_string environment + = + let module Disambiguate' = OldDisambiguate.Make (C) in + let name_context = + List.map + (function + Some (n,_) -> Some n + | None -> None + ) context + in + let lexbuf = Lexing.from_string term_as_string in + let dom,mk_metasenv_and_expr = + CicTextualParserContext.main + ~context:name_context ~metasenv CicTextualLexer.token lexbuf + in + Disambiguate'.disambiguate_input mqi_handle + context metasenv dom mk_metasenv_and_expr environment + end + end -module Make (C : DisambiguateTypes.Callbacks) = +module CSCTexDisambiguatingParser = struct - let disambiguate_term mqi_handle context metasenv term_as_string environment = - let module Disambiguate' = Disambiguate.Make (C) in - let term = CicTextualParser2.parse_term (Stream.of_string term_as_string) in - Disambiguate'.disambiguate_term - mqi_handle context metasenv term environment + module EnvironmentP3 = OldDisambiguate.EnvironmentP3 + + module Make (C : DisambiguateTypes.Callbacks) = + struct + let + disambiguate_term mqi_handle context metasenv term_as_string environment + = + let module Disambiguate' = OldDisambiguate.Make (C) in + let name_context = + List.map + (function + Some (n,_) -> Some n + | None -> None + ) context + in + let lexbuf = Lexing.from_string term_as_string in + let dom,mk_metasenv_and_expr = + TexCicTextualParserContext.main + ~context:name_context ~metasenv TexCicTextualLexer.token lexbuf + in + Disambiguate'.disambiguate_input mqi_handle + context metasenv dom mk_metasenv_and_expr environment + end end -;; + +include AndreaAndZackDisambiguatingParser +(* +include CSCTextualDisambiguatingParser +include CSCTexDisambiguatingParser +*) diff --git a/helm/gTopLevel/oldDisambiguate.ml b/helm/gTopLevel/oldDisambiguate.ml index 6338690bc..8d6ef6295 100644 --- a/helm/gTopLevel/oldDisambiguate.ml +++ b/helm/gTopLevel/oldDisambiguate.ml @@ -279,3 +279,79 @@ prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ; (known_ids @ dom', resolve_id'), metasenv',term end ;; + +module EnvironmentP3 = + struct + type t = domain_and_interpretation + + let empty = "" + + let to_string (dom,resolve_id) = + let string_of_cic_textual_parser_uri uri = + let module C = Cic in + let module CTP = CicTextualParser0 in + let uri' = + match uri with + CTP.ConUri uri -> UriManager.string_of_uri uri + | CTP.VarUri uri -> UriManager.string_of_uri uri + | CTP.IndTyUri (uri,tyno) -> + UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) + | CTP.IndConUri (uri,tyno,consno) -> + UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^ + string_of_int consno + in + (* 4 = String.length "cic:" *) + String.sub uri' 4 (String.length uri' - 4) + in + String.concat "\n" + (List.map + (function v -> + let uri = + match resolve_id v with + None -> assert false + | Some (CicTextualParser0.Uri uri) -> uri + | Some (CicTextualParser0.Term _) + | Some CicTextualParser0.Implicit -> assert false + in + "alias " ^ + (match v with + CicTextualParser0.Id id -> id + | CicTextualParser0.Symbol (descr,_) -> + (* CSC: To be implemented *) + assert false + )^ " " ^ (string_of_cic_textual_parser_uri uri) + ) dom) + + let of_string inputtext = + let regexpr = + let alfa = "[a-zA-Z_-]" in + let digit = "[0-9]" in + let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in + let blanks = "\( \|\t\|\n\)+" in + let nonblanks = "[^ \t\n]+" in + let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *) + Str.regexp + ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)") + in + let rec aux n = + try + let n' = Str.search_forward regexpr inputtext n in + let id = CicTextualParser0.Id (Str.matched_group 2 inputtext) in + let uri = + MQueryMisc.cic_textual_parser_uri_of_string + ("cic:" ^ (Str.matched_group 5 inputtext)) + in + let dom,resolve_id = aux (n' + 1) in + if List.mem id dom then + dom,resolve_id + else + id::dom, + (function id' -> + if id = id' then + Some (CicTextualParser0.Uri uri) + else resolve_id id') + with + Not_found -> ([],function _ -> None) + in + aux 0 + end diff --git a/helm/gTopLevel/oldDisambiguate.mli b/helm/gTopLevel/oldDisambiguate.mli index 242b3102a..372f50085 100644 --- a/helm/gTopLevel/oldDisambiguate.mli +++ b/helm/gTopLevel/oldDisambiguate.mli @@ -65,3 +65,11 @@ module Make (C : Callbacks) : id_to_uris:domain_and_interpretation -> domain_and_interpretation * Cic.metasenv * Cic.term end + +module EnvironmentP3 : + sig + type t = domain_and_interpretation + val empty : string + val to_string : t -> string + val of_string : string -> t + end diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml index c89fe04b2..b89974d71 100644 --- a/helm/gTopLevel/texTermEditor.ml +++ b/helm/gTopLevel/texTermEditor.ml @@ -46,21 +46,19 @@ class type term_editor = method reset : unit (* The input of set_term is unquoted *) method set_term : string -> unit - method id_to_uris : Disambiguate.domain_and_interpretation ref + method environment : DisambiguatingParser.EnvironmentP3.t ref end ;; -let empty_id_to_uris = ([],function _ -> None);; - -module Make(C:Disambiguate.Callbacks) = +module Make(C:DisambiguateTypes.Callbacks) = struct - module Disambiguate' = Disambiguate.Make(C);; + module Disambiguate' = DisambiguatingParser.Make(C);; class term_editor_impl mqi_handle ?packing ?width ?height - ?isnotempty_callback ?share_id_to_uris_with () : term_editor + ?isnotempty_callback ?share_environment_with () : term_editor = let mmlwidget = GMathViewAux.single_selection_math_view @@ -131,10 +129,13 @@ module Make(C:Disambiguate.Callbacks) = mmlwidget#thaw ; adj#set_value adj#upper ; false) in - let id_to_uris = - match share_id_to_uris_with with - None -> ref empty_id_to_uris - | Some obj -> obj#id_to_uris + let environment = + match share_environment_with with + None -> + ref + (DisambiguatingParser.EnvironmentP3.of_string + DisambiguatingParser.EnvironmentP3.empty) + | Some obj -> obj#environment in let _ = match isnotempty_callback with @@ -206,18 +207,14 @@ module Make(C:Disambiguate.Callbacks) = ) context in prerr_endline ("###CSC: " ^ (Mathml_editor.get_tex tex_editor)) ; - let lexbuf = Lexing.from_string (Mathml_editor.get_tex tex_editor) in - let dom,mk_metasenv_and_expr = - TexCicTextualParserContext.main - ~context:name_context ~metasenv TexCicTextualLexer.token lexbuf - in - let id_to_uris',metasenv,expr = - Disambiguate'.disambiguate_input mqi_handle - context metasenv dom mk_metasenv_and_expr ~id_to_uris:!id_to_uris - in - id_to_uris := id_to_uris' ; - metasenv,expr - method id_to_uris = id_to_uris + let environment',metasenv,expr = + Disambiguate'.disambiguate_term mqi_handle + context metasenv (Mathml_editor.get_tex tex_editor) !environment + in + environment := environment' ; + metasenv,expr + + method environment = environment end let term_editor = new term_editor_impl diff --git a/helm/gTopLevel/texTermEditor.mli b/helm/gTopLevel/texTermEditor.mli index beb21ec85..8b040c983 100644 --- a/helm/gTopLevel/texTermEditor.mli +++ b/helm/gTopLevel/texTermEditor.mli @@ -34,12 +34,10 @@ class type term_editor = method reset : unit (* The input of set_term is unquoted *) method set_term : string -> unit - method id_to_uris : Disambiguate.domain_and_interpretation ref + method environment : DisambiguatingParser.EnvironmentP3.t ref end -val empty_id_to_uris : Disambiguate.domain_and_interpretation - -module Make (C : Disambiguate.Callbacks) : +module Make (C : DisambiguateTypes.Callbacks) : sig val term_editor : MQIConn.handle -> @@ -47,6 +45,6 @@ module Make (C : Disambiguate.Callbacks) : ?width:int -> ?height:int -> ?isnotempty_callback:(bool -> unit) -> - ?share_id_to_uris_with:term_editor -> + ?share_environment_with:term_editor -> unit -> term_editor end