mQueryLevels2.cmx: mQueryLevels2.cmi
mQueryGenerator.cmo: mQueryGenerator.cmi
mQueryGenerator.cmx: mQueryGenerator.cmi
-gTopLevel.cmo: cic2Xml.cmi cic2acic.cmi logicalOperations.cmi \
- mQueryGenerator.cmi mQueryLevels.cmi mQueryLevels2.cmi proofEngine.cmi \
- sequentPp.cmi xml2Gdome.cmi
-gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx logicalOperations.cmx \
- mQueryGenerator.cmx mQueryLevels.cmx mQueryLevels2.cmx proofEngine.cmx \
- sequentPp.cmx xml2Gdome.cmx
+disambiguate.cmo: mQueryGenerator.cmi disambiguate.cmi
+disambiguate.cmx: mQueryGenerator.cmx disambiguate.cmi
+gTopLevel.cmo: cic2Xml.cmi cic2acic.cmi disambiguate.cmi \
+ logicalOperations.cmi mQueryGenerator.cmi mQueryLevels.cmi \
+ mQueryLevels2.cmi proofEngine.cmi sequentPp.cmi xml2Gdome.cmi
+gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx disambiguate.cmx \
+ logicalOperations.cmx mQueryGenerator.cmx mQueryLevels.cmx \
+ mQueryLevels2.cmx proofEngine.cmx sequentPp.cmx xml2Gdome.cmx
proofEngineReduction.ml proofEngineReduction.mli \
proofEngineStructuralRules.ml proofEngineStructuralRules.mli \
tacticals.ml tacticals.mli reductionTactics.ml reductionTactics.mli \
- primitiveTactics.ml primitiveTactics.mli variousTactics.ml variousTactics.mli \
- introductionTactics.ml introductionTactics.mli eliminationTactics.ml eliminationTactics.mli \
- negationTactics.ml negationTactics.mli equalityTactics.ml equalityTactics.mli \
- ring.ml ring.mli fourier.ml fourierR.ml fourierR.mli\
- proofEngine.ml proofEngine.mli \
- doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \
- cic2acic.mli cic2Xml.ml cic2Xml.mli logicalOperations.ml \
+ primitiveTactics.ml primitiveTactics.mli variousTactics.ml \
+ variousTactics.mli introductionTactics.ml introductionTactics.mli \
+ eliminationTactics.ml eliminationTactics.mli negationTactics.ml \
+ negationTactics.mli equalityTactics.ml equalityTactics.mli ring.ml \
+ ring.mli fourier.ml fourierR.ml fourierR.mli proofEngine.ml \
+ proofEngine.mli doubleTypeInference.ml doubleTypeInference.mli \
+ cic2acic.ml cic2acic.mli cic2Xml.ml cic2Xml.mli logicalOperations.ml \
logicalOperations.mli sequentPp.ml sequentPp.mli mQueryGenerator.mli \
- mQueryLevels.ml mQueryLevels2.mli mQueryLevels2.ml mQueryGenerator.ml gTopLevel.ml
+ mQueryLevels.ml mQueryLevels2.mli mQueryLevels2.ml mQueryGenerator.ml\
+ disambiguate.ml disambiguate.mli gTopLevel.ml
TOPLEVELOBJS = xml2Gdome.cmo proofEngineTypes.cmo proofEngineHelpers.cmo \
proofEngineReduction.cmo proofEngineStructuralRules.cmo \
tacticals.cmo reductionTactics.cmo primitiveTactics.cmo \
- variousTactics.cmo introductionTactics.cmo eliminationTactics.cmo \
- negationTactics.cmo equalityTactics.cmo ring.cmo fourier.cmo fourierR.cmo \
- proofEngine.cmo doubleTypeInference.cmo cic2acic.cmo \
- cic2Xml.cmo logicalOperations.cmo sequentPp.cmo \
- mQueryLevels.cmo mQueryLevels2.cmo mQueryGenerator.cmo \
+ variousTactics.cmo introductionTactics.cmo \
+ eliminationTactics.cmo negationTactics.cmo equalityTactics.cmo \
+ ring.cmo fourier.cmo fourierR.cmo proofEngine.cmo \
+ doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \
+ logicalOperations.cmo sequentPp.cmo mQueryLevels.cmo \
+ mQueryLevels2.cmo mQueryGenerator.cmo disambiguate.cmo \
gTopLevel.cmo
depend:
--- /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 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+(** Functions that should be moved in another module **)
+
+exception IllFormedUri of string;;
+
+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)
+;;
+
+let cic_textual_parser_uri_of_string uri' =
+ prerr_endline ("cic_textual_parser_uri_of_string INPUT = " ^ uri');
+ try
+ (* Constant *)
+ if String.sub uri' (String.length uri' - 4) 4 = ".con" then
+ CicTextualParser0.ConUri (UriManager.uri_of_string uri')
+ else
+ if String.sub uri' (String.length uri' - 4) 4 = ".var" then
+ CicTextualParser0.VarUri (UriManager.uri_of_string uri')
+ else
+ (try
+ (* Inductive Type *)
+ let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
+ CicTextualParser0.IndTyUri (uri'',typeno)
+ with
+ _ ->
+ (* Constructor of an Inductive Type *)
+ let uri'',typeno,consno =
+ CicTextualLexer.indconuri_of_uri uri'
+ in
+ CicTextualParser0.IndConUri (uri'',typeno,consno)
+ )
+ with
+ _ -> raise (IllFormedUri uri')
+;;
+let cic_textual_parser_uri_of_string uri' =
+ let res = cic_textual_parser_uri_of_string uri' in
+ prerr_endline ("RESULT: " ^ (string_of_cic_textual_parser_uri res));
+ res
+
+(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
+let wrong_xpointer_format_from_wrong_xpointer_format' uri =
+ try
+ let index_sharp = String.index uri '#' in
+ let index_rest = index_sharp + 10 in
+ let baseuri = String.sub uri 0 index_sharp in
+ let rest =
+ String.sub uri index_rest (String.length uri - index_rest - 1)
+ in
+ baseuri ^ "#" ^ rest
+ with Not_found -> uri
+;;
+
+(* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
+let get_last_query =
+ let query = ref "" in
+ MQueryGenerator.set_confirm_query
+ (function q -> query := MQueryUtil.text_of_query q ; true) ;
+ function result ->
+ !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
+;;
+
+(** This module provides a functor to disambiguate the input **)
+(** given a set of user-interface call-backs **)
+
+module type Callbacks =
+ sig
+ val output_html : string -> unit
+ val interactive_user_uri_choice :
+ selection_mode:[`SINGLE | `EXTENDED] ->
+ ?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 =
+ string list * (string -> CicTextualParser0.uri option)
+;;
+
+module Make(C:Callbacks) =
+ struct
+
+ let locate_one_id id =
+ let result = MQueryGenerator.locate id in
+ let uris =
+ List.map
+ (function uri,_ ->
+ wrong_xpointer_format_from_wrong_xpointer_format' uri
+ ) result in
+ let html=
+ " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>"
+ in
+ C.output_html html ;
+ 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:`EXTENDED
+ ~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 cic_textual_parser_uri_of_string uris'
+
+
+ exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
+
+ type test_result =
+ Ok of Cic.term * Cic.metasenv
+ | Ko
+ | Uncertain
+
+ let disambiguate_input 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 locate_one_id dom' in
+ let tests_no =
+ List.fold_left (fun i uris -> i * List.length uris) 1 list_of_uris
+ in
+ if tests_no > 1 then
+ C.output_html
+ ("<h1>Disambiguation phase started: " ^
+ string_of_int tests_no ^ " cases will be tried.") ;
+ (* 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'' =
+ let resolve_id' =
+ function id ->
+ match resolve_id id with
+ None -> None
+ | Some uri -> Some (CicTextualParser0.Uri uri)
+ in
+ 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 saved_status = !CicTextualParser0.metasenv in
+ let metasenv',expr = mk_metasenv_and_expr resolve_id'' in
+(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
+ (* The parser is imperative ==> we must restore the old status ;-(( *)
+ CicTextualParser0.metasenv := saved_status ;
+ 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::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
+ filter uris
+ | _,_ -> 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
+ ("+++++ ASSERTION FAILED: " ^
+ "a refine operation should not modify the metasenv") ;
+ (* 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 ->
+ id,
+ match resolve id with
+ None -> assert false
+ | Some 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 ^ ")"
+ ) 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 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+(** Functions that should be moved in another module **)
+exception IllFormedUri of string
+val string_of_cic_textual_parser_uri : CicTextualParser0.uri -> string
+val cic_textual_parser_uri_of_string : string -> CicTextualParser0.uri
+
+val wrong_xpointer_format_from_wrong_xpointer_format' : string -> string
+
+(** This module provides a functor to disambiguate the input **)
+(** given a set of user-interface call-backs **)
+
+module type Callbacks =
+ sig
+ val output_html : string -> unit
+ val interactive_user_uri_choice :
+ selection_mode:[`SINGLE | `EXTENDED] ->
+ ?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 =
+ string list * (string -> CicTextualParser0.uri option)
+
+module Make :
+ functor (C : Callbacks) ->
+ sig
+ exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
+ val disambiguate_input :
+ Cic.context ->
+ Cic.metasenv ->
+ string list ->
+ ((string -> CicTextualParser0.interp_codomain option) ->
+ Cic.metasenv * Cic.term) ->
+ id_to_uris:domain_and_interpretation ->
+ domain_and_interpretation * Cic.metasenv * Cic.term
+ end
(******************************************************************************)
-(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
-let wrong_xpointer_format_from_wrong_xpointer_format' uri =
- try
- let index_sharp = String.index uri '#' in
- let index_rest = index_sharp + 10 in
- let baseuri = String.sub uri 0 index_sharp in
- let rest = String.sub uri index_rest (String.length uri - index_rest - 1) in
- baseuri ^ "#" ^ rest
- with Not_found -> uri
-;;
-
(* GLOBAL CONSTANTS *)
let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
(* MISC FUNCTIONS *)
-exception IllFormedUri of string;;
-
-let cic_textual_parser_uri_of_string uri' =
- try
- (* Constant *)
- if String.sub uri' (String.length uri' - 4) 4 = ".con" then
- CicTextualParser0.ConUri (UriManager.uri_of_string uri')
- else
- if String.sub uri' (String.length uri' - 4) 4 = ".var" then
- CicTextualParser0.VarUri (UriManager.uri_of_string uri')
- else
- (try
- (* Inductive Type *)
- let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
- CicTextualParser0.IndTyUri (uri'',typeno)
- with
- _ ->
- (* Constructor of an Inductive Type *)
- let uri'',typeno,consno =
- CicTextualLexer.indconuri_of_uri uri'
- in
- CicTextualParser0.IndConUri (uri'',typeno,consno)
- )
- with
- _ -> raise (IllFormedUri uri')
-;;
-
let term_of_cic_textual_parser_uri uri =
let module C = Cic in
let module CTP = CicTextualParser0 in
~packing:scrolled_window#add ~width:400 ~height:280 () in
let expr =
let term =
- term_of_cic_textual_parser_uri (cic_textual_parser_uri_of_string uri)
+ term_of_cic_textual_parser_uri
+ (Disambiguate.cic_textual_parser_uri_of_string uri)
in
(Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
in
exception NoChoice;;
let
- interactive_user_uri_choice ~selection_mode ?(ok="Ok")
+ interactive_user_uri_choice ~(selection_mode:[`SINGLE|`EXTENDED]) ?(ok="Ok")
?(enable_button_for_non_vars=false) ~title ~msg uris
=
let choices = ref [] in
let expected_height = 18 * List.length uris in
let height = if expected_height > 400 then 400 else expected_height in
GList.clist ~columns:1 ~packing:scrolled_window#add
- ~height ~selection_mode () in
+ ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in
let _ = List.map (function x -> clist#append [x]) uris in
let hbox2 =
GPack.hbox ~border_width:0
let n' = Str.search_forward regexpr inputtext n in
let id = Str.matched_group 2 inputtext in
let uri =
- cic_textual_parser_uri_of_string
+ Disambiguate.cic_textual_parser_uri_of_string
("cic:" ^ (Str.matched_group 5 inputtext))
in
let dom,resolve_id = aux (n' + 1) in
let result = MQueryGenerator.locate id in
let uris =
List.map
- (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
+ (function uri,_ ->
+ Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format' uri)
result in
let html =
(" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
| Some uri -> UriManager.uri_of_string ("cic:" ^ uri)
;;
-let locate_one_id id =
- let result = MQueryGenerator.locate id in
- let uris =
- List.map
- (function uri,_ ->
- wrong_xpointer_format_from_wrong_xpointer_format' uri
- ) result in
- let html= " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>" in
- output_html (rendering_window ())#outputhtml html ;
- let uris' =
- match uris with
- [] ->
- [UriManager.string_of_uri
- (input_or_locate_uri ~title:("URI matching \"" ^ id ^ "\" unknown."))]
- | [uri] -> [uri]
- | _ ->
- interactive_user_uri_choice
- ~selection_mode:`EXTENDED
- ~ok:"Try every selection."
- ~enable_button_for_non_vars:true
- ~title:"Ambiguous input."
- ~msg:
- ("Ambiguous input \"" ^ id ^
- "\". Please, choose one or more interpretations:")
- uris
- in
- List.map cic_textual_parser_uri_of_string uris'
-;;
-
-
-exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;;
exception AmbiguousInput;;
-type test_result =
- Ok of Cic.term * Cic.metasenv
- | Ko
- | Uncertain
-
-let disambiguate_input context metasenv dom mk_metasenv_and_expr =
- 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 locate_one_id dom' in
- let tests_no =
- List.fold_left (fun i uris -> i * List.length uris) 1 list_of_uris
- in
- if tests_no > 1 then
- output_html (outputhtml ())
- ("<h1>Disambiguation phase started: " ^
- string_of_int tests_no ^ " cases will be tried.") ;
- (* 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'' =
- let resolve_id' =
- function id ->
- match resolve_id id with
- None -> None
- | Some uri -> Some (CicTextualParser0.Uri uri)
- in
- 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 saved_status = !CicTextualParser0.metasenv in
- let metasenv',expr = mk_metasenv_and_expr resolve_id'' in
-(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
- (* The parser is imperative ==> we must restore the old status ;-(( *)
- CicTextualParser0.metasenv := saved_status ;
- 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::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
- filter uris
- | _,_ -> 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
- ("+++++ ASSERTION FAILED: " ^
- "a refine operation should not modify the metasenv") ;
- (* 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 ->
- id,
- match resolve id with
- None -> assert false
- | Some 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 ^ ")"
- ) dom
- ) resolve_ids
- in
- let index = interactive_interpretation_choice choices in
- List.nth resolve_ids index
- in
- id_to_uris := known_ids @ dom', resolve_id' ;
- metasenv',term
+(* A WIDGET TO ENTER CIC TERMS *)
+
+module Callbacks =
+ struct
+ let output_html msg = output_html (outputhtml ()) msg;;
+ let interactive_user_uri_choice =
+ fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
+ interactive_user_uri_choice ~selection_mode ?ok
+ ?enable_button_for_non_vars ~title ~msg;;
+ let interactive_interpretation_choice = interactive_interpretation_choice;;
+ let input_or_locate_uri = input_or_locate_uri;;
+ end
;;
-(* A WIDGET TO ENTER CIC TERMS *)
+module Disambiguate' = Disambiguate.Make(Callbacks);;
class term_editor ?packing ?width ?height ?isnotempty_callback () =
let input = GEdit.text ~editable:true ?width ?height ?packing () in
CicTextualParserContext.main
~context:name_context ~metasenv CicTextualLexer.token lexbuf
in
- disambiguate_input context metasenv dom mk_metasenv_and_expr
+ let id_to_uris',metasenv,expr =
+ Disambiguate'.disambiguate_input context metasenv dom mk_metasenv_and_expr
+ ~id_to_uris:!id_to_uris
+ in
+ id_to_uris := id_to_uris' ;
+ metasenv,expr
end
;;
(fun ~row ~column ~event ->
let (uristr,_) = List.nth results row in
match
- cic_textual_parser_uri_of_string
- (wrong_xpointer_format_from_wrong_xpointer_format' uristr)
+ Disambiguate.cic_textual_parser_uri_of_string
+ (Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format'
+ uristr)
with
CicTextualParser0.ConUri uri
| CicTextualParser0.VarUri uri
let uris =
List.map
(function uri,_ ->
- wrong_xpointer_format_from_wrong_xpointer_format' uri
+ Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format' uri
) result in
let html =
" <h1>Backward Query: </h1>" ^
if
ProofEngine.can_apply
(term_of_cic_textual_parser_uri
- (cic_textual_parser_uri_of_string uri))
+ (Disambiguate.cic_textual_parser_uri_of_string uri))
then
uri::tl',exc
else
projects / helm.git / commitdiff