From 195b0fd30ddcb7f9b3a8cb3ff44457ff88d13bb0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 4 Nov 2002 09:56:02 +0000 Subject: [PATCH] - new CicTextualParser - improved disambiguation of parsed stuff - improved interface for disambiguating uris --- helm/gTopLevel/gTopLevel.ml | 435 +++++++++++++++++++++++++----------- 1 file changed, 305 insertions(+), 130 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 58e6180f0..88b6f9206 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -85,6 +85,11 @@ let current_cic_infos = ref None;; let current_goal_infos = ref None;; let current_scratch_infos = ref None;; +let id_to_uris = ref ([],function _ -> None);; + +let check_term = ref (fun _ _ _ -> assert false);; +let rendering_window = ref None;; + (* COMMAND LINE OPTIONS *) let usedb = ref true @@ -121,6 +126,7 @@ let cic_textual_parser_uri_of_uri uri' = ) ;; + let term_of_uri uri = let module C = Cic in let module CTP = CicTextualParser0 in @@ -131,6 +137,209 @@ let term_of_uri uri = | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[]) ;; +(* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *) + +exception NoChoice;; + +let interactive_user_uri_choice ?(cancel="Cancel") ~title ~msg uris = + let choice = ref None in + let window = GWindow.dialog ~modal:true ~title () in + let lMessage = + GMisc.label ~text:msg ~packing:window#vbox#add () in + let vbox = GPack.vbox ~border_width:10 + ~packing:(window#action_area#pack ~expand:true ~padding:4) () in + let hbox1 = GPack.hbox ~border_width:10 ~packing:vbox#add () in + let combo = + GEdit.combo ~popdown_strings:uris ~packing:hbox1#add () in + let checkb = + GButton.button ~label:"Check" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let hbox = GPack.hbox ~border_width:10 ~packing:vbox#add () in + let okb = + GButton.button ~label:"Ok" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let cancelb = + GButton.button ~label:cancel + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + (* actions *) + let ok_callback () = + choice := Some combo#entry#text ; + window#destroy () + in + let check_callback () = !check_term [] [] (term_of_uri combo#entry#text) in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore (okb#connect#clicked ok_callback) ; + ignore (checkb#connect#clicked check_callback) ; + window#set_position `CENTER ; + window#show () ; + GMain.Main.main () ; + match !choice with + None -> raise NoChoice + | Some uri -> uri +;; + +(* MISC FUNCTIONS *) + +(* 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 "
" +;; + +let register_alias (id,uri) = + let dom,resolve_id = !id_to_uris in + id_to_uris := + (if List.mem id dom then dom else id::dom), + function id' -> if id' = id then Some uri else resolve_id id' +;; + +let output_html outputhtml msg = + htmlheader_and_content := !htmlheader_and_content ^ msg ; + outputhtml#source (!htmlheader_and_content ^ htmlfooter) ; + outputhtml#set_topline (-1) +;; + +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 + begin + match !rendering_window with + None -> assert false + | Some rw -> output_html rw#outputhtml html ; + end ; + let uris' = + match uris with + [] -> + (match + (GToolbox.input_string ~title:"Unknown input" + ("No URI matching \"" ^ id ^ "\" found. Please enter its URI")) + with + None -> raise NoChoice + | Some uri -> ["cic:" ^ uri] + ) + | [uri] -> [uri] + | _ -> + try + [interactive_user_uri_choice + ~cancel:"Try every possibility." + ~title:"Ambiguous input." + ~msg: + ("Ambiguous input \"" ^ id ^ + "\". Please, choose one interpretation:") + uris + ] + with + NoChoice -> uris + in + List.map cic_textual_parser_uri_of_uri uris' +;; + +exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;; +exception AmbiguousInput;; + +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 + (* and now we compute the list of all possible assignments from id to uris *) + let resolve_ids = + let rec aux ids list_of_uris = + match ids,list_of_uris with + [],[] -> [resolve_id] + | id::idtl,uris::uristl -> + let resolves = aux idtl uristl in + List.concat + (List.map + (function uri -> + List.map + (function f -> + function id' -> if id = id' then Some uri else f id' + ) resolves + ) uris + ) + | _,_ -> assert false + in + aux dom' list_of_uris + in +prerr_endline ("##### NE DISAMBIGUO: " ^ string_of_int (List.length resolve_ids)) ; + (* now we select only the ones that generates well-typed terms *) + let resolve_ids' = + let rec filter = + function + [] -> [] + | resolve::tl -> + let metasenv',expr = mk_metasenv_and_expr resolve in + try +(*CSC: Bug here: we do not try to typecheck also the metasenv' *) + ignore + (CicTypeChecker.type_of_aux' metasenv context expr) ; + resolve::(filter tl) + with + _ -> filter tl + in + filter resolve_ids + in + let resolve_id' = + match resolve_ids' with + [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput + | [resolve_id] -> resolve_id + | _ -> + let choices = + List.map + (function resolve -> + String.concat " ; " + (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 choice = + GToolbox.question_box ~title:"Ambiguous input." + ~buttons:choices + ~default:1 "Ambiguous input. Please, choose one interpretation." + in + if choice > 0 then + List.nth resolve_ids' (choice - 1) + else + (* No choice from the user *) + raise NoChoice + in + id_to_uris := known_ids @ dom', resolve_id' ; + mk_metasenv_and_expr resolve_id' +;; + let domImpl = Gdome.domImplementation ();; let parseStyle name = @@ -346,12 +555,6 @@ let mml_of_cic_term metano term = res ;; -let output_html outputhtml msg = - htmlheader_and_content := !htmlheader_and_content ^ msg ; - outputhtml#source (!htmlheader_and_content ^ htmlfooter) ; - outputhtml#set_topline (-1) -;; - (***********************) (* TACTICS *) (***********************) @@ -412,32 +615,38 @@ let call_tactic_with_input tactic rendering_window () = None -> assert false | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty in + let canonical_context = + match !ProofEngine.goal with + None -> assert false + | Some metano -> + let (_,canonical_context,_) = + List.find (function (m,_,_) -> m=metano) metasenv + in + canonical_context + in let context = List.map (function Some (n,_) -> Some n - | None -> None) - (match !ProofEngine.goal with - None -> assert false - | Some metano -> - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=metano) metasenv - in - canonical_context - ) + | None -> None + ) canonical_context in try while true do match - CicTextualParserContext.main - curi context metasenv CicTextualLexer.token lexbuf + CicTextualParserContext.main context metasenv CicTextualLexer.token + lexbuf register_alias with None -> () - | Some (metasenv',expr) -> - ProofEngine.proof := Some (uri,metasenv',bo,ty) ; - tactic expr ; - refresh_sequent proofw ; - refresh_proof output + | Some (dom,mk_metasenv_and_expr) -> + let (metasenv',expr) = + disambiguate_input canonical_context metasenv dom + mk_metasenv_and_expr + in + ProofEngine.proof := Some (uri,metasenv',bo,ty) ; + tactic expr ; + refresh_sequent proofw ; + refresh_proof output done with CicTextualParser0.Eof -> @@ -554,34 +763,39 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () = None -> assert false | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty in + let canonical_context = + match !ProofEngine.goal with + None -> assert false + | Some metano -> + let (_,canonical_context,_) = + List.find (function (m,_,_) -> m=metano) metasenv + in + canonical_context in let context = List.map (function Some (n,_) -> Some n - | None -> None) - (match !ProofEngine.goal with - None -> assert false - | Some metano -> - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=metano) metasenv - in - canonical_context - ) + | None -> None + ) canonical_context in begin try while true do match - CicTextualParserContext.main curi context metasenv - CicTextualLexer.token lexbuf + CicTextualParserContext.main context metasenv + CicTextualLexer.token lexbuf register_alias with None -> () - | Some (metasenv',expr) -> - ProofEngine.proof := Some (uri,metasenv',bo,ty) ; - tactic ~goal_input:(Hashtbl.find ids_to_terms id) - ~input:expr ; - refresh_sequent proofw ; - refresh_proof output + | Some (dom,mk_metasenv_and_expr) -> + let (metasenv',expr) = + disambiguate_input canonical_context metasenv dom + mk_metasenv_and_expr + in + ProofEngine.proof := Some (uri,metasenv',bo,ty) ; + tactic ~goal_input:(Hashtbl.find ids_to_terms id) + ~input:expr ; + refresh_sequent proofw ; + refresh_proof output done with CicTextualParser0.Eof -> @@ -1105,16 +1319,22 @@ let state rendering_window () = try while true do (* Execute the actions *) - match CicTextualParser.main CicTextualLexer.token lexbuf with + match + CicTextualParserContext.main [] [] CicTextualLexer.token + lexbuf register_alias + with None -> () - | Some expr -> - let _ = CicTypeChecker.type_of_aux' [] [] expr in - ProofEngine.proof := - Some (UriManager.uri_of_string "cic:/dummy.con", - [1,[],expr], Cic.Meta (1,[]), expr) ; - ProofEngine.goal := Some 1 ; - refresh_sequent proofw ; - refresh_proof output ; + | Some (dom,mk_metasenv_and_expr) -> + let metasenv,expr = + disambiguate_input [] [] dom mk_metasenv_and_expr + in + let _ = CicTypeChecker.type_of_aux' metasenv [] expr in + ProofEngine.proof := + Some (UriManager.uri_of_string "cic:/dummy.con", + (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ; + ProofEngine.goal := Some 1 ; + refresh_sequent proofw ; + refresh_proof output ; done with CicTextualParser0.Eof -> @@ -1133,11 +1353,22 @@ let state rendering_window () = ("

" ^ Printexc.to_string e ^ "

") ; ;; +let check_term_in_scratch scratch_window metasenv context expr = + try + let ty = CicTypeChecker.type_of_aux' metasenv context expr in + let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in +prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ; + scratch_window#show () ; + scratch_window#mmlwidget#load_tree ~dom:mml + with + e -> + print_endline ("? " ^ CicPp.ppterm expr) ; + raise e +;; + let check rendering_window scratch_window () = let inputt = (rendering_window#inputt : GEdit.text) in let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let output = (rendering_window#output : GMathView.math_view) in - let proofw = (rendering_window#proofw : GMathView.math_view) in let inputlen = inputt#length in let input = inputt#get_chars 0 inputlen ^ "\n" in let curi,metasenv = @@ -1167,21 +1398,15 @@ let check rendering_window scratch_window () = while true do (* Execute the actions *) match - CicTextualParserContext.main curi names_context metasenv - CicTextualLexer.token lexbuf + CicTextualParserContext.main names_context metasenv CicTextualLexer.token + lexbuf register_alias with None -> () - | Some (metasenv',expr) -> - try - let ty = CicTypeChecker.type_of_aux' metasenv' context expr in - let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in -prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ; - scratch_window#show () ; - scratch_window#mmlwidget#load_tree ~dom:mml - with - e -> - print_endline ("? " ^ CicPp.ppterm expr) ; - raise e + | Some (dom,mk_metasenv_and_expr) -> + let (metasenv',expr) = + disambiguate_input context metasenv dom mk_metasenv_and_expr + in + check_term_in_scratch scratch_window metasenv' context expr done with CicTextualParser0.Eof -> () @@ -1192,30 +1417,17 @@ prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ; exception NoObjectsLocated;; -let user_uri_choice uris = +let user_uri_choice ~title ~msg uris = let uri = match uris with [] -> raise NoObjectsLocated | [uri] -> uri | uris -> - let choice = - GToolbox.question_box ~title:"Ambiguous result." - ~buttons:uris ~default:1 - "Ambiguous result. Please, choose one." - in - List.nth uris (choice-1) + interactive_user_uri_choice ~title ~msg uris in String.sub uri 4 (String.length uri - 4) ;; -(* 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 "
" -;; - let locate rendering_window () = let inputt = (rendering_window#inputt : GEdit.text) in let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in @@ -1233,7 +1445,13 @@ let locate rendering_window () = result in let html = ("

Locate Query: 

" ^ get_last_query result ^ "
") in output_html outputhtml html ; - let uri' = user_uri_choice uris in + let uri' = + user_uri_choice ~title:"Ambiguous input." + ~msg: + ("Ambiguous input \"" ^ head ^ + "\". Please, choose one interpetation:") + uris + in ignore ((inputt#insert_text uri') ~pos:0) with e -> @@ -1300,7 +1518,11 @@ let searchPattern rendering_window () = string_of_int (List.length uris') ^ "" in output_html outputhtml html' ; - let uri' = user_uri_choice uris' in + let uri' = + user_uri_choice ~title:"Ambiguous input." + ~msg:"Many lemmas can be successfully applied. Please, choose one:" + uris' + in inputt#delete_text 0 inputlen ; ignore ((inputt#insert_text uri') ~pos:0) with @@ -1661,6 +1883,7 @@ object(self) method show = window#show initializer button_export_to_postscript#misc#set_sensitive false ; + check_term := (check_term_in_scratch scratch_window) ; (* signal handlers here *) ignore(output#connect#selection_changed @@ -1716,8 +1939,6 @@ end;; (* MAIN *) -let rendering_window = ref None;; - let initialize_everything () = let module U = Unix in let output = GMathView.math_view ~width:350 ~height:280 () @@ -1733,54 +1954,8 @@ let initialize_everything () = let _ = if !usedb then - begin -(* - Mqint.init "dbname=helm" ; -*) - Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; - CicTextualParser0.set_locate_object - (function 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 - begin - match !rendering_window with - None -> assert false - | Some rw -> output_html rw#outputhtml html ; - end ; - let uri = - match uris with - [] -> - (match - (GToolbox.input_string ~title:"Unknown input" - ("No URI matching \"" ^ id ^ "\" found. Please enter its URI")) - with - None -> None - | Some uri -> Some ("cic:" ^ uri) - ) - | [uri] -> Some uri - | _ -> - let choice = - GToolbox.question_box ~title:"Ambiguous input." - ~buttons:uris ~default:1 "Ambiguous input. Please, choose one." - in - if choice > 0 then - Some (List.nth uris (choice - 1)) - else - (* No choice from the user *) - None - in - match uri with - Some uri' -> Some (cic_textual_parser_uri_of_uri uri') - | None -> None - ) - end ; +(* Mqint.init "dbname=helm_mowgli" ; *) + Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; ignore (GtkMain.Main.init ()) ; initialize_everything () ; if !usedb then Mqint.close (); -- 2.39.2