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
)
;;
+
let term_of_uri uri =
let module C = Cic in
let module CTP = CicTextualParser0 in
| 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 ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
+;;
+
+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= " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>" 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 =
res
;;
-let output_html outputhtml msg =
- htmlheader_and_content := !htmlheader_and_content ^ msg ;
- outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
- outputhtml#set_topline (-1)
-;;
-
(***********************)
(* TACTICS *)
(***********************)
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 ->
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 ->
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 ->
("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
;;
+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 =
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 -> ()
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 ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
-;;
-
let locate rendering_window () =
let inputt = (rendering_window#inputt : GEdit.text) in
let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
result in
let html = (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>") 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 ->
string_of_int (List.length uris') ^ "</h1>"
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
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
(* MAIN *)
-let rendering_window = ref None;;
-
let initialize_everything () =
let module U = Unix in
let output = GMathView.math_view ~width:350 ~height:280 ()
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 =
- (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
- 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 ();
projects / helm.git / commitdiff