+termEditor.cmi: disambiguatingParser.cmi
invokeTactics.cmi: termEditor.cmi termViewer.cmi
hbugs.cmi: invokeTactics.cmi
+chosenTermEditor.cmi: disambiguatingParser.cmi
proofEngine.cmo: proofEngine.cmi
proofEngine.cmx: proofEngine.cmi
logicalOperations.cmo: proofEngine.cmi logicalOperations.cmi
logicalOperations.cmx: proofEngine.cmx logicalOperations.cmi
-termEditor.cmo: termEditor.cmi
-termEditor.cmx: termEditor.cmi
+oldDisambiguate.cmo: oldDisambiguate.cmi
+oldDisambiguate.cmx: oldDisambiguate.cmi
+disambiguatingParser.cmo: disambiguatingParser.cmi
+disambiguatingParser.cmx: disambiguatingParser.cmi
+termEditor.cmo: disambiguatingParser.cmi termEditor.cmi
+termEditor.cmx: disambiguatingParser.cmx termEditor.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
-gTopLevel.cmo: chosenTransformer.cmi hbugs.cmi invokeTactics.cmi \
+chosenTermEditor.cmo: termEditor.cmi chosenTermEditor.cmi
+chosenTermEditor.cmx: termEditor.cmx chosenTermEditor.cmi
+gTopLevel.cmo: chosenTermEditor.cmi chosenTransformer.cmi \
+ disambiguatingParser.cmi hbugs.cmi invokeTactics.cmi \
logicalOperations.cmi proofEngine.cmi termEditor.cmi termViewer.cmi
-gTopLevel.cmx: chosenTransformer.cmx hbugs.cmx invokeTactics.cmx \
+gTopLevel.cmx: chosenTermEditor.cmx chosenTransformer.cmx \
+ disambiguatingParser.cmx hbugs.cmx invokeTactics.cmx \
logicalOperations.cmx proofEngine.cmx termEditor.cmx termViewer.cmx
BIN_DIR = /usr/local/bin
REQUIRES = lablgtkmathview helm-cic_textual_parser helm-tex_cic_textual_parser \
- helm-cic_proof_checking helm-xml gdome2-xslt helm-cic_unification \
- helm-mathql helm-mathql_interpreter helm-mathql_generator \
- helm-tactics threads hbugs-client mathml-editor \
- helm-cic_transformations helm-logger helm-cic_textual_parser2
+ gdome2-xslt helm-mathql_interpreter helm-mathql_generator \
+ helm-tactics hbugs-client mathml-editor helm-cic_transformations \
+ helm-cic_textual_parser2
PREDICATES = "gnome,init,glade"
OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o
OCAMLFIND = ocamlfind
$(MAKE) -C ../hbugs/ stop
INTERFACE_FILES = \
- proofEngine.mli logicalOperations.mli \
- termEditor.mli xmlDiff.mli chosenTransformer.mli termViewer.mli \
- invokeTactics.mli hbugs.mli
+ proofEngine.mli logicalOperations.mli oldDisambiguate.mli \
+ disambiguatingParser.mli termEditor.mli xmlDiff.mli chosenTransformer.mli \
+ termViewer.mli invokeTactics.mli hbugs.mli chosenTermEditor.mli
+# texTermEditor.mli
DEPOBJS = $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) gTopLevel.ml
--- /dev/null
+(*
+module ChosenTermEditor = TexTermEditor;;
+*)
+module ChosenTermEditor = TermEditor;;
+
+module Make = ChosenTermEditor.Make;;
+class type term_editor = ChosenTermEditor.term_editor;;
--- /dev/null
+class type term_editor =
+ object
+ method coerce : GObj.widget
+ method get_as_string : string
+ method get_metasenv_and_term :
+ context:Cic.context ->
+ metasenv:Cic.metasenv -> Cic.metasenv * Cic.term
+ method environment : DisambiguatingParser.Environment.t ref
+ method reset : unit
+ method set_term : string -> unit
+ end
+
+module Make :
+ functor (C : Disambiguate_types.Callbacks) ->
+ sig
+ val term_editor :
+ MQIConn.handle ->
+ ?packing:(GObj.widget -> unit) ->
+ ?width:int ->
+ ?height:int ->
+ ?isnotempty_callback:(bool -> unit) ->
+ ?share_environment_with:term_editor -> unit -> term_editor
+ end
--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+exception NoWellTypedInterpretation
+
+module Environment =
+ struct
+ type t = Disambiguate_types.environment
+
+ let empty = Disambiguate_types.Environment.empty
+
+ let to_string env =
+prerr_endline "TODO: implement and move away" ;
+ Disambiguate_types.Environment.fold
+ (fun i v s ->
+ match i with
+ | Disambiguate_types.Id id ->s ^ Printf.sprintf "alias %s %s\n" id (fst v)
+ | _ -> "")
+ env ""
+
+ 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 = Disambiguate_types.Id (Str.matched_group 2 inputtext) in
+ let uri = "cic:" ^ (Str.matched_group 5 inputtext) in
+ let resolve_id = aux (n' + 1) in
+ if Disambiguate_types.Environment.mem id resolve_id then
+ resolve_id
+ else
+ let term = Disambiguate.term_of_uri uri in
+ (Disambiguate_types.Environment.add id (uri, (fun _ _ _ -> term))
+ resolve_id)
+ with
+ Not_found -> Disambiguate_types.Environment.empty
+ in
+ aux 0
+ end
+;;
+
+module Make (C : Disambiguate_types.Callbacks) =
+ struct
+ let disambiguate_term mqi_handle context metasenv term_as_string environment =
+ let module Disambiguate' = Disambiguate.Make (C) in
+ let term = Parser.parse_term (Stream.of_string term_as_string) in
+ Disambiguate'.disambiguate_term
+ mqi_handle context metasenv term environment
+ end
+;;
--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+exception NoWellTypedInterpretation
+
+module Environment :
+ sig
+ type t
+ val empty : t
+ val to_string : t -> string
+ val of_string : string -> t
+ end
+
+module Make (C : Disambiguate_types.Callbacks) :
+ sig
+ val disambiguate_term :
+ MQIConn.handle ->
+ Cic.context ->
+ Cic.metasenv ->
+ string ->
+ Environment.t -> (* previous interpretation status *)
+ Environment.t * (* new interpretation status *)
+ Cic.metasenv * (* new metasenv *)
+ Cic.term (* disambiguated term *)
+ end
+
let edit_aliases () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let id_to_uris = inputt#id_to_uris in
+ let id_to_uris = inputt#environment in
let chosen = ref false in
let window =
GWindow.window
ignore (cancelb#connect#clicked window#destroy) ;
ignore
(okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
- let resolve_id = !id_to_uris in
ignore
(input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0)
- (Disambiguate_types.Environment.fold
- (fun i v s ->
- match i with
- | Disambiguate_types.Id id -> s ^ sprintf "alias %s %s\n" id (fst v)
- | _ -> "")
- resolve_id "")) ;
-(*
- (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)
- )
-*)
+ (DisambiguatingParser.Environment.to_string !id_to_uris)) ;
window#show () ;
GtkThread.main ();
if !chosen then
- let resolve_id =
- let inputtext = input#buffer#get_text () in
- 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 = Disambiguate_types.Id (Str.matched_group 2 inputtext) in
- let uri = "cic:" ^ (Str.matched_group 5 inputtext) in
- let resolve_id = aux (n' + 1) in
- if Disambiguate_types.Environment.mem id resolve_id then
- resolve_id
- else
- let term = Disambiguate.term_of_uri uri in
- (Disambiguate_types.Environment.add id (uri, (fun _ _ _ -> term))
- resolve_id)
- with
- Not_found -> TermEditor.empty_id_to_uris
- in
- aux 0
- in
- id_to_uris := resolve_id
+ id_to_uris :=
+ DisambiguatingParser.Environment.of_string (input#buffer#get_text ())
;;
let proveit () =
(* A WIDGET TO ENTER CIC TERMS *)
-(*
-module ChosenTermEditor = TexTermEditor;;
-module ChosenTextualParser0 = TexCicTextualParser0;;
-*)
-module ChosenTermEditor = TermEditor;;
-module ChosenTextualParser0 = CicTextualParser0;;
-
module Callbacks =
struct
- let get_metasenv () = !ChosenTextualParser0.metasenv
- let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv
-
let output_html ?append_NL = output_html ?append_NL (outputhtml ())
let interactive_user_uri_choice =
fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
TexTermEditor'.term_editor
mqi_handle
~width:400 ~height:20 ~packing:scrolled_window#add
- ~share_id_to_uris_with:inputt ()
+ ~share_environment_with:inputt ()
~isnotempty_callback:
(function b ->
(*non_empty_type := b ;*)
TexTermEditor'.term_editor
mqi_handle
~width:400 ~height:20 ~packing:scrolled_window#add
- ~share_id_to_uris_with:inputt ()
+ ~share_environment_with:inputt ()
~isnotempty_callback:
(function b ->
(* (*non_empty_type := b ;*)
TexTermEditor'.term_editor
mqi_handle
~width:400 ~height:100 ~packing:scrolled_window#add
- ~share_id_to_uris_with:inputt ()
+ ~share_environment_with:inputt ()
~isnotempty_callback:
(function b ->
non_empty_type := b ;
okb#misc#set_sensitive (b && uri_entry#text <> ""))
in
let _ =
-let xxx = inputt#get_as_string in
- newinputt#set_term xxx ;
-(*
- newinputt#set_term inputt#get_as_string ;
-*)
+ newinputt#set_term inputt#get_as_string ;
inputt#reset in
let _ =
uri_entry#connect#changed
--- /dev/null
+(* Copyright (C) 2000-2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 06/01/2002 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+open Printf
+
+(** This module provides a functor to disambiguate the input **)
+(** given a set of user-interface call-backs **)
+
+module type Callbacks =
+ sig
+ val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit
+ val interactive_user_uri_choice :
+ selection_mode:[`SINGLE | `MULTIPLE] ->
+ ?ok:string ->
+ ?enable_button_for_non_vars:bool ->
+ title:string -> msg:string -> id:string -> string list -> string list
+ val interactive_interpretation_choice :
+ (string * string) list list -> int
+ val input_or_locate_uri : title:string -> UriManager.uri
+ end
+;;
+
+type domain_and_interpretation =
+ CicTextualParser0.interpretation_domain_item list *
+ CicTextualParser0.interpretation
+;;
+
+module Make(C:Callbacks) =
+ struct
+
+ let locate_one_id mqi_handle id =
+ let query = MQueryGenerator.locate id in
+ let result = MQueryInterpreter.execute mqi_handle query in
+ let uris =
+ List.map
+ (function uri,_ ->
+ MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
+ ) result in
+ C.output_html (`Msg (`T "Locate query:"));
+ MQueryUtil.text_of_query
+ (fun s -> C.output_html ~append_NL:false (`Msg (`T s)))
+ "" query;
+ C.output_html (`Msg (`T "Result:"));
+ MQueryUtil.text_of_result (fun s -> C.output_html (`Msg (`T s))) "" result;
+ let uris' =
+ match uris with
+ [] ->
+ [UriManager.string_of_uri
+ (C.input_or_locate_uri
+ ~title:("URI matching \"" ^ id ^ "\" unknown."))]
+ | [uri] -> [uri]
+ | _ ->
+ C.interactive_user_uri_choice
+ ~selection_mode:`MULTIPLE
+ ~ok:"Try every selection."
+ ~enable_button_for_non_vars:true
+ ~title:"Ambiguous input."
+ ~msg:
+ ("Ambiguous input \"" ^ id ^
+ "\". Please, choose one or more interpretations:")
+ ~id
+ uris
+ in
+ List.map MQueryMisc.cic_textual_parser_uri_of_string uris'
+
+
+ exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
+
+ type test_result =
+ Ok of Cic.term * Cic.metasenv
+ | Ko
+ | Uncertain
+
+ type ambiguous_choices =
+ Uris of CicTextualParser0.uri list
+ | Symbols of (CicTextualParser0.interpretation -> Cic.term) list
+
+ let disambiguate_input mqi_handle context metasenv dom mk_metasenv_and_expr ~id_to_uris=
+ let known_ids,resolve_id = id_to_uris in
+ let dom' =
+ let rec filter =
+ function
+ [] -> []
+ | he::tl ->
+ if List.mem he known_ids then filter tl else he::(filter tl)
+ in
+ filter dom
+ in
+ (* for each id in dom' we get the list of uris associated to it *)
+ let list_of_uris =
+ List.map
+ (function
+ CicTextualParser0.Id id -> Uris (locate_one_id mqi_handle id)
+ | CicTextualParser0.Symbol (descr,choices) ->
+ (* CSC: Implementare la funzione di filtraggio manuale *)
+ (* CSC: corrispondente alla locate_one_id *)
+ Symbols (List.map snd choices)
+ ) dom' in
+ let tests_no =
+ List.fold_left
+ (fun i uris ->
+ let len =
+ match uris with
+ Uris l -> List.length l
+ | Symbols l -> List.length l
+ in
+ i * len
+ ) 1 list_of_uris
+ in
+ if tests_no > 1 then
+ C.output_html (`Msg (`T (sprintf
+ "Disambiguation phase started: up to %d cases will be tried"
+ tests_no)));
+ (* and now we compute the list of all possible assignments from *)
+ (* id to uris that generate well-typed terms *)
+ let resolve_ids =
+ (* function to test if a partial interpretation is so far correct *)
+ let test resolve_id residual_dom =
+ (* We put implicits in place of every identifier that is not *)
+ (* resolved by resolve_id *)
+ let resolve_id' =
+ List.fold_left
+ (fun f id ->
+ function id' ->
+ if id = id' then Some (CicTextualParser0.Implicit) else f id'
+ ) resolve_id residual_dom
+ in
+ (* and we try to refine the term *)
+ let metasenv',expr = mk_metasenv_and_expr resolve_id' in
+(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
+ try
+ let term,_,_,metasenv'' =
+ CicRefine.type_of_aux' metasenv' context expr
+ in
+ Ok (term,metasenv'')
+ with
+ CicRefine.MutCaseFixAndCofixRefineNotImplemented ->
+ (try
+ let term = CicTypeChecker.type_of_aux' metasenv' context expr in
+ Ok (term,metasenv')
+ with _ -> Ko
+ )
+ | CicRefine.Uncertain _ ->
+prerr_endline ("%%% UNCERTAIN!!! " ^ CicPp.ppterm expr) ;
+ Uncertain
+ | _ ->
+prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ;
+ Ko
+ in
+ let rec aux resolve_id ids list_of_uris =
+ match ids,list_of_uris with
+ [],[] ->
+ (match test resolve_id [] with
+ Ok (term,metasenv) -> [resolve_id,term,metasenv]
+ | Ko | Uncertain -> [])
+ | id::idtl,uris::uristl ->
+ let rec filter =
+ function
+ [] -> []
+ | (uri : CicTextualParser0.interpretation_codomain_item)::uritl ->
+ let resolve_id' =
+ function id' -> if id = id' then Some uri else resolve_id id'
+ in
+ (match test resolve_id' idtl with
+ Ok (term,metasenv) ->
+ (* the next three ``if''s are used to avoid the base *)
+ (* case where the term would be refined a second time. *)
+ (if uristl = [] then
+ [resolve_id',term,metasenv]
+ else
+ (aux resolve_id' idtl uristl)
+ ) @ (filter uritl)
+ | Uncertain ->
+ (if uristl = [] then []
+ else
+ (aux resolve_id' idtl uristl)
+ ) @ (filter uritl)
+ | Ko ->
+ filter uritl
+ )
+ in
+ (match uris with
+ Uris uris ->
+ filter
+ (List.map (function uri -> CicTextualParser0.Uri uri) uris)
+ | Symbols symbols ->
+ filter
+ (List.map
+ (function sym -> CicTextualParser0.Term sym) symbols))
+ | _,_ -> assert false
+ in
+ aux resolve_id dom' list_of_uris
+ in
+ List.iter
+ (function (resolve,term,newmetasenv) ->
+ (* If metasen <> newmetasenv is a normal condition, we should *)
+ (* be prepared to apply the returned substitution to the *)
+ (* whole current proof. *)
+ if metasenv <> newmetasenv then
+ begin
+ prerr_endline
+ (Printf.sprintf
+ "+++++ ASSERTION FAILED: a refine operation should not modify the metasenv. Old metasenv:\n %s\n New metasenv:\n %s\n"
+ (CicMetaSubst.ppmetasenv [] metasenv)
+ (CicMetaSubst.ppmetasenv [] newmetasenv)) ;
+ (* an assert would raise an exception that could be caught *)
+ exit 1
+ end
+ ) resolve_ids ;
+ let resolve_id',term,metasenv' =
+ match resolve_ids with
+ [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
+ | [resolve_id] -> resolve_id
+ | _ ->
+ let choices =
+ List.map
+ (function (resolve,_,_) ->
+ List.map
+ (function id ->
+ (match id with
+ CicTextualParser0.Id id -> id
+ | CicTextualParser0.Symbol (descr,_) -> descr
+ ),
+ match resolve id with
+ None -> assert false
+ | Some (CicTextualParser0.Uri uri) ->
+ (match uri with
+ CicTextualParser0.ConUri uri
+ | CicTextualParser0.VarUri uri ->
+ UriManager.string_of_uri uri
+ | CicTextualParser0.IndTyUri (uri,tyno) ->
+ UriManager.string_of_uri uri ^ "#xpointer(1/" ^
+ string_of_int (tyno+1) ^ ")"
+ | CicTextualParser0.IndConUri (uri,tyno,consno) ->
+ UriManager.string_of_uri uri ^ "#xpointer(1/" ^
+ string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")")
+ | Some (CicTextualParser0.Term term) ->
+ (* CSC: Implementare resa delle scelte *)
+ "To be implemented XXX01"
+ | Some CicTextualParser0.Implicit -> assert false
+ ) dom
+ ) resolve_ids
+ in
+ let index = C.interactive_interpretation_choice choices in
+ List.nth resolve_ids index
+ in
+ (known_ids @ dom', resolve_id'), metasenv',term
+end
+;;
--- /dev/null
+(* Copyright (C) 2000-2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 15/01/2003 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+(** This module provides a functor to disambiguate the input **)
+(** given a set of user-interface call-backs **)
+
+module type Callbacks =
+ sig
+ val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit
+ val interactive_user_uri_choice :
+ selection_mode:[`SINGLE | `MULTIPLE] ->
+ ?ok:string ->
+ ?enable_button_for_non_vars:bool ->
+ title:string -> msg:string -> id:string -> string list -> string list
+ val interactive_interpretation_choice :
+ (string * string) list list -> int
+ val input_or_locate_uri : title:string -> UriManager.uri
+ end
+
+type domain_and_interpretation =
+ CicTextualParser0.interpretation_domain_item list *
+ CicTextualParser0.interpretation
+
+module Make (C : Callbacks) :
+ sig
+ exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
+ val disambiguate_input :
+ MQIConn.handle ->
+ Cic.context ->
+ Cic.metasenv ->
+ CicTextualParser0.interpretation_domain_item list ->
+ (CicTextualParser0.interpretation -> Cic.metasenv * Cic.term) ->
+ id_to_uris:domain_and_interpretation ->
+ domain_and_interpretation * Cic.metasenv * Cic.term
+ end
open Printf
-open Disambiguate_types
-
(* A WIDGET TO ENTER CIC TERMS *)
class type term_editor =
method reset : unit
(* The input of set_term is unquoted *)
method set_term : string -> unit
- method id_to_uris : environment ref
+ method environment : DisambiguatingParser.Environment.t ref
end
-let empty_id_to_uris = Environment.empty
-
-module Make(C: Callbacks) =
+module Make(C:Disambiguate_types.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 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.Environment.empty
+ | Some obj -> obj#environment
in
let input = GText.view ~editable:true ?width ?height ?packing () in
let _ =
| None -> None
) context
in
- let term =
- Parser.parse_term (Stream.of_string (input#buffer#get_text ()))
- in
- let id_to_uris',metasenv,expr =
- Disambiguate'.disambiguate_term mqi_handle context metasenv term
- ~aliases:!id_to_uris
+ let environment',metasenv,expr =
+ Disambiguate'.disambiguate_term mqi_handle context metasenv
+ (input#buffer#get_text ()) !environment
in
- id_to_uris := id_to_uris';
+ environment := environment';
(metasenv, expr)
- method id_to_uris = id_to_uris
+ method environment = environment
end
let term_editor = new term_editor_impl
metasenv:Cic.metasenv -> Cic.metasenv * Cic.term
method reset : unit
method set_term : string -> unit
- method id_to_uris : Disambiguate_types.environment ref
+ method environment : DisambiguatingParser.Environment.t ref
end
-val empty_id_to_uris : Disambiguate_types.environment
-
-module Make (C : Callbacks) :
+module Make (C : Disambiguate_types.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