("<h1 color=\"red\">No term selected</h1>")
;;
+let call_tactic_with_hypothesis_input tactic rendering_window () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+ let proofw = (rendering_window#proofw : GMathView.math_view) in
+ let output = (rendering_window#output : GMathView.math_view) in
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ let savedproof = !ProofEngine.proof in
+ let savedgoal = !ProofEngine.goal in
+ match proofw#get_selection with
+ Some node ->
+ let xpath =
+ ((node : Gdome.element)#getAttributeNS
+ ~namespaceURI: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 rendering_window#proofw ;
+ refresh_proof rendering_window#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 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
+ ("<h1 color=\"red\">No term selected</h1>")
+;;
+
+
let intros rendering_window = call_tactic ProofEngine.intros rendering_window;;
let exact rendering_window =
call_tactic_with_input ProofEngine.exact rendering_window
let letin rendering_window =
call_tactic_with_input ProofEngine.letin rendering_window
;;
+let clearbody rendering_window =
+ call_tactic_with_hypothesis_input ProofEngine.clearbody rendering_window
+;;
+let clear rendering_window =
+ call_tactic_with_hypothesis_input ProofEngine.clear rendering_window
+;;
let whd_in_scratch scratch_window =
let letinb =
GButton.button ~label:"Let ... In"
~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let hbox4 =
+ GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let clearbodyb =
+ GButton.button ~label:"ClearBody"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let clearb =
+ GButton.button ~label:"Clear"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
let outputhtml =
GHtml.xmhtml
~source:"<html><body bgColor=\"white\"></body></html>"
ignore(cutb#connect#clicked (cut self)) ;
ignore(changeb#connect#clicked (change self)) ;
ignore(letinb#connect#clicked (letin self)) ;
+ ignore(clearbodyb#connect#clicked (clearbody self)) ;
+ ignore(clearb#connect#clicked (clear self)) ;
ignore(introsb#connect#clicked (intros self)) ;
Logger.log_callback :=
(Logger.log_to_html ~print_and_flush:(output_html outputhtml))
None -> assert false
| Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
in
- let term' = reduction_function context term in
- (* We don't know if [term] is a subterm of [ty] or a subterm of *)
- (* the type of one metavariable. So we replace it everywhere. *)
- (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
- (*CSC: che si guadagni nulla in fatto di efficienza. *)
- let replace =
- ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term'
+ (* We don't know if [term] is a subterm of [ty] or a subterm of *)
+ (* the type of one metavariable. So we replace it everywhere. *)
+ (*CSC: Il vero problema e' che non sapendo dove sia il term non *)
+ (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma, *)
+ (*CSC: e' meglio prima cercare il termine e scoprirne il *)
+ (*CSC: contesto, poi ridurre e infine rimpiazzare. *)
+ let replace context where=
+(*CSC: Per il momento se la riduzione fallisce significa solamente che *)
+(*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *)
+(*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *)
+ try
+ let term' = reduction_function context term in
+ ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term'
+ ~where:where
+ with
+ _ -> where
in
- let ty' = replace ty in
+ let ty' = replace context ty in
let context' =
- List.map
- (function
- Some (name,Cic.Def t) -> Some (name,Cic.Def (replace t))
- | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
- | None -> None
- ) context
+ List.fold_right
+ (fun entry context ->
+ match entry with
+ Some (name,Cic.Def t) ->
+ (Some (name,Cic.Def (replace context t)))::context
+ | Some (name,Cic.Decl t) ->
+ (Some (name,Cic.Decl (replace context t)))::context
+ | None -> None::context
+ ) context []
in
let metasenv' =
List.map
else
raise NotConvertible
;;
+
+let clearbody =
+ let module C = Cic in
+ function
+ None -> assert false
+ | Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
+ | Some (n_to_clear_body, C.Def term) as hyp_to_clear_body ->
+ let curi,metasenv,pbo,pty =
+ match !proof with
+ None -> assert false
+ | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
+ in
+ let metano,_,_ =
+ match !goal with
+ None -> assert false
+ | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
+ in
+ let string_of_name =
+ function
+ C.Name n -> n
+ | C.Anonimous -> "_"
+ in
+ let metasenv' =
+ List.map
+ (function
+ (m,canonical_context,ty) when m = metano ->
+ let canonical_context' =
+ List.fold_right
+ (fun entry context ->
+ match entry with
+ t when t == hyp_to_clear_body ->
+ let cleared_entry =
+ let ty =
+ CicTypeChecker.type_of_aux' metasenv context term
+ in
+ Some (n_to_clear_body, Cic.Decl ty)
+ in
+ cleared_entry::context
+ | None -> None::context
+ | Some (n,C.Decl t)
+ | Some (n,C.Def t) ->
+ let _ =
+ try
+ CicTypeChecker.type_of_aux' metasenv context t
+ with
+ _ ->
+ raise
+ (Fail
+ ("The correctness of hypothesis " ^
+ string_of_name n ^
+ " relies on the body of " ^
+ string_of_name n_to_clear_body)
+ )
+ in
+ entry::context
+ ) canonical_context []
+ in
+ let _ =
+ try
+ CicTypeChecker.type_of_aux' metasenv canonical_context' ty
+ with
+ _ ->
+ raise
+ (Fail
+ ("The correctness of the goal relies on the body of " ^
+ string_of_name n_to_clear_body))
+ in
+ m,canonical_context',ty
+ | t -> t
+ ) metasenv
+ in
+ proof := Some (curi,metasenv',pbo,pty)
+;;
+
+let clear hyp_to_clear =
+ let module C = Cic in
+ match hyp_to_clear with
+ None -> assert false
+ | Some (n_to_clear, _) ->
+ let curi,metasenv,pbo,pty =
+ match !proof with
+ None -> assert false
+ | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
+ in
+ let metano,context,ty =
+ match !goal with
+ None -> assert false
+ | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
+ in
+ let string_of_name =
+ function
+ C.Name n -> n
+ | C.Anonimous -> "_"
+ in
+ let metasenv' =
+ List.map
+ (function
+ (m,canonical_context,ty) when m = metano ->
+ let canonical_context' =
+ List.fold_right
+ (fun entry context ->
+ match entry with
+ t when t == hyp_to_clear -> None::context
+ | None -> None::context
+ | Some (n,C.Decl t)
+ | Some (n,C.Def t) ->
+ let _ =
+ try
+ CicTypeChecker.type_of_aux' metasenv context t
+ with
+ _ ->
+ raise
+ (Fail
+ ("Hypothesis " ^
+ string_of_name n ^
+ " uses hypothesis " ^
+ string_of_name n_to_clear)
+ )
+ in
+ entry::context
+ ) canonical_context []
+ in
+ let _ =
+ try
+ CicTypeChecker.type_of_aux' metasenv canonical_context' ty
+ with
+ _ ->
+ raise
+ (Fail
+ ("Hypothesis " ^ string_of_name n_to_clear ^
+ " occurs in the goal"))
+ in
+ m,canonical_context',ty
+ | t -> t
+ ) metasenv
+ in
+ proof := Some (curi,metasenv',pbo,pty)
+;;
projects / helm.git / commitdiff