termEditor.cmi: disambiguatingParser.cmi
+texTermEditor.cmi: oldDisambiguate.cmi
invokeTactics.cmi: termEditor.cmi termViewer.cmi
hbugs.cmi: invokeTactics.cmi
chosenTermEditor.cmi: disambiguatingParser.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
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
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
+include TermEditor
(*
-module ChosenTermEditor = TexTermEditor;;
+include TexTermEditor
*)
-module ChosenTermEditor = TermEditor;;
-
-module Make = ChosenTermEditor.Make;;
-class type term_editor = ChosenTermEditor.term_editor;;
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
+*)
(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
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
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
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
) 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
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 ->
?width:int ->
?height:int ->
?isnotempty_callback:(bool -> unit) ->
- ?share_id_to_uris_with:term_editor ->
+ ?share_environment_with:term_editor ->
unit -> term_editor
end
projects / helm.git / commitdiff