-let decompose_uris_choice_callback uris =
-(* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *)
- let module U = UriManager in
- List.map
- (function uri ->
- match Misc.cic_textual_parser_uri_of_string uri with
- CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
- | _ -> assert false)
- (interactive_user_uri_choice
- ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false
- ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose"
- (List.map
- (function (uri,typeno,_) ->
- U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1)
- ) uris)
- )
-;;
-
-(***********************)
-(* TACTICS *)
-(***********************)
-
-let call_tactic tactic () =
- let notebook = (rendering_window ())#notebook in
- let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let savedproof = !ProofEngine.proof in
- let savedgoal = !ProofEngine.goal in
- begin
- try
- tactic () ;
- refresh_sequent notebook ;
- refresh_proof output
- with
- 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 notebook
- | 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 notebook ;
- refresh_proof output
- | e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- end
-;;
-
-let call_tactic_with_input tactic () =
- let notebook = (rendering_window ())#notebook in
- let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let savedproof = !ProofEngine.proof in
- let savedgoal = !ProofEngine.goal in
- let uri,metasenv,bo,ty =
- match !ProofEngine.proof with
- 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
- try
- let metasenv',expr =
- inputt#get_metasenv_and_term canonical_context metasenv
- in
- ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
- tactic expr ;
- refresh_sequent notebook ;
- refresh_proof output ;
- inputt#reset
- with
- 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 notebook
- | 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 notebook ;
- refresh_proof output
- | e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
-;;
-
-let call_tactic_with_goal_input tactic () =
- let module L = LogicalOperations in
- let module G = Gdome in
- let notebook = (rendering_window ())#notebook in
- let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let savedproof = !ProofEngine.proof in
- let savedgoal = !ProofEngine.goal in
- match notebook#proofw#get_selections with
- [node] ->
- let xpath =
- ((node : Gdome.element)#getAttributeNS
- ~namespaceURI:Misc.helmns
- ~localName:(G.domString "xref"))#to_string
- in
- if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
- else
- begin
- try
- match !current_goal_infos with
- Some (ids_to_terms, ids_to_father_ids,_) ->
- let id = xpath in
- tactic (Hashtbl.find ids_to_terms id) ;
- refresh_sequent notebook ;
- refresh_proof output
- | None -> assert false (* "ERROR: No current term!!!" *)
- with
- 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 notebook
- | 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 notebook ;
- refresh_proof output
- | e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- end
- | [] ->
- output_html outputhtml
- ("<h1 color=\"red\">No term selected</h1>")
- | _ ->
- output_html outputhtml
- ("<h1 color=\"red\">Many terms selected</h1>")
-;;
-
-let call_tactic_with_goal_inputs tactic () =
- let module L = LogicalOperations in
- let module G = Gdome in
- let notebook = (rendering_window ())#notebook in
- let output =
- ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let savedproof = !ProofEngine.proof in
- let savedgoal = !ProofEngine.goal in
- try
- let term_of_node node =
- let xpath =
- ((node : Gdome.element)#getAttributeNS
- ~namespaceURI:Misc.helmns
- ~localName:(G.domString "xref"))#to_string
- in
- if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
- else
- match !current_goal_infos with
- Some (ids_to_terms, ids_to_father_ids,_) ->
- let id = xpath in
- (Hashtbl.find ids_to_terms id)
- | None -> assert false (* "ERROR: No current term!!!" *)
- in
- match notebook#proofw#get_selections with
- [] ->
- output_html outputhtml
- ("<h1 color=\"red\">No term selected</h1>")
- | l ->
- let terms = List.map term_of_node l in
- match !current_goal_infos with
- Some (ids_to_terms, ids_to_father_ids,_) ->
- tactic terms ;
- refresh_sequent notebook ;
- refresh_proof output
- | None -> assert false (* "ERROR: No current term!!!" *)
- with
- 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 notebook
- | 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 notebook ;
- refresh_proof output
- | e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal
-;;
-
-let call_tactic_with_input_and_goal_input tactic () =
- let module L = LogicalOperations in
- let module G = Gdome in
- let notebook = (rendering_window ())#notebook in
- let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let savedproof = !ProofEngine.proof in
- let savedgoal = !ProofEngine.goal in
- match notebook#proofw#get_selections with
- [node] ->
- let xpath =
- ((node : Gdome.element)#getAttributeNS
- ~namespaceURI:Misc.helmns
- ~localName:(G.domString "xref"))#to_string
- in
- if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
- else
- begin
- try
- match !current_goal_infos with
- Some (ids_to_terms, ids_to_father_ids,_) ->
- let id = xpath in
- let uri,metasenv,bo,ty =
- match !ProofEngine.proof with
- 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 (metasenv',expr) =
- inputt#get_metasenv_and_term canonical_context metasenv
- in
- ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
- tactic ~goal_input:(Hashtbl.find ids_to_terms id)
- ~input:expr ;
- refresh_sequent notebook ;
- refresh_proof output ;
- inputt#reset
- | None -> assert false (* "ERROR: No current term!!!" *)
- with
- 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 notebook
- | 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 notebook ;
- refresh_proof output
- | e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- end
- | [] ->
- output_html outputhtml
- ("<h1 color=\"red\">No term selected</h1>")
- | _ ->
- output_html outputhtml
- ("<h1 color=\"red\">Many terms selected</h1>")
-;;
-
-let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
- let module L = LogicalOperations in
- let module G = Gdome in
- let mmlwidget =
- (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let savedproof = !ProofEngine.proof in
- let savedgoal = !ProofEngine.goal in
- match mmlwidget#get_selections with
- [node] ->
- let xpath =
- ((node : Gdome.element)#getAttributeNS
- ~namespaceURI:Misc.helmns
- ~localName:(G.domString "xref"))#to_string
- in
- if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
- else
- begin
- try
- match !current_scratch_infos with
- (* term is the whole goal in the scratch_area *)
- Some (term,ids_to_terms, ids_to_father_ids,_) ->
- let id = xpath in
- let expr = tactic term (Hashtbl.find ids_to_terms id) in
- let mml = mml_of_cic_term 111 expr in
- scratch_window#show () ;
- scratch_window#mmlwidget#load_doc ~dom:mml
- | None -> assert false (* "ERROR: No current term!!!" *)
- with
- e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
- end
- | [] ->
- output_html outputhtml
- ("<h1 color=\"red\">No term selected</h1>")
- | _ ->
- output_html outputhtml
- ("<h1 color=\"red\">Many terms selected</h1>")
-;;
-
-let call_tactic_with_goal_inputs_in_scratch tactic scratch_window () =
- let module L = LogicalOperations in
- let module G = Gdome in
- let mmlwidget =
- (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let savedproof = !ProofEngine.proof in
- let savedgoal = !ProofEngine.goal in
- match mmlwidget#get_selections with
- [] ->
- output_html outputhtml
- ("<h1 color=\"red\">No term selected</h1>")
- | l ->
- try
- match !current_scratch_infos with
- (* term is the whole goal in the scratch_area *)
- Some (term,ids_to_terms, ids_to_father_ids,_) ->
- let term_of_node node =
- let xpath =
- ((node : Gdome.element)#getAttributeNS
- ~namespaceURI:Misc.helmns
- ~localName:(G.domString "xref"))#to_string
- in
- if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
- else
- let id = xpath in
- Hashtbl.find ids_to_terms id
- in
- let terms = List.map term_of_node l in
- let expr = tactic terms term in
- let mml = mml_of_cic_term 111 expr in
- scratch_window#show () ;
- scratch_window#mmlwidget#load_doc ~dom:mml
- | None -> assert false (* "ERROR: No current term!!!" *)
- with
- e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
-;;
-
-let call_tactic_with_hypothesis_input tactic () =
- let module L = LogicalOperations in
- let module G = Gdome in
- let notebook = (rendering_window ())#notebook in
- let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let savedproof = !ProofEngine.proof in
- let savedgoal = !ProofEngine.goal in
- match notebook#proofw#get_selections with
- [node] ->
- let xpath =
- ((node : Gdome.element)#getAttributeNS
- ~namespaceURI:Misc.helmns
- ~localName:(G.domString "xref"))#to_string
- in
- if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
- else
- begin
- try
- match !current_goal_infos with
- Some (_,_,ids_to_hypotheses) ->
- let id = xpath in
- tactic (Hashtbl.find ids_to_hypotheses id) ;
- refresh_sequent notebook ;
- refresh_proof output
- | None -> assert false (* "ERROR: No current term!!!" *)
- with
- 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 notebook
- | 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 notebook ;
- refresh_proof output
- | e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- end
- | [] ->
- output_html outputhtml
- ("<h1 color=\"red\">No term selected</h1>")
- | _ ->
- output_html outputhtml
- ("<h1 color=\"red\">Many terms selected</h1>")
-;;
-
-
-let intros = call_tactic (ProofEngine.intros ~mk_fresh_name_callback);;
-let exact = call_tactic_with_input ProofEngine.exact;;
-let apply = call_tactic_with_input ProofEngine.apply;;
-let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;;
-let elimtype = call_tactic_with_input ProofEngine.elim_type;;
-let whd = call_tactic_with_goal_inputs ProofEngine.whd;;
-let reduce = call_tactic_with_goal_inputs ProofEngine.reduce;;
-let simpl = call_tactic_with_goal_inputs ProofEngine.simpl;;
-let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
-let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
-let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;;
-let cut = call_tactic_with_input (ProofEngine.cut ~mk_fresh_name_callback);;
-let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
-let letin = call_tactic_with_input (ProofEngine.letin ~mk_fresh_name_callback);;
-let ring = call_tactic ProofEngine.ring;;
-let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
-let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
-let fourier = call_tactic ProofEngine.fourier;;
-let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
-let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl;;
-let replace = call_tactic_with_input_and_goal_input ProofEngine.replace;;
-let reflexivity = call_tactic ProofEngine.reflexivity;;
-let symmetry = call_tactic ProofEngine.symmetry;;
-let transitivity = call_tactic_with_input ProofEngine.transitivity;;
-let exists = call_tactic ProofEngine.exists;;
-let split = call_tactic ProofEngine.split;;
-let left = call_tactic ProofEngine.left;;
-let right = call_tactic ProofEngine.right;;
-let assumption = call_tactic ProofEngine.assumption;;
-let generalize =
- call_tactic_with_goal_inputs (ProofEngine.generalize ~mk_fresh_name_callback);;
-let absurd = call_tactic_with_input ProofEngine.absurd;;
-let contradiction = call_tactic ProofEngine.contradiction;;
-let decompose =
- call_tactic_with_input
- (ProofEngine.decompose ~uris_choice_callback:decompose_uris_choice_callback);;
-
-let whd_in_scratch scratch_window =
- call_tactic_with_goal_inputs_in_scratch ProofEngine.whd_in_scratch
- scratch_window
-;;
-let reduce_in_scratch scratch_window =
- call_tactic_with_goal_inputs_in_scratch ProofEngine.reduce_in_scratch
- scratch_window
-;;
-let simpl_in_scratch scratch_window =
- call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch
- scratch_window
-;;
-
-
-
-(**********************)
-(* END OF TACTICS *)
-(**********************)
-
-
projects / helm.git / commitdiff