let getterURL = Configuration.getter_url;;
let processorURL = Configuration.processor_url;;
-(*
-let processorURL = "http://phd.cs.unibo.it:8080/helm/servelt/uwobo/";;
-let getterURL = "http://phd.cs.unibo.it:8081/";;
-let processorURL = "http://localhost:8080/helm/servelt/uwobo/";;
-let getterURL = "http://localhost:8081/";;
-*)
let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
let mml_args =
(* CALLBACKS *)
+exception RefreshSequentException of exn;;
+exception RefreshProofException of exn;;
+
let refresh_proof (output : GMathView.math_view) =
- let uri,currentproof =
- match !ProofEngine.proof with
- None -> assert false
- | Some (uri,metasenv,bo,ty) ->
- uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty))
- in
- let
- (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types)
- =
- Cic2acic.acic_object_of_cic_object currentproof
- in
- let mml = mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types in
- output#load_tree mml ;
- current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
+ try
+ let uri,currentproof =
+ match !ProofEngine.proof with
+ None -> assert false
+ | Some (uri,metasenv,bo,ty) ->
+ uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty))
+ in
+ let
+ (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types)
+ =
+ Cic2acic.acic_object_of_cic_object currentproof
+ in
+ let mml =
+ mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
+ in
+ output#load_tree mml ;
+ current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
+ with
+ e -> raise (RefreshProofException e)
;;
let refresh_sequent (proofw : GMathView.math_view) =
- match !ProofEngine.goal with
- None -> proofw#unload
- | Some (_,currentsequent) ->
- let metasenv =
- match !ProofEngine.proof with
- None -> assert false
- | Some (_,metasenv,_,_) -> metasenv
- in
- let sequent_gdome,ids_to_terms,ids_to_father_ids =
- SequentPp.XmlPp.print_sequent metasenv currentsequent
+ try
+ match !ProofEngine.goal with
+ None -> proofw#unload
+ | Some (_,currentsequent) ->
+ let metasenv =
+ match !ProofEngine.proof with
+ None -> assert false
+ | Some (_,metasenv,_,_) -> metasenv
in
- let sequent_doc =
- Xml2Gdome.document_of_xml domImpl sequent_gdome
+ let sequent_gdome,ids_to_terms,ids_to_father_ids =
+ SequentPp.XmlPp.print_sequent metasenv currentsequent
in
- let sequent_mml =
- applyStylesheets sequent_doc sequent_styles sequent_args
+ let sequent_doc =
+ Xml2Gdome.document_of_xml domImpl sequent_gdome
in
- proofw#load_tree ~dom:sequent_mml ;
- current_goal_infos := Some (ids_to_terms,ids_to_father_ids)
+ let sequent_mml =
+ applyStylesheets sequent_doc sequent_styles sequent_args
+ in
+ proofw#load_tree ~dom:sequent_mml ;
+ current_goal_infos := Some (ids_to_terms,ids_to_father_ids)
+ with
+ e -> raise (RefreshSequentException e)
+;;
+
(*
ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
~name:"/public/sacerdot/guruguru1" ~indent:true ()) ;
-ignore(domImpl#saveDocumentToFile ~doc:sequent_mml
- ~name:"/public/sacerdot/guruguru2" ~indent:true ())
*)
-;;
let mml_of_cic_term term =
let context =
refresh_sequent proofw ;
refresh_proof output
with
- e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw ;
+ refresh_proof output
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
end
;;
in
let context =
List.map
- (function (_,n,_) -> n)
+ (function
+ ProofEngine.Definition (n,_)
+ | ProofEngine.Declaration (n,_) -> n)
(match !ProofEngine.goal with
None -> assert false
| Some (_,(ctx,_)) -> ctx
with
CicTextualParser0.Eof ->
inputt#delete_text 0 inputlen
+ | RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw ;
+ refresh_proof output
| e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>");
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal
+ ProofEngine.goal := savedgoal ;
;;
let call_tactic_with_goal_input tactic rendering_window () =
refresh_proof rendering_window#output
| None -> assert false (* "ERROR: No current term!!!" *)
with
- e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw ;
+ refresh_proof output
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
end
| None ->
output_html outputhtml
in
let context =
List.map
- (function (_,n,_) -> n)
+ (function
+ ProofEngine.Definition (n,_)
+ | ProofEngine.Declaration (n,_) -> n)
(match !ProofEngine.goal with
None -> assert false
| Some (_,(ctx,_)) -> ctx
end
| None -> assert false (* "ERROR: No current term!!!" *)
with
- e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw ;
+ refresh_proof output
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
end
| None ->
output_html outputhtml
let change rendering_window =
call_tactic_with_input_and_goal_input ProofEngine.change rendering_window
;;
+let letin rendering_window =
+ call_tactic_with_input ProofEngine.letin rendering_window
+;;
let whd_in_scratch scratch_window =
refresh_sequent rendering_window#proofw
| None -> assert false (* "ERROR: No current term!!!" *)
with
- e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
end
| None -> assert false (* "ERROR: No selection!!!" *)
;;
ProofEngine.proof :=
Some (uri, metasenv, bo, ty) ;
ProofEngine.goal := None ;
- inputt#delete_text 0 inputlen ;
- ignore(oldinputt#insert_text input oldinputt#length) ;
refresh_sequent proofw ;
refresh_proof output ;
+ inputt#delete_text 0 inputlen ;
+ ignore(oldinputt#insert_text input oldinputt#length)
with
- e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
;;
let state rendering_window () =
match CicTextualParser.main CicTextualLexer.token lexbuf with
None -> ()
| Some expr ->
- try
- 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,([],expr)) ;
- refresh_sequent proofw ;
- refresh_proof output ;
- with
- e ->
- print_endline ("? " ^ CicPp.ppterm expr) ;
- raise e
+ 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,([],expr)) ;
+ refresh_sequent proofw ;
+ refresh_proof output ;
done
with
CicTextualParser0.Eof ->
inputt#delete_text 0 inputlen ;
ignore(oldinputt#insert_text input oldinputt#length)
+ | RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
| e ->
output_html outputhtml
("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
let check rendering_window scratch_window () =
let inputt = (rendering_window#inputt : GEdit.text) in
- let oldinputt = (rendering_window#oldinputt : 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
None -> []
| Some (_,(ctx,_)) -> ctx
in
- ProofEngine.cic_context_of_context context,
- List.map (function (_,n,_) -> n) context
+ ProofEngine.cic_context_of_named_context context,
+ List.map
+ (function
+ ProofEngine.Declaration (n,_)
+ | ProofEngine.Definition (n,_) -> n
+ ) context
in
(* Do something interesting *)
let lexbuf = Lexing.from_string input in
raise e
done
with
- CicTextualParser0.Eof ->
- inputt#delete_text 0 inputlen ;
- ignore(oldinputt#insert_text input oldinputt#length)
+ CicTextualParser0.Eof -> ()
| e ->
output_html outputhtml
("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
let changeb =
GButton.button ~label:"Change"
~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let letinb =
+ GButton.button ~label:"Let ... In"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
let outputhtml =
GHtml.xmhtml
~source:"<html><body bgColor=\"white\"></body></html>"
ignore(foldb#connect#clicked (fold self)) ;
ignore(cutb#connect#clicked (cut self)) ;
ignore(changeb#connect#clicked (change self)) ;
+ ignore(letinb#connect#clicked (letin self)) ;
ignore(introsb#connect#clicked (intros self)) ;
Logger.log_callback :=
(Logger.log_to_html ~print_and_flush:(output_html outputhtml))
projects / helm.git / blobdiff