From c8b208db309024a3dfefe1cda073734afc27bf3c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 21 Jan 2003 11:24:52 +0000 Subject: [PATCH] New module Disambiguate to hold: - a functor to disambiguate terms. The input module holds all the callbacks to the user (that will be implemented differently in Gtk and as Web forms). - some utility functions working on CicTextualParser0.uri which should be moved somewhere else. --- helm/gTopLevel/.depend | 14 +- helm/gTopLevel/Makefile | 28 +-- helm/gTopLevel/disambiguate.ml | 321 ++++++++++++++++++++++++++++++++ helm/gTopLevel/disambiguate.mli | 74 ++++++++ helm/gTopLevel/gTopLevel.ml | 264 +++----------------------- 5 files changed, 449 insertions(+), 252 deletions(-) create mode 100644 helm/gTopLevel/disambiguate.ml create mode 100644 helm/gTopLevel/disambiguate.mli diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 58de61eda..6989c187b 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -94,9 +94,11 @@ mQueryLevels2.cmo: mQueryLevels2.cmi 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 diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index e4ece089e..e919c6a24 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -18,24 +18,26 @@ DEPOBJS = xml2Gdome.ml xml2Gdome.mli proofEngineTypes.ml proofEngineHelpers.ml \ 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: diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml new file mode 100644 index 000000000..11de21b18 --- /dev/null +++ b/helm/gTopLevel/disambiguate.ml @@ -0,0 +1,321 @@ +(* 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 *) +(* 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 ^ "

Result:

" ^ MQueryUtil.text_of_result result "
" +;; + +(** 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= + "

Locate Query: 

" ^ get_last_query result ^ "
" + 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 + ("

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 +;; diff --git a/helm/gTopLevel/disambiguate.mli b/helm/gTopLevel/disambiguate.mli new file mode 100644 index 000000000..63206cb15 --- /dev/null +++ b/helm/gTopLevel/disambiguate.mli @@ -0,0 +1,74 @@ +(* 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 *) +(* 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 diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index d1b9b9964..ebe26c3e3 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -34,17 +34,6 @@ (******************************************************************************) -(* 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";; @@ -172,33 +161,6 @@ Arg.parse argspec ignore "" (* 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 @@ -258,7 +220,8 @@ let check_window outputhtml uris = ~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 @@ -280,7 +243,7 @@ let check_window outputhtml uris = 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 @@ -298,7 +261,7 @@ let 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 @@ -963,7 +926,7 @@ let edit_aliases () = 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 @@ -1164,7 +1127,8 @@ let locate_callback id = 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 = ("

Locate Query: 

" ^ get_last_query result ^ "
") @@ -1282,195 +1246,23 @@ let input_or_locate_uri ~title = | 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= "

Locate Query: 

" ^ get_last_query result ^ "
" 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 ()) - ("

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 @@ -1504,7 +1296,12 @@ object(self) 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 ;; @@ -2451,8 +2248,9 @@ let show_query_results results = (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 @@ -2908,7 +2706,7 @@ let searchPattern () = 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 = "

Backward Query:

" ^ @@ -2925,7 +2723,7 @@ let searchPattern () = 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 -- 2.39.2