From 5dac9432fa233251332953770319c0b95984e1c5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 11 Oct 2002 17:58:37 +0000 Subject: [PATCH] - rewrite extended to handle rewritings with eqT - equality_replace implemented (based on the new rewriting tactic) --- helm/gTopLevel/Makefile | 2 +- helm/gTopLevel/fourierR.ml | 53 +++++++++++++++++++------------------- 2 files changed, 27 insertions(+), 28 deletions(-) diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index f0ec4bfce..403b8b180 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -2,7 +2,7 @@ BIN_DIR = /usr/local/bin REQUIRES = lablgtkmathview helm-cic_textual_parser helm-cic_proof_checking \ helm-xml gdome2-xslt helm-cic_unification helm-mathql \ helm-mathql_interpreter -PREDICATES = +PREDICATES = "gnome,init" OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index b9e782330..d2725ff15 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -31,11 +31,22 @@ let rewrite_tac ~term:equality ~status:(proof,goal) = let module U = UriManager in let curi,metasenv,pbo,pty = proof in let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in - let ty,t1,t2 = + let eq_ind_r,ty,t1,t2 = match CicTypeChecker.type_of_aux' metasenv context equality with C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2] when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind") -> - ty,t1,t2 + let eq_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con",0) + in + eq_ind_r,ty,t1,t2 + | C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") -> + let eqT_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",0) + in + eqT_ind_r,ty,t1,t2 | _ -> raise (ProofEngineTypes.Fail @@ -51,16 +62,7 @@ let rewrite_tac ~term:equality ~status:(proof,goal) = in C.Lambda (C.Name "dummy_for_rewrite", ty, gty'') in -prerr_endline ("##### Atteso: " ^ CicPp.ppterm - (C.Lambda (C.Name "x", ty, - C.Appl - [C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind",0,0) ; - ty ; C.Rel 3 ; C.Rel 1])) -) ; prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); - let eq_ind_r = - C.Const - (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con",0) in let fresh_meta = ProofEngineHelpers.new_meta proof in let irl = ProofEngineHelpers.identity_relocation_list_for_metavariable context in @@ -477,6 +479,7 @@ i.e. on obtient une contradiction. *) +let _eqT = Cic.MutInd(UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") 0 0 ;; let _False = Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 0 ;; let _not = Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con") 0;; let _R0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;; @@ -770,23 +773,21 @@ let rec superlift c n= ;; -(* fix !!!!!!!!!! this may not work *) let equality_replace a b ~status = + let module C = Cic in let proof,goal = status in let curi,metasenv,pbo,pty = proof in let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in -prerr_endline (" " ^ CicPp.ppterm b) ; -prerr_endline ("### IN MY_CUT: ") ; -prerr_endline ("@ " ^ CicPp.ppterm ty) ; -List.iter (function Some (n,Cic.Decl t) -> prerr_endline ("# " ^ CicPp.ppterm t)) context ; -prerr_endline ("##- IN MY_CUT ") ; -let res = - let _eqT_ind = Cic.Const( UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con" ) 0 in -(*CSC: codice ad-hoc per questo caso!!! Non funge in generale *) - PrimitiveTactics.apply_tac ~term:(Cic.Appl [_eqT_ind;_R;b;Cic.Lambda(Cic.Name "pippo",_R,Cic.Appl [_not; Cic.Appl [_Rlt;_R0;Cic.Rel 1]])]) ~status -in -prerr_endline "EUREKA" ; -res + let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in + let (proof,goals) = + rewrite_tac ~term:(C.Meta (fresh_meta,irl)) + ~status:((curi,metasenv',pbo,pty),goal) + in + (proof,fresh_meta::goals) ;; let tcl_fail a ~status:(proof,goal) = @@ -1032,8 +1033,6 @@ let rec fourier ~status:(s_proof,s_goal)= ~continuation:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:(if sres then _Rnot_lt_lt else _Rnot_le_le)) - ~continuation:Ring.id_tac -(*CSC ~continuation:(Tacticals.thens ~start:(equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc) ~continuations:[tac2;(Tacticals.thens @@ -1051,7 +1050,7 @@ let rec fourier ~status:(s_proof,s_goal)= ) ] (* end continuations before comment *) - ) *) + ) ); !tac1] );(*end tac:=*) -- 2.39.2