From 9b5c1945c6d3af81f07c41da187404c2431cefa3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 26 Apr 2002 10:37:40 +0000 Subject: [PATCH] * Many improvements (expecially in exceptions handling) * The cases in which existential variables are now handled "correctly" have been increased. Neverthless, existential variables are still implemented in a completely wrong way. * First commit after the commit of cic_unification. --- helm/gTopLevel/gTopLevel.ml | 173 +++++++++++++++++++++++++--------- helm/gTopLevel/proofEngine.ml | 68 ++++++++++--- 2 files changed, 183 insertions(+), 58 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 268d2846e..f6556ed8c 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -165,50 +165,60 @@ let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types = (* 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 = @@ -256,11 +266,26 @@ let call_tactic tactic rendering_window () = refresh_sequent proofw ; refresh_proof output with - e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; + RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw ; + refresh_proof output + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; end ;; @@ -304,11 +329,33 @@ let call_tactic_with_input tactic rendering_window () = with CicTextualParser0.Eof -> inputt#delete_text 0 inputlen + | RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") ; +prerr_endline "PROVA CHE FA SOLLEVARE UN'ECCEZIONE:" ; flush stderr ; +begin +match !ProofEngine.proof with Some (_,metasenv,bo,_) -> +List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ +CicPp.ppterm ty) ; flush stderr) metasenv ; +prerr_endline ("PROOF: " ^ CicPp.ppterm bo) ; flush stderr ; +end ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw ; + refresh_proof output | e -> output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

"); + ("

" ^ Printexc.to_string e ^ "

") ; ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal + ProofEngine.goal := savedgoal ; ;; let call_tactic_with_goal_input tactic rendering_window () = @@ -338,9 +385,26 @@ 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 - ("

" ^ Printexc.to_string e ^ "

") + RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw ; + refresh_proof output + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; end | None -> output_html outputhtml @@ -409,9 +473,26 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () = end | None -> assert false (* "ERROR: No current term!!!" *) with - e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") + RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw ; + refresh_proof output + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; end | None -> output_html outputhtml diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 5f64134b5..ac828a959 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -28,7 +28,21 @@ let cic_context_of_named_context = ) ;; -let refine_meta_with_brand_new_metasenv meta term newmetasenv = +(* refine_meta_with_brand_new_metasenv meta term apply_subst_replacing *) +(* newmetasenv *) +(* This (heavy) function must be called when a tactic can instantiate old *) +(* metavariables (i.e. existential variables). It substitues the metasenv *) +(* of the proof with the result of removing [meta] from the domain of *) +(* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *) +(* in the current proof. Finally it applies [apply_subst_replacing] to *) +(* current proof. *) +(*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *) +(*CSC: ci ripasso sopra apply_subst!!! *) +(*CSC: Inoltre, potrebbe essere questa funzione ad applicare apply_subst a *) +(*CSC: newmetasenv!!! *) +let refine_meta_with_brand_new_metasenv meta term apply_subst_replacing + newmetasenv += let (uri,bo,ty) = match !proof with None -> assert false @@ -37,7 +51,7 @@ let refine_meta_with_brand_new_metasenv meta term newmetasenv = let subst_in t = ProofEngineReduction.replace ~what:(Cic.Meta meta) ~with_what:term ~where:t in - let bo' = subst_in bo in + let bo' = apply_subst_replacing (subst_in bo) in let metasenv' = List.remove_assoc meta newmetasenv in proof := Some (uri,metasenv',bo',ty) ;; @@ -236,9 +250,9 @@ let new_metasenv_for_apply ty = ;; (*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *) -let classify_metas newmeta in_subst_domain apply_subst = - List.fold_left - (fun (old_uninst,new_uninst) (i,ty) -> +let classify_metas newmeta in_subst_domain apply_subst metasenv = + List.fold_right + (fun (i,ty) (old_uninst,new_uninst) -> if in_subst_domain i then old_uninst,new_uninst else @@ -247,7 +261,7 @@ let classify_metas newmeta in_subst_domain apply_subst = ((i,ty')::old_uninst),new_uninst else old_uninst,((i,ty')::new_uninst) - ) ([],[]) + ) metasenv ([],[]) ;; (* The term bo must be closed in the current context *) @@ -276,6 +290,14 @@ let apply term = let subst = CicUnification.fo_unif newmetasenv ciccontext consthead ty in let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in let apply_subst = CicUnification.apply_subst subst in +(*CSC: estremamente inefficiente: fare una passata sola per rimpiazzarle tutte*) + let apply_subst_replacing t = + List.fold_left + (fun t (i,bo) -> + ProofEngineReduction.replace + ~what:(Cic.Meta i) ~with_what:bo ~where:t) + t subst + in let old_uninstantiatedmetas,new_uninstantiatedmetas = classify_metas newmeta in_subst_domain apply_subst newmetasenv in @@ -289,11 +311,18 @@ let apply term = in Cic.Appl (term::arguments) in - refine_meta_with_brand_new_metasenv metano bo' + refine_meta_with_brand_new_metasenv metano bo' apply_subst_replacing (new_uninstantiatedmetas@old_uninstantiatedmetas) ; +prerr_endline "QUI4" ; flush stderr ; ( match new_uninstantiatedmetas with [] -> goal := None | (i,ty)::_ -> goal := Some (i,(context,ty)) +) ; +List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm ty) ; flush stderr) (new_uninstantiatedmetas@old_uninstantiatedmetas) +; prerr_endline "FATTO" ; flush stderr ; +List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm ty) ; flush stderr) (match !proof with Some (_,m,_,_) -> m) ; +prerr_endline ("PROVA: " ^ CicPp.ppterm (match !proof with Some (_,_,b,_) -> b)) +; prerr_endline "FATTO2" ; flush stderr ;; let eta_expand metasenv ciccontext t arg = @@ -449,11 +478,25 @@ prerr_endline "unwind"; flush stderr; (* When unwinding the META that corresponds to the elimination *) (* predicate (which is emeta), we must also perform one-step *) (* beta-reduction. *) - let apply_subst = - function t -> - let t' = CicUnification.apply_subst subst1 t in - CicUnification.apply_subst_reducing - subst2 (Some (emeta,List.length fargs)) t' + let apply_subst t = + let t' = CicUnification.apply_subst subst1 t in + CicUnification.apply_subst_reducing + subst2 (Some (emeta,List.length fargs)) t' + in +(*CSC: estremamente inefficiente: fare una passata sola per rimpiazzarle tutte*) + let apply_subst_replacing t = + let t' = + List.fold_left + (fun t (i,bo) -> + ProofEngineReduction.replace + ~what:(Cic.Meta i) ~with_what:bo ~where:t) + t subst1 + in + List.fold_left + (fun t (i,bo) -> + ProofEngineReduction.replace + ~what:(Cic.Meta i) ~with_what:bo ~where:t) + t' subst2 in let newmetasenv' = List.map (function (i,ty) -> i, apply_subst ty) newmetasenv @@ -469,6 +512,7 @@ prerr_endline "unwind"; flush stderr; prerr_endline ("BODY': " ^ CicPp.ppterm bo') ; flush stdout ; List.iter (function (i,t) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm t)) (new_uninstantiatedmetas@old_uninstantiatedmetas) ; flush stderr ; refine_meta_with_brand_new_metasenv metano bo' + apply_subst_replacing (new_uninstantiatedmetas@old_uninstantiatedmetas) ; match new_uninstantiatedmetas with [] -> goal := None -- 2.39.2