From cbf6c7edd81459a9f22a5a8b5377b4f53297fd60 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 18 Apr 2002 08:57:10 +0000 Subject: [PATCH] * Many improvements * The interface now gives the user the possibility of (re-)opening an existing constant. * Tactic Elim no more exposed in the user interface. Replaced by ElimIntros. * Selection of subterms in the hypothesis of the goal is now "sound". * Reduction tactics (Whd, Reduce, Simpl) now work also on the hypothesis. New bug/feature: their changes are lost when moving to another goal and coming back afterwards. --- helm/gTopLevel/gTopLevel.ml | 54 ++++++++++++++--- helm/gTopLevel/proofEngine.ml | 83 ++++++++++++-------------- helm/gTopLevel/proofEngineReduction.ml | 6 +- helm/gTopLevel/sequentPp.ml | 61 ++++++++++--------- 4 files changed, 122 insertions(+), 82 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 0cfccab99..5726f3d8c 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -399,8 +399,8 @@ let exact rendering_window = let apply rendering_window = call_tactic_with_input ProofEngine.apply rendering_window ;; -let elim rendering_window = - call_tactic_with_input ProofEngine.elim rendering_window +let elimintros rendering_window = + call_tactic_with_input ProofEngine.elim_intros rendering_window ;; let whd rendering_window = call_tactic_with_goal_input ProofEngine.whd rendering_window @@ -486,6 +486,40 @@ let proveit rendering_window () = | None -> assert false (* "ERROR: No selection!!!" *) ;; +exception NotADefinition;; + +let open_ rendering_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 + let inputlen = inputt#length in + let input = inputt#get_chars 0 inputlen ^ "\n" in + try + let uri = UriManager.uri_of_string ("cic:" ^ input) in + CicTypeChecker.typecheck uri ; + let metasenv,bo,ty = + match CicEnvironment.get_cooked_obj uri 0 with + Cic.Definition (_,bo,ty,_) -> [],bo,ty + | Cic.CurrentProof (_,metasenv,bo,ty) -> metasenv,bo,ty + | Cic.Axiom _ + | Cic.Variable _ + | Cic.InductiveDefinition _ -> raise NotADefinition + in + 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 ; + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; +;; + let state rendering_window () = let inputt = (rendering_window#inputt : GEdit.text) in let oldinputt = (rendering_window#oldinputt : GEdit.text) in @@ -518,7 +552,7 @@ let state rendering_window () = with CicTextualParser0.Eof -> inputt#delete_text 0 inputlen ; - ignore(oldinputt#insert_text input oldinputt#length) ; + ignore(oldinputt#insert_text input oldinputt#length) | e -> print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout ;; @@ -703,9 +737,14 @@ class rendering_window output proofw (label : GMisc.label) = ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180 ~packing:(vbox#pack ~padding:5) () in + let hbox4 = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let stateb = GButton.button ~label:"State" - ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let openb = + GButton.button ~label:"Open" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let inputt = GEdit.text ~editable:true ~width:400 ~height: 100 ~packing:(vbox#pack ~padding:5) () in let vbox1 = @@ -725,8 +764,8 @@ class rendering_window output proofw (label : GMisc.label) = let applyb = GButton.button ~label:"Apply" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let elimb = - GButton.button ~label:"Elim" + let elimintrosb = + GButton.button ~label:"ElimIntros" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let whdb = GButton.button ~label:"Whd" @@ -775,9 +814,10 @@ object(self) ignore(proveitb#connect#clicked (proveit self)) ; ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ; ignore(stateb#connect#clicked (state self)) ; + ignore(openb#connect#clicked (open_ self)) ; ignore(exactb#connect#clicked (exact self)) ; ignore(applyb#connect#clicked (apply self)) ; - ignore(elimb#connect#clicked (elim self)) ; + ignore(elimintrosb#connect#clicked (elimintros self)) ; ignore(whdb#connect#clicked (whd self)) ; ignore(reduceb#connect#clicked (reduce self)) ; ignore(simplb#connect#clicked (simpl self)) ; diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 60baf8e59..90d189981 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -539,6 +539,11 @@ prerr_endline "dopo refine meta" ; flush stdout ; | [] -> goal := None ;; +let elim_intros term = + elim term ; + intros () +;; + let reduction_tactic reduction_function term = let curi,metasenv,pbo,pty = match !proof with @@ -551,47 +556,27 @@ let reduction_tactic reduction_function term = | Some (metano,(context,ty)) -> metano,context,ty in let term' = reduction_function term in - let ty' = ProofEngineReduction.replace term term' ty in - let metasenv' = - List.map - (function - (n,_) when n = metano -> (metano,ty') - | _ as t -> t - ) metasenv - in - proof := Some (curi,metasenv',pbo,pty) ; - goal := Some (metano,(context,ty')) + (* 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 ~what:term ~with_what:term' in + let ty' = replace ty in + let context' = List.map (function (bt,n,t) -> bt,n,replace t) context in + let metasenv' = + List.map + (function + (n,_) when n = metano -> (metano,ty') + | _ as t -> t + ) metasenv + in + proof := Some (curi,metasenv',pbo,pty) ; + goal := Some (metano,(context',ty')) ;; let whd = reduction_tactic CicReduction.whd;; let reduce = reduction_tactic ProofEngineReduction.reduce;; -(* let simpl = reduction_tactic ProofEngineReduction.simpl;; -*) - -let simpl term = - 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,(context,ty)) -> metano,context,ty - in - let term' = ProofEngineReduction.simpl term in - let ty' = ProofEngineReduction.replace term term' ty in - let metasenv' = - List.map - (function - (n,_) when n = metano -> (metano,ty') - | _ as t -> t - ) metasenv - in - proof := Some (curi,metasenv',pbo,pty) ; - goal := Some (metano,(context,ty')) -;; (* It is just the opposite of whd. The code should probably be merged. *) let fold term = @@ -606,16 +591,22 @@ let fold term = | Some (metano,(context,ty)) -> metano,context,ty in let term' = CicReduction.whd term in - let ty' = ProofEngineReduction.replace term' term ty in - let metasenv' = - List.map - (function - (n,_) when n = metano -> (metano,ty') - | _ as t -> t - ) metasenv - in - proof := Some (curi,metasenv',pbo,pty) ; - goal := Some (metano,(context,ty')) + (* 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 ~what:term' ~with_what:term in + let ty' = replace ty in + let context' = List.map (function (bt,n,t) -> bt,n,replace t) context in + let metasenv' = + List.map + (function + (n,_) when n = metano -> (metano,ty') + | _ as t -> t + ) metasenv + in + proof := Some (curi,metasenv',pbo,pty) ; + goal := Some (metano,(context',ty')) ;; let cut term = diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index 52f07e4dc..9771b7d82 100644 --- a/helm/gTopLevel/proofEngineReduction.ml +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -59,7 +59,11 @@ let replace ~what ~with_what ~where = | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t) | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t) | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t) - | C.Appl l -> C.Appl (List.map aux l) + | C.Appl l -> + (* Invariant enforced: no application of an application *) + (match List.map aux l with + (C.Appl l')::tl -> C.Appl (l'@tl) + | l' -> C.Appl l') | C.Const _ as t -> t | C.Abst _ as t -> t | C.MutInd _ as t -> t diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml index a30f44d5a..7bdfeb5c3 100644 --- a/helm/gTopLevel/sequentPp.ml +++ b/helm/gTopLevel/sequentPp.ml @@ -40,35 +40,40 @@ module XmlPp = struct let print_sequent metasenv (context,goal) = let module X = Xml in - let final_s,final_env = - (List.fold_right - (fun (b,n,t) (s,env) -> - let (acic,_,_,ids_to_inner_sorts,_) = - Cic2acic.acic_of_cic_env metasenv env t - in - [< s ; - X.xml_nempty - (match b with - ProofEngine.Definition -> "Def" - | ProofEngine.Declaration -> "Decl" - ) ["name",(match n with Cic.Name n -> n | _ -> assert false)] - (Cic2Xml.print_term - (UriManager.uri_of_string "cic:/dummy.con") - ids_to_inner_sorts acic) - >],((n,t)::env) (* CSC: sbagliato!!! Giusto solo se Declaration! *) - ) context ([<>],[]) - ) - in - let (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,_) = - Cic2acic.acic_of_cic_env metasenv final_env goal + let ids_to_terms = Hashtbl.create 503 in + let ids_to_father_ids = Hashtbl.create 503 in + let ids_to_inner_sorts = Hashtbl.create 503 in + let ids_to_inner_types = Hashtbl.create 503 in + let seed = ref 0 in + let acic_of_cic_env = + Cic2acic.acic_of_cic_env' seed ids_to_terms ids_to_father_ids + ids_to_inner_sorts ids_to_inner_types metasenv in - X.xml_nempty "Sequent" [] - [< final_s ; - Xml.xml_nempty "Goal" [] - (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con") - ids_to_inner_sorts acic) - >], - ids_to_terms,ids_to_father_ids + let final_s,final_env = + (List.fold_right + (fun (b,n,t) (s,env) -> + let acic = acic_of_cic_env env t in + [< s ; + X.xml_nempty + (match b with + ProofEngine.Definition -> "Def" + | ProofEngine.Declaration -> "Decl" + ) ["name",(match n with Cic.Name n -> n | _ -> assert false)] + (Cic2Xml.print_term + (UriManager.uri_of_string "cic:/dummy.con") + ids_to_inner_sorts acic) + >],((n,t)::env) (* CSC: sbagliato!!! Giusto solo se Declaration! *) + ) context ([<>],[]) + ) + in + let acic = acic_of_cic_env final_env goal in + X.xml_nempty "Sequent" [] + [< final_s ; + Xml.xml_nempty "Goal" [] + (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con") + ids_to_inner_sorts acic) + >], + ids_to_terms,ids_to_father_ids ;; end ;; -- 2.39.2