From dfa0ff915fcf79a3ef9d45b74303175ba2e49d13 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 28 Jan 2003 10:22:00 +0000 Subject: [PATCH] moved tactics in ocaml/tactics --- helm/gTopLevel/eliminationTactics.ml | 220 --- helm/gTopLevel/eliminationTactics.mli | 33 - helm/gTopLevel/equalityTactics.ml | 238 --- helm/gTopLevel/equalityTactics.mli | 35 - helm/gTopLevel/fourier.ml | 244 ---- helm/gTopLevel/fourierR.ml | 1297 ----------------- helm/gTopLevel/fourierR.mli | 5 - helm/gTopLevel/introductionTactics.ml | 59 - helm/gTopLevel/introductionTactics.mli | 31 - helm/gTopLevel/negationTactics.ml | 71 - helm/gTopLevel/negationTactics.mli | 28 - helm/gTopLevel/primitiveTactics.ml | 548 ------- helm/gTopLevel/primitiveTactics.mli | 41 - helm/gTopLevel/proofEngineHelpers.ml | 122 -- helm/gTopLevel/proofEngineHelpers.mli | 45 - helm/gTopLevel/proofEngineReduction.ml | 826 ----------- helm/gTopLevel/proofEngineReduction.mli | 47 - helm/gTopLevel/proofEngineStructuralRules.ml | 149 -- helm/gTopLevel/proofEngineStructuralRules.mli | 27 - helm/gTopLevel/proofEngineTypes.ml | 41 - helm/gTopLevel/reductionTactics.ml | 127 -- helm/gTopLevel/reductionTactics.mli | 36 - helm/gTopLevel/ring.ml | 594 -------- helm/gTopLevel/ring.mli | 12 - helm/gTopLevel/tacticals.ml | 249 ---- helm/gTopLevel/tacticals.mli | 61 - helm/gTopLevel/variousTactics.ml | 206 --- helm/gTopLevel/variousTactics.mli | 34 - 28 files changed, 5426 deletions(-) delete mode 100644 helm/gTopLevel/eliminationTactics.ml delete mode 100644 helm/gTopLevel/eliminationTactics.mli delete mode 100644 helm/gTopLevel/equalityTactics.ml delete mode 100644 helm/gTopLevel/equalityTactics.mli delete mode 100644 helm/gTopLevel/fourier.ml delete mode 100644 helm/gTopLevel/fourierR.ml delete mode 100644 helm/gTopLevel/fourierR.mli delete mode 100644 helm/gTopLevel/introductionTactics.ml delete mode 100644 helm/gTopLevel/introductionTactics.mli delete mode 100644 helm/gTopLevel/negationTactics.ml delete mode 100644 helm/gTopLevel/negationTactics.mli delete mode 100644 helm/gTopLevel/primitiveTactics.ml delete mode 100644 helm/gTopLevel/primitiveTactics.mli delete mode 100644 helm/gTopLevel/proofEngineHelpers.ml delete mode 100644 helm/gTopLevel/proofEngineHelpers.mli delete mode 100644 helm/gTopLevel/proofEngineReduction.ml delete mode 100644 helm/gTopLevel/proofEngineReduction.mli delete mode 100644 helm/gTopLevel/proofEngineStructuralRules.ml delete mode 100644 helm/gTopLevel/proofEngineStructuralRules.mli delete mode 100644 helm/gTopLevel/proofEngineTypes.ml delete mode 100644 helm/gTopLevel/reductionTactics.ml delete mode 100644 helm/gTopLevel/reductionTactics.mli delete mode 100644 helm/gTopLevel/ring.ml delete mode 100644 helm/gTopLevel/ring.mli delete mode 100644 helm/gTopLevel/tacticals.ml delete mode 100644 helm/gTopLevel/tacticals.mli delete mode 100644 helm/gTopLevel/variousTactics.ml delete mode 100644 helm/gTopLevel/variousTactics.mli diff --git a/helm/gTopLevel/eliminationTactics.ml b/helm/gTopLevel/eliminationTactics.ml deleted file mode 100644 index fc6906cbc..000000000 --- a/helm/gTopLevel/eliminationTactics.ml +++ /dev/null @@ -1,220 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* -let induction_tac ~term ~status:((proof,goal) as status) = - let module C = Cic in - let module R = CicReduction in - let module P = PrimitiveTactics in - let module T = Tacticals in - let module S = ProofEngineStructuralRules in - let module U = UriManager in - let (_,metasenv,_,_) = proof in - let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let termty = CicTypeChecker.type_of_aux' metasenv context term in (* per ora non serve *) - - T.then_ ~start:(T.repeat_tactic - ~tactic:(T.then_ ~start:(VariousTactics.generalize_tac ~term) (* chissa' se cosi' funziona? *) - ~continuation:(P.intros)) - ~continuation:(P.elim_intros_simpl ~term) - ~status -;; -*) - - -let elim_type_tac ~term ~status = - let module C = Cic in - let module P = PrimitiveTactics in - let module T = Tacticals in - T.thens - ~start: (P.cut_tac ~term) - ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ] - ~status -;; - -(* Questa era gia' in ring.ml!!!! NB: adesso in ring non c'e' piu' :-) -let elim_type_tac ~term ~status = - warn "in Ring.elim_type_tac"; - Tacticals.thens ~start:(cut_tac ~term) - ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status -*) - - -(* PROVE DI DECOMPOSE *) -(* guardare quali sono i tipi induttivi decomponibili presenti in -profondita' nel term; chiamare una funzione di call-back passando questa -lista e ritornando la lista di termini che l'utente vuole decomporre; -decomporre. *) - - -exception InteractiveUserUriChoiceNotRegistered - -let interactive_user_uri_choice = - (ref (fun ~selection_mode -> raise InteractiveUserUriChoiceNotRegistered) : - (selection_mode:[`SINGLE | `EXTENDED] -> - ?ok:string -> - ?enable_button_for_non_vars:bool -> - title:string -> msg:string -> string list -> string list) ref) -;; - -exception IllFormedUri of string - -let cic_textual_parser_uri_of_string uri' = - try - (* Constant *) - if String.sub uri' (String.length uri' - 4) 4 = ".con" then - CicTextualParser0.ConUri (UriManager.uri_of_string uri') - else - if String.sub uri' (String.length uri' - 4) 4 = ".var" then - CicTextualParser0.VarUri (UriManager.uri_of_string uri') - else - (try - (* Inductive Type *) - let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in - CicTextualParser0.IndTyUri (uri'',typeno) - with - _ -> - (* Constructor of an Inductive Type *) - let uri'',typeno,consno = - CicTextualLexer.indconuri_of_uri uri' - in - CicTextualParser0.IndConUri (uri'',typeno,consno) - ) - with - _ -> raise (IllFormedUri uri') -;; - -let constructor_uri_of_string uri = - match cic_textual_parser_uri_of_string uri with - CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[]) - | _ -> assert false -;; - -let call_back uris = -(* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *) - let module U = UriManager in - List.map - (constructor_uri_of_string) - (!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) - ) -;; - - -let decompose_tac ~term ~status:((proof,goal) as status) = - let module C = Cic in - let module R = CicReduction in - let module P = PrimitiveTactics in - let module T = Tacticals in - let module S = ProofEngineStructuralRules in - let _,metasenv,_,_ = proof in - let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let old_context_len = List.length context in -(* let nr_of_hyp_still_to_elim = ref 1 in *) - let termty = CicTypeChecker.type_of_aux' metasenv context term in - - let rec make_list termty = -(* altamente inefficente? *) - let rec search_inductive_types urilist termty = - (* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *) - match termty with - (C.MutInd (uri,typeno,exp_named_subst)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) -> - (uri,typeno,exp_named_subst)::urilist - | (C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::applist)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) -> - (uri,typeno,exp_named_subst)::(List.fold_left search_inductive_types urilist applist) - | _ -> urilist - (* N.B: in un caso tipo (and A !C:Prop.(or B C)) l'or *non* viene selezionato! *) - in - let rec purge_duplicates urilist = - let rec aux triple urilist = - match urilist with - [] -> [] - | hd::tl -> - if (hd = triple) - then aux triple tl - else hd::(aux triple tl) - in - match urilist with - [] -> [] - | hd::tl -> hd::(purge_duplicates (aux hd tl)) - in - purge_duplicates (search_inductive_types [] termty) - in - - let urilist = - (* list of triples (uri,typeno,exp_named_subst) of Inductive Types found in term and chosen by the user *) - (* N.B.: due to a bug in call_back exp_named_subst are not significant (they all are []) *) - call_back (make_list termty) in - - let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim ~status:((proof,goal) as status) = -prerr_endline ("%%%%%%% nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim)); - if nr_of_hyp_still_to_elim <> 0 then - let _,metasenv,_,_ = proof in - let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in - let old_context_len = List.length context in - let termty = CicTypeChecker.type_of_aux' metasenv context term' in -prerr_endline ("%%%%%%% elim_clear termty= " ^ CicPp.ppterm termty); - match termty with - C.MutInd (uri,typeno,exp_named_subst) - | C.Appl((C.MutInd (uri,typeno,exp_named_subst))::_) - when (List.mem (uri,typeno,exp_named_subst) urilist) -> -prerr_endline ("%%%%%%% elim " ^ CicPp.ppterm termty); - T.then_ - ~start:(P.elim_intros_simpl_tac ~term:term') - ~continuation:( - (* clear the hyp that has just been eliminated *) - (fun ~status:((proof,goal) as status) -> - let _,metasenv,_,_ = proof in - let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in - let new_context_len = List.length context in -prerr_endline ("%%%%%%% newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim)); - let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim + (new_context_len - old_context_len) - 1 in - T.then_ - ~start:( - if (term'==term) (* this is the first application of elim: there's no need to clear the hyp *) - then begin prerr_endline ("%%%%%%% no clear"); T.id_tac end - else begin prerr_endline ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:(List.nth context (new_nr_of_hyp_still_to_elim))) end) - ~continuation:(elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim) - ~status - )) - ~status - | _ -> - let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim - 1 in -prerr_endline ("%%%%%%% fail; hyp=" ^ (string_of_int new_nr_of_hyp_still_to_elim)); - elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim ~status - else (* raise (ProofEngineTypes.Fail "Decomopse: finished decomposing"); *) T.id_tac ~status - - in -(* T.repeat_tactic ~tactic: *) - (elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1) - ~status -;; - - - diff --git a/helm/gTopLevel/eliminationTactics.mli b/helm/gTopLevel/eliminationTactics.mli deleted file mode 100644 index a49c77158..000000000 --- a/helm/gTopLevel/eliminationTactics.mli +++ /dev/null @@ -1,33 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -val elim_type_tac: term:Cic.term -> ProofEngineTypes.tactic - -val interactive_user_uri_choice: ( selection_mode:[`SINGLE | `EXTENDED] -> - ?ok:string -> - ?enable_button_for_non_vars:bool -> - title:string -> msg:string -> string list -> string list) ref - -val decompose_tac: term:Cic.term -> ProofEngineTypes.tactic diff --git a/helm/gTopLevel/equalityTactics.ml b/helm/gTopLevel/equalityTactics.ml deleted file mode 100644 index 79b5b1dbe..000000000 --- a/helm/gTopLevel/equalityTactics.ml +++ /dev/null @@ -1,238 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - - -let rewrite_tac ~term:equality ~status:(proof,goal) = - let module C = Cic in - 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 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/eq.ind") -> - let eq_ind_r = - C.Const - (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[]) - 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",[]) - in - eqT_ind_r,ty,t1,t2 - | _ -> - raise - (ProofEngineTypes.Fail - "Rewrite: the argument is not a proof of an equality") - in - let pred = - let gty' = CicSubstitution.lift 1 gty in - let t1' = CicSubstitution.lift 1 t1 in - let gty'' = - ProofEngineReduction.replace_lifting - ~equality:ProofEngineReduction.alpha_equivalence - ~what:t1' ~with_what:(C.Rel 1) ~where:gty' - in - C.Lambda (C.Name "dummy_for_rewrite", ty, gty'') - in -prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); - let fresh_meta = ProofEngineHelpers.new_meta proof in - let irl = - ProofEngineHelpers.identity_relocation_list_for_metavariable context in - let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in - - let (proof',goals) = - PrimitiveTactics.exact_tac - ~term:(C.Appl - [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]) - ~status:((curi,metasenv',pbo,pty),goal) - in - assert (List.length goals = 0) ; - (proof',[fresh_meta]) -;; - - -let rewrite_simpl_tac ~term ~status = - Tacticals.then_ - ~start:(rewrite_tac ~term) - ~continuation: - (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) - ~status -;; - - -let rewrite_back_tac ~term:equality ~status:(proof,goal) = - let module C = Cic in - 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 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/eq.ind") -> - let eq_ind_r = - C.Const - (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind.con",[]) - in - eq_ind_r,ty,t2,t1 - | 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.con",[]) - in - eqT_ind_r,ty,t2,t1 - | _ -> - raise - (ProofEngineTypes.Fail - "Rewrite: the argument is not a proof of an equality") - in - let pred = - let gty' = CicSubstitution.lift 1 gty in - let t1' = CicSubstitution.lift 1 t1 in - let gty'' = - ProofEngineReduction.replace_lifting - ~equality:ProofEngineReduction.alpha_equivalence - ~what:t1' ~with_what:(C.Rel 1) ~where:gty' - in - C.Lambda (C.Name "dummy_for_rewrite", ty, gty'') - in -prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); - let fresh_meta = ProofEngineHelpers.new_meta proof in - let irl = - ProofEngineHelpers.identity_relocation_list_for_metavariable context in - let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in - - let (proof',goals) = - PrimitiveTactics.exact_tac - ~term:(C.Appl - [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]) - ~status:((curi,metasenv',pbo,pty),goal) - in - assert (List.length goals = 0) ; - (proof',[fresh_meta]) - -;; - - -let rewrite_back_simpl_tac ~term ~status = - Tacticals.then_ - ~start:(rewrite_back_tac ~term) - ~continuation: - (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) - ~status -;; - - -let replace_tac ~what ~with_what ~status:((proof, goal) as status) = - let module C = Cic in - let module U = UriManager in - let module P = PrimitiveTactics in - let module T = Tacticals in - let _,metasenv,_,_ = proof in - let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in - let wty = CicTypeChecker.type_of_aux' metasenv context what in - try - if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what)) - then T.thens - ~start:( - P.cut_tac - ~term:( - C.Appl [ - (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 0, [])) ; (* quale uguaglianza usare, eq o eqT ? *) - wty ; - what ; - with_what])) - ~continuations:[ - T.then_ - ~start:(rewrite_back_tac ~term:(C.Rel 1)) (* C.Name "dummy_for_replace" *) - ~continuation:( - ProofEngineStructuralRules.clear - ~hyp:(List.hd context)) ; -(* (Some(C.Name "dummy_for_replace" , C.Def (CicTypeChecker.type_of_aux' metasenv context (C.Rel 1)) (* NOOOO!!!!! tipo di dummy *) )))) ; *) - T.id_tac] - ~status - else raise (ProofEngineTypes.Fail "Replace: terms not replaceable") - with (Failure "hd") -> raise (ProofEngineTypes.Fail "Replace: empty context") -;; - - -(* All these tacs do is applying the right constructor/theorem *) - -let reflexivity_tac = - IntroductionTactics.constructor_tac ~n:1 -;; - - -let symmetry_tac ~status:(proof, goal) = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let (_,metasenv,_,_) = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - match (R.whd context ty) with - (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> - PrimitiveTactics.apply_tac ~status:(proof,goal) - ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/sym_eq.con", [])) - - | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> - PrimitiveTactics.apply_tac ~status:(proof,goal) - ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con", [])) - - | _ -> raise (ProofEngineTypes.Fail "Symmetry failed") -;; - - -let transitivity_tac ~term ~status:((proof, goal) as status) = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let module T = Tacticals in - let (_,metasenv,_,_) = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - match (R.whd context ty) with - (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> - T.thens - ~start:(PrimitiveTactics.apply_tac - ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con", []))) - ~continuations: - [PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac] - ~status - - | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> - T.thens - ~start:(PrimitiveTactics.apply_tac - ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/trans_eqT.con", []))) - ~continuations: - [T.id_tac ; T.id_tac ; PrimitiveTactics.exact_tac ~term] - ~status - - | _ -> raise (ProofEngineTypes.Fail "Transitivity failed") -;; - - diff --git a/helm/gTopLevel/equalityTactics.mli b/helm/gTopLevel/equalityTactics.mli deleted file mode 100644 index 7d57a0c11..000000000 --- a/helm/gTopLevel/equalityTactics.mli +++ /dev/null @@ -1,35 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -val rewrite_tac: term:Cic.term -> ProofEngineTypes.tactic -val rewrite_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic -val rewrite_back_tac: term:Cic.term -> ProofEngineTypes.tactic -val rewrite_back_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic -val replace_tac: what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic - -val reflexivity_tac: ProofEngineTypes.tactic -val symmetry_tac: ProofEngineTypes.tactic -val transitivity_tac: term:Cic.term -> ProofEngineTypes.tactic - diff --git a/helm/gTopLevel/fourier.ml b/helm/gTopLevel/fourier.ml deleted file mode 100644 index d7728c0b3..000000000 --- a/helm/gTopLevel/fourier.ml +++ /dev/null @@ -1,244 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* match ie.coef with - [] -> raise (Failure "empty ineq") - |(c::r) -> if rinf c r0 - then pop ie lneg - else if rinf r0 c then pop ie lpos - else pop ie lnul) - s; - [!lneg;!lnul;!lpos] -;; -(* initialise les histoires d'une liste d'inéquations données par leurs listes de coefficients et leurs strictitudes (!): -(add_hist [(equation 1, s1);...;(équation n, sn)]) -= -[{équation 1, [1;0;...;0], s1}; - {équation 2, [0;1;...;0], s2}; - ... - {équation n, [0;0;...;1], sn}] -*) -let add_hist le = - let n = List.length le in - let i=ref 0 in - List.map (fun (ie,s) -> - let h =ref [] in - for k=1 to (n-(!i)-1) do pop r0 h; done; - pop r1 h; - for k=1 to !i do pop r0 h; done; - i:=!i+1; - {coef=ie;hist=(!h);strict=s}) - le -;; -(* additionne deux inéquations *) -let ie_add ie1 ie2 = {coef=List.map2 rplus ie1.coef ie2.coef; - hist=List.map2 rplus ie1.hist ie2.hist; - strict=ie1.strict || ie2.strict} -;; -(* multiplication d'une inéquation par un rationnel (positif) *) -let ie_emult a ie = {coef=List.map (fun x -> rmult a x) ie.coef; - hist=List.map (fun x -> rmult a x) ie.hist; - strict= ie.strict} -;; -(* on enlève le premier coefficient *) -let ie_tl ie = {coef=List.tl ie.coef;hist=ie.hist;strict=ie.strict} -;; -(* le premier coefficient: "tête" de l'inéquation *) -let hd_coef ie = List.hd ie.coef -;; - -(* calcule toutes les combinaisons entre inéquations de tête négative et inéquations de tête positive qui annulent le premier coefficient. -*) -let deduce_add lneg lpos = - let res=ref [] in - List.iter (fun i1 -> - List.iter (fun i2 -> - let a = rop (hd_coef i1) in - let b = hd_coef i2 in - pop (ie_tl (ie_add (ie_emult b i1) - (ie_emult a i2))) res) - lpos) - lneg; - !res -;; -(* élimination de la première variable à partir d'une liste d'inéquations: -opération qu'on itère dans l'algorithme de Fourier. -*) -let deduce1 s i= - match (partitionne s) with - [lneg;lnul;lpos] -> - let lnew = deduce_add lneg lpos in - (match lneg with [] -> print_string("non posso ridurre "^string_of_int i^"\n")|_->(); - match lpos with [] -> print_string("non posso ridurre "^string_of_int i^"\n")|_->()); - (List.map ie_tl lnul)@lnew - |_->assert false -;; -(* algorithme de Fourier: on élimine successivement toutes les variables. -*) -let deduce lie = - let n = List.length (fst (List.hd lie)) in - let lie=ref (add_hist lie) in - for i=1 to n-1 do - lie:= deduce1 !lie i; - done; - !lie -;; - -(* donne [] si le système a des find solutions, -sinon donne [c,s,lc] -où lc est la combinaison linéaire des inéquations de départ -qui donne 0 < c si s=true - ou 0 <= c sinon -cette inéquation étant absurde. -*) -(** Tryes to find if the system admits solutions. - @param lie the list of inequations - @return a list that can be empty if the system has solutions. Otherwise it returns a - one elements list [\[(c,s,lc)\]]. {b c} is the rational that can be obtained solving the system, - {b s} is true if the inequation that proves that the system is absurd is of type [c < 0], false if - [c <= 0], {b lc} is a list of rational that represents the liear combination to obtain the - absurd inequation *) -let unsolvable lie = - let lr = deduce lie in - let res = ref [] in - (try (List.iter (fun e -> - match e with - {coef=[c];hist=lc;strict=s} -> - if (rinf c r0 && (not s)) || (rinfeq c r0 && s) - then (res := [c,s,lc]; - raise (Failure "contradiction found")) - |_->assert false) - lr) - with _ -> ()); - !res -;; - -(* Exemples: - -let test1=[[r1;r1;r0],true;[rop r1;r1;r1],false;[r0;rop r1;rop r1],false];; -deduce test1;; -unsolvable test1;; - -let test2=[ -[r1;r1;r0;r0;r0],false; -[r0;r1;r1;r0;r0],false; -[r0;r0;r1;r1;r0],false; -[r0;r0;r0;r1;r1],false; -[r1;r0;r0;r0;r1],false; -[rop r1;rop r1;r0;r0;r0],false; -[r0;rop r1;rop r1;r0;r0],false; -[r0;r0;rop r1;rop r1;r0],false; -[r0;r0;r0;rop r1;rop r1],false; -[rop r1;r0;r0;r0;rop r1],false -];; -deduce test2;; -unsolvable test2;; - -*) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml deleted file mode 100644 index 4008836fc..000000000 --- a/helm/gTopLevel/fourierR.ml +++ /dev/null @@ -1,1297 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - - -(******************** OTHER USEFUL TACTICS **********************) -(* Galla: moved in variousTactics.ml - -let rewrite_tac ~term:equality ~status:(proof,goal) = - let module C = Cic in - 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 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/eq.ind") -> - let eq_ind_r = - C.Const - (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[]) - 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",[]) - in - eqT_ind_r,ty,t1,t2 - | _ -> - raise - (ProofEngineTypes.Fail - "Rewrite: the argument is not a proof of an equality") - in - let pred = - let gty' = CicSubstitution.lift 1 gty in - let t1' = CicSubstitution.lift 1 t1 in - let gty'' = - ProofEngineReduction.replace_lifting - ~equality:ProofEngineReduction.alpha_equivalence - ~what:t1' ~with_what:(C.Rel 1) ~where:gty' - in - C.Lambda (C.Name "dummy_for_rewrite", ty, gty'') - in -prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); - let fresh_meta = ProofEngineHelpers.new_meta proof in - let irl = - ProofEngineHelpers.identity_relocation_list_for_metavariable context in - let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in - - let (proof',goals) = - PrimitiveTactics.exact_tac - ~term:(C.Appl - [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]) - ~status:((curi,metasenv',pbo,pty),goal) - in - assert (List.length goals = 0) ; - (proof',[fresh_meta]) -;; - - -let rewrite_simpl_tac ~term ~status = - Tacticals.then_ ~start:(rewrite_tac ~term) - ~continuation: - (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) - ~status -;; -*) - -(******************** THE FOURIER TACTIC ***********************) - -(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients -des inéquations et équations sont entiers. En attendant la tactique Field. -*) - -open Fourier - - -let debug x = print_string ("____ "^x) ; flush stdout;; - -let debug_pcontext x = - let str = ref "" in - List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^ - a ^ " " | _ ->()) x ; - debug ("contesto : "^ (!str) ^ "\n") -;; - -(****************************************************************************** -Operations on linear combinations. - -Opérations sur les combinaisons linéaires affines. -La partie homogène d'une combinaison linéaire est en fait une table de hash -qui donne le coefficient d'un terme du calcul des constructions, -qui est zéro si le terme n'y est pas. -*) - - - -(** - The type for linear combinations -*) -type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational} -;; - -(** - @return an empty flin -*) -let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0} -;; - -(** - @param f a flin - @param x a Cic.term - @return the rational associated with x (coefficient) -*) -let flin_coef f x = - try - (Hashtbl.find f.fhom x) - with - _ -> r0 -;; - -(** - Adds c to the coefficient of x - @param f a flin - @param x a Cic.term - @param c a rational - @return the new flin -*) -let flin_add f x c = - match x with - Cic.Rel(n) ->( - let cx = flin_coef f x in - Hashtbl.remove f.fhom x; - Hashtbl.add f.fhom x (rplus cx c); - f) - |_->debug ("Internal error in Fourier! this is not a Rel "^CicPp.ppterm x^"\n"); - let cx = flin_coef f x in - Hashtbl.remove f.fhom x; - Hashtbl.add f.fhom x (rplus cx c); - f -;; -(** - Adds c to f.fcste - @param f a flin - @param c a rational - @return the new flin -*) -let flin_add_cste f c = - {fhom=f.fhom; - fcste=rplus f.fcste c} -;; - -(** - @return a empty flin with r1 in fcste -*) -let flin_one () = flin_add_cste (flin_zero()) r1;; - -(** - Adds two flin -*) -let flin_plus f1 f2 = - let f3 = flin_zero() in - Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom; - Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom; - flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste; -;; - -(** - Substracts two flin -*) -let flin_minus f1 f2 = - let f3 = flin_zero() in - Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom; - Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom; - flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste); -;; - -(** - @return a times f -*) -let flin_emult a f = - let f2 = flin_zero() in - Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom; - flin_add_cste f2 (rmult a f.fcste); -;; - - -(*****************************************************************************) - - -(** - @param t a term - @raise Failure if conversion is impossible - @return rational proiection of t -*) -let rec rational_of_term t = - (* fun to apply f to the first and second rational-term of l *) - let rat_of_binop f l = - let a = List.hd l and - b = List.hd(List.tl l) in - f (rational_of_term a) (rational_of_term b) - in - (* as before, but f is unary *) - let rat_of_unop f l = - f (rational_of_term (List.hd l)) - in - match t with - | Cic.Cast (t1,t2) -> (rational_of_term t1) - | Cic.Appl (t1::next) -> - (match t1 with - Cic.Const (u,boh) -> - (match (UriManager.string_of_uri u) with - "cic:/Coq/Reals/Rdefinitions/Ropp.con" -> - rat_of_unop rop next - |"cic:/Coq/Reals/Rdefinitions/Rinv.con" -> - rat_of_unop rinv next - |"cic:/Coq/Reals/Rdefinitions/Rmult.con" -> - rat_of_binop rmult next - |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" -> - rat_of_binop rdiv next - |"cic:/Coq/Reals/Rdefinitions/Rplus.con" -> - rat_of_binop rplus next - |"cic:/Coq/Reals/Rdefinitions/Rminus.con" -> - rat_of_binop rminus next - | _ -> failwith "not a rational") - | _ -> failwith "not a rational") - | Cic.Const (u,boh) -> - (match (UriManager.string_of_uri u) with - "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1 - |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0 - | _ -> failwith "not a rational") - | _ -> failwith "not a rational" -;; - -(* coq wrapper -let rational_of_const = rational_of_term;; -*) -let fails f a = - try - let tmp = (f a) in - false - with - _-> true - ;; - -let rec flin_of_term t = - let fl_of_binop f l = - let a = List.hd l and - b = List.hd(List.tl l) in - f (flin_of_term a) (flin_of_term b) - in - try( - match t with - | Cic.Cast (t1,t2) -> (flin_of_term t1) - | Cic.Appl (t1::next) -> - begin - match t1 with - Cic.Const (u,boh) -> - begin - match (UriManager.string_of_uri u) with - "cic:/Coq/Reals/Rdefinitions/Ropp.con" -> - flin_emult (rop r1) (flin_of_term (List.hd next)) - |"cic:/Coq/Reals/Rdefinitions/Rplus.con"-> - fl_of_binop flin_plus next - |"cic:/Coq/Reals/Rdefinitions/Rminus.con"-> - fl_of_binop flin_minus next - |"cic:/Coq/Reals/Rdefinitions/Rmult.con"-> - begin - let arg1 = (List.hd next) and - arg2 = (List.hd(List.tl next)) - in - if fails rational_of_term arg1 - then - if fails rational_of_term arg2 - then - ( (* prodotto tra 2 incognite ????? impossibile*) - failwith "Sistemi lineari!!!!\n" - ) - else - ( - match arg1 with - Cic.Rel(n) -> (*trasformo al volo*) - (flin_add (flin_zero()) arg1 (rational_of_term arg2)) - |_-> (* test this *) - let tmp = flin_of_term arg1 in - flin_emult (rational_of_term arg2) (tmp) - ) - else - if fails rational_of_term arg2 - then - ( - match arg2 with - Cic.Rel(n) -> (*trasformo al volo*) - (flin_add (flin_zero()) arg2 (rational_of_term arg1)) - |_-> (* test this *) - let tmp = flin_of_term arg2 in - flin_emult (rational_of_term arg1) (tmp) - - ) - else - ( (*prodotto tra razionali*) - (flin_add_cste (flin_zero()) (rmult (rational_of_term arg1) (rational_of_term arg2))) - ) - (*try - begin - (*let a = rational_of_term arg1 in - debug("ho fatto rational of term di "^CicPp.ppterm arg1^ - " e ho ottenuto "^string_of_int a.num^"/"^string_of_int a.den^"\n");*) - let a = flin_of_term arg1 - try - begin - let b = (rational_of_term arg2) in - debug("ho fatto rational of term di "^CicPp.ppterm arg2^ - " e ho ottenuto "^string_of_int b.num^"/"^string_of_int b.den^"\n"); - (flin_add_cste (flin_zero()) (rmult a b)) - end - with - _ -> debug ("ho fallito2 su "^CicPp.ppterm arg2^"\n"); - (flin_add (flin_zero()) arg2 a) - end - with - _-> debug ("ho fallito1 su "^CicPp.ppterm arg1^"\n"); - (flin_add(flin_zero()) arg1 (rational_of_term arg2)) - *) - end - |"cic:/Coq/Reals/Rdefinitions/Rinv.con"-> - let a=(rational_of_term (List.hd next)) in - flin_add_cste (flin_zero()) (rinv a) - |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"-> - begin - let b=(rational_of_term (List.hd(List.tl next))) in - try - begin - let a = (rational_of_term (List.hd next)) in - (flin_add_cste (flin_zero()) (rdiv a b)) - end - with - _-> (flin_add (flin_zero()) (List.hd next) (rinv b)) - end - |_->assert false - end - |_ -> assert false - end - | Cic.Const (u,boh) -> - begin - match (UriManager.string_of_uri u) with - "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one () - |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero () - |_-> assert false - end - |_-> assert false) - with _ -> debug("eccezione = "^CicPp.ppterm t^"\n");flin_add (flin_zero()) t r1 -;; - -(* coq wrapper -let flin_of_constr = flin_of_term;; -*) - -(** - Translates a flin to (c,x) list - @param f a flin - @return something like (c1,x1)::(c2,x2)::...::(cn,xn) -*) -let flin_to_alist f = - let res=ref [] in - Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f; - !res -;; - -(* Représentation des hypothèses qui sont des inéquations ou des équations. -*) - -(** - The structure for ineq -*) -type hineq={hname:Cic.term; (* le nom de l'hypothèse *) - htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *) - hleft:Cic.term; - hright:Cic.term; - hflin:flin; - hstrict:bool} -;; - -(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0 -*) - -let ineq1_of_term (h,t) = - match t with (* match t *) - Cic.Appl (t1::next) -> - let arg1= List.hd next in - let arg2= List.hd(List.tl next) in - (match t1 with (* match t1 *) - Cic.Const (u,boh) -> - (match UriManager.string_of_uri u with (* match u *) - "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> - [{hname=h; - htype="Rlt"; - hleft=arg1; - hright=arg2; - hflin= flin_minus (flin_of_term arg1) - (flin_of_term arg2); - hstrict=true}] - |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> - [{hname=h; - htype="Rgt"; - hleft=arg2; - hright=arg1; - hflin= flin_minus (flin_of_term arg2) - (flin_of_term arg1); - hstrict=true}] - |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> - [{hname=h; - htype="Rle"; - hleft=arg1; - hright=arg2; - hflin= flin_minus (flin_of_term arg1) - (flin_of_term arg2); - hstrict=false}] - |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> - [{hname=h; - htype="Rge"; - hleft=arg2; - hright=arg1; - hflin= flin_minus (flin_of_term arg2) - (flin_of_term arg1); - hstrict=false}] - |_->assert false)(* match u *) - | Cic.MutInd (u,i,o) -> - (match UriManager.string_of_uri u with - "cic:/Coq/Init/Logic_Type/eqT.ind" -> - let t0= arg1 in - let arg1= arg2 in - let arg2= List.hd(List.tl (List.tl next)) in - (match t0 with - Cic.Const (u,boh) -> - (match UriManager.string_of_uri u with - "cic:/Coq/Reals/Rdefinitions/R.con"-> - [{hname=h; - htype="eqTLR"; - hleft=arg1; - hright=arg2; - hflin= flin_minus (flin_of_term arg1) - (flin_of_term arg2); - hstrict=false}; - {hname=h; - htype="eqTRL"; - hleft=arg2; - hright=arg1; - hflin= flin_minus (flin_of_term arg2) - (flin_of_term arg1); - hstrict=false}] - |_-> assert false) - |_-> assert false) - |_-> assert false) - |_-> assert false)(* match t1 *) - |_-> assert false (* match t *) -;; -(* coq wrapper -let ineq1_of_constr = ineq1_of_term;; -*) - -(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq) -*) - -let rec print_rl l = - match l with - []-> () - | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next -;; - -let rec print_sys l = - match l with - [] -> () - | (a,b)::next -> (print_rl a; - print_string (if b=true then "strict\n"else"\n"); - print_sys next) - ;; - -(*let print_hash h = - Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h -;;*) - -let fourier_lineq lineq1 = - let nvar=ref (-1) in - let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *) - List.iter (fun f -> - Hashtbl.iter (fun x c -> - try (Hashtbl.find hvar x;()) - with _-> nvar:=(!nvar)+1; - Hashtbl.add hvar x (!nvar); - debug("aggiungo una var "^ - string_of_int !nvar^" per "^ - CicPp.ppterm x^"\n")) - f.hflin.fhom) - lineq1; - (*print_hash hvar;*) - debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n"); - let sys= List.map (fun h-> - let v=Array.create ((!nvar)+1) r0 in - Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x) <- c) - h.hflin.fhom; - ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict)) - lineq1 in - debug ("chiamo unsolvable sul sistema di "^ - string_of_int (List.length sys) ^"\n"); - print_sys sys; - unsolvable sys -;; - -(***************************************************************************** -Construction de la preuve en cas de succès de la méthode de Fourier, -i.e. on obtient une contradiction. -*) - - -let _eqT = Cic.MutInd(UriManager.uri_of_string - "cic:/Coq/Init/Logic_Type/eqT.ind") 0 [] ;; -let _False = Cic.MutInd (UriManager.uri_of_string - "cic:/Coq/Init/Logic/False.ind") 0 [] ;; -let _not = Cic.Const (UriManager.uri_of_string - "cic:/Coq/Init/Logic/not.con") [];; -let _R0 = Cic.Const (UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/R0.con") [] ;; -let _R1 = Cic.Const (UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/R1.con") [] ;; -let _R = Cic.Const (UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/R.con") [] ;; -let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") [] ;; -let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") [] ;; -let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") [] ;; -let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") [] ;; -let _Rfourier_le=Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") [] ;; -let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") [] ;; -let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") [] ;; -let _Rfourier_lt=Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") [] ;; -let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") [] ;; -let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") [] ;; -let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") [] ;; -let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") [] ;; -let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") [] ;; -let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") [] ;; -let _Rinv = Cic.Const (UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Rinv.con") [] ;; -let _Rinv_R1 = Cic.Const(UriManager.uri_of_string - "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) [] ;; -let _Rle = Cic.Const (UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Rle.con") [] ;; -let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") [] ;; -let _Rle_not_lt = Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") [] ;; -let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") [] ;; -let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") [] ;; -(*let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") [] ;;*) -let _Rlt = Cic.Const (UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Rlt.con") [] ;; -let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") [] ;; -let _Rlt_not_le = Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") [] ;; -let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") [] ;; -let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") [] ;; -let _Rminus = Cic.Const (UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Rminus.con") [] ;; -let _Rmult = Cic.Const (UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Rmult.con") [] ;; -let _Rnot_le_le =Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") [] ;; -let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") [] ;; -let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") [] ;; -let _Ropp = Cic.Const (UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Ropp.con") [] ;; -let _Rplus = Cic.Const (UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Rplus.con") [] ;; - -(******************************************************************************) - -let is_int x = (x.den)=1 -;; - -(* fraction = couple (num,den) *) -let rec rational_to_fraction x= (x.num,x.den) -;; - -(* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1))) -*) - -let rec int_to_real_aux n = - match n with - 0 -> _R0 (* o forse R0 + R0 ????? *) - | 1 -> _R1 - | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ] -;; - - -let int_to_real n = - let x = int_to_real_aux (abs n) in - if n < 0 then - Cic.Appl [ _Ropp ; x ] - else - x -;; - - -(* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1))) -*) - -let rational_to_real x = - let (n,d)=rational_to_fraction x in - Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ] -;; - -(* preuve que 0 m=goal) metasenv in - debug ("th = "^ CicPp.ppterm t ^"\n"); - debug ("ty = "^ CicPp.ppterm ty^"\n"); - in - let tacn=ref - (fun ~status -> pall "n0" ~status _Rlt_zero_1 ; - PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in - let tacd=ref - (fun ~status -> pall "d0" ~status _Rlt_zero_1 ; - PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in - - - for i=1 to n-1 do - tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i) - ~status _Rlt_zero_pos_plus1; - PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status) - ~continuation:!tacn); - done; - for i=1 to d-1 do - tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d" - ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac - ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd); - done; - - - -debug("TAC ZERO INF POS\n"); - -(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) - ~continuations:[ - !tacn ; - !tacd ] - ~status) -;; - - - -(* preuve que 0<=n*1/d -*) - -let tac_zero_infeq_pos gl (n,d) ~status = - (*let cste = pf_parse_constr gl in*) - debug("inizio tac_zero_infeq_pos\n"); - let tacn = ref - (*(if n=0 then - (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero ) - else*) - (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 ) - (* ) *) - in - let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in - for i=1 to n-1 do - tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac - ~term:_Rle_zero_pos_plus1) ~continuation:!tacn); - done; - for i=1 to d-1 do - tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac - ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); - done; - let r = - (Tacticals.thens ~start:(PrimitiveTactics.apply_tac - ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) ~status in - debug("fine tac_zero_infeq_pos\n"); - r -;; - - - -(* preuve que 0<(-n)*(1/d) => False -*) - -let tac_zero_inf_false gl (n,d) ~status= - debug("inizio tac_zero_inf_false\n"); - if n=0 then - (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in - debug("fine\n"); - r) - else - (debug "2\n";let r = (Tacticals.then_ ~start:( - fun ~status:(proof,goal as status) -> - let curi,metasenv,pbo,pty = proof in - let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in - debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with " - ^ CicPp.ppterm ty ^"\n"); - let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in - debug("!!!!!!!!!2\n"); - r - ) - ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in - debug("fine\n"); - r - ) -;; - -(* preuve que 0<=n*(1/d) => False ; n est negatif -*) - -let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)= -debug("stat tac_zero_infeq_false\n"); -let r = - let curi,metasenv,pbo,pty = proof in - let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in - - debug("faccio fold di " ^ CicPp.ppterm - (Cic.Appl - [_Rle ; _R0 ; - Cic.Appl - [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]] - ] - ) ^ "\n") ; - debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n"); - (*CSC: Patch to undo the over-simplification of RewriteSimpl *) - Tacticals.then_ - ~start: - (ReductionTactics.fold_tac ~reduction:CicReduction.whd - ~also_in_hypotheses:false - ~term: - (Cic.Appl - [_Rle ; _R0 ; - Cic.Appl - [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]] - ] - ) - ) - ~continuation: - (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) - ~continuation:(tac_zero_inf_pos (-n,d))) ~status in - debug("end tac_zero_infeq_false\n"); - r -(*PORTING - Tacticals.id_tac ~status -*) -;; - - -(* *********** ********** ******** ??????????????? *********** **************) - -let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let fresh_meta = ProofEngineHelpers.new_meta proof in - let irl = - ProofEngineHelpers.identity_relocation_list_for_metavariable context in - let metasenv' = (fresh_meta,context,t)::metasenv in - let proof' = curi,metasenv',pbo,pty in - let proof'',goals = - PrimitiveTactics.apply_tac - (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) (* ??? *)*) - ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *) - ~status:(proof',goal) - in - proof'',fresh_meta::goals -;; - - - - - -let my_cut ~term:c ~status:(proof,goal)= - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - -debug("my_cut di "^CicPp.ppterm c^"\n"); - - - let fresh_meta = ProofEngineHelpers.new_meta proof in - let irl = - ProofEngineHelpers.identity_relocation_list_for_metavariable context in - let metasenv' = (fresh_meta,context,c)::metasenv in - let proof' = curi,metasenv',pbo,pty in - let proof'',goals = - apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c, - CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)] - ~status:(proof',goal) - in - (* We permute the generated goals to be consistent with Coq *) - match goals with - [] -> assert false - | he::tl -> proof'',he::fresh_meta::tl -;; - - -let exact = PrimitiveTactics.exact_tac;; - -let tac_use h ~status:(proof,goal as status) = -debug("Inizio TC_USE\n"); -let curi,metasenv,pbo,pty = proof in -let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in -debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); -debug ("ty = "^ CicPp.ppterm ty^"\n"); - -let res = -match h.htype with - "Rlt" -> exact ~term:h.hname ~status - |"Rle" -> exact ~term:h.hname ~status - |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac - ~term:_Rfourier_gt_to_lt) - ~continuation:(exact ~term:h.hname)) ~status - |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac - ~term:_Rfourier_ge_to_le) - ~continuation:(exact ~term:h.hname)) ~status - |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac - ~term:_Rfourier_eqLR_to_le) - ~continuation:(exact ~term:h.hname)) ~status - |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac - ~term:_Rfourier_eqRL_to_le) - ~continuation:(exact ~term:h.hname)) ~status - |_->assert false -in -debug("Fine TAC_USE\n"); -res -;; - - - -let is_ineq (h,t) = - match t with - Cic.Appl ( Cic.Const(u,boh)::next) -> - (match (UriManager.string_of_uri u) with - "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true - |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true - |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true - |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true - |"cic:/Coq/Init/Logic_Type/eqT.con" -> - (match (List.hd next) with - Cic.Const (uri,_) when - UriManager.string_of_uri uri = - "cic:/Coq/Reals/Rdefinitions/R.con" -> true - | _ -> false) - |_->false) - |_->false -;; - -let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;; - -let mkAppL a = - Cic.Appl(Array.to_list a) -;; - -(* Résolution d'inéquations linéaires dans R *) -let rec strip_outer_cast c = match c with - | Cic.Cast (c,_) -> strip_outer_cast c - | _ -> c -;; - -(*let find_in_context id context = - let rec find_in_context_aux c n = - match c with - [] -> failwith (id^" not found in context") - | a::next -> (match a with - Some (Cic.Name(name),_) when name = id -> n - (*? magari al posto di _ qualcosaltro?*) - | _ -> find_in_context_aux next (n+1)) - in - find_in_context_aux context 1 -;; - -(* mi sembra quadratico *) -let rec filter_real_hyp context cont = - match context with - [] -> [] - | Some(Cic.Name(h),Cic.Decl(t))::next -> ( - let n = find_in_context h cont in - debug("assegno "^string_of_int n^" a "^CicPp.ppterm t^"\n"); - [(Cic.Rel(n),t)] @ filter_real_hyp next cont) - | a::next -> debug(" no\n"); filter_real_hyp next cont -;;*) -let filter_real_hyp context _ = - let rec filter_aux context num = - match context with - [] -> [] - | Some(Cic.Name(h),Cic.Decl(t))::next -> - ( - (*let n = find_in_context h cont in*) - debug("assegno "^string_of_int num^" a "^h^":"^CicPp.ppterm t^"\n"); - [(Cic.Rel(num),t)] @ filter_aux next (num+1) - ) - | a::next -> filter_aux next (num+1) - in - filter_aux context 1 -;; - - -(* lifts everithing at the conclusion level *) -let rec superlift c n= - match c with - [] -> [] - | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl( - CicSubstitution.lift n a))] @ superlift next (n+1) - | Some(name,Cic.Def(a))::next -> [Some(name,Cic.Def( - CicSubstitution.lift n a))] @ superlift next (n+1) - | _::next -> superlift next (n+1) (*?? ??*) - -;; - -let equality_replace a b ~status = -debug("inizio EQ\n"); - 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 - 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 -debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl))); - let (proof,goals) = - EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) - ~status:((curi,metasenv',pbo,pty),goal) - in - let new_goals = fresh_meta::goals in -debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = " - ^string_of_int( List.length goals)^"+ meta\n"); - (proof,new_goals) -;; - -let tcl_fail a ~status:(proof,goal) = - match a with - 1 -> raise (ProofEngineTypes.Fail "fail-tactical") - |_-> (proof,[goal]) -;; - -(* Galla: moved in variousTactics.ml -let assumption_tac ~status:(proof,goal)= - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let num = ref 0 in - let tac_list = List.map - ( fun x -> num := !num + 1; - match x with - Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num))) - | _ -> ("fake",tcl_fail 1) - ) - context - in - Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal) -;; -*) -(* Galla: moved in negationTactics.ml -(* !!!!! fix !!!!!!!!!! *) -let contradiction_tac ~status:(proof,goal)= - Tacticals.then_ - (*inutile sia questo che quello prima della chiamata*) - ~start:PrimitiveTactics.intros_tac - ~continuation:(Tacticals.then_ - ~start:(VariousTactics.elim_type_tac ~term:_False) - ~continuation:(assumption_tac)) - ~status:(proof,goal) -;; -*) - -(* ********************* TATTICA ******************************** *) - -let rec fourier ~status:(s_proof,s_goal)= - let s_curi,s_metasenv,s_pbo,s_pty = s_proof in - let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal) - s_metasenv in - - debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n"); - debug_pcontext s_context; - - let fhyp = String.copy "new_hyp_for_fourier" in - -(* here we need to negate the thesis, but to do this we need to apply the right -theoreme,so let's parse our thesis *) - - let th_to_appl = ref _Rfourier_not_le_gt in - (match s_ty with - Cic.Appl ( Cic.Const(u,boh)::args) -> - (match UriManager.string_of_uri u with - "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl := - _Rfourier_not_ge_lt - |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl := - _Rfourier_not_gt_le - |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl := - _Rfourier_not_le_gt - |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl := - _Rfourier_not_lt_ge - |_-> failwith "fourier can't be applyed") - |_-> failwith "fourier can't be applyed"); - (* fix maybe strip_outer_cast goes here?? *) - - (* now let's change our thesis applying the th and put it with hp *) - - let proof,gl = - Tacticals.then_ - ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl) - ~continuation:PrimitiveTactics.intros_tac - ~status:(s_proof,s_goal) in - let goal = if List.length gl = 1 then List.hd gl - else failwith "a new goal" in - - debug ("port la tesi sopra e la nego. contesto :\n"); - debug_pcontext s_context; - - (* now we have all the right environment *) - - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - - - (* now we want to convert hp to inequations, but first we must lift - everyting to thesis level, so that a variable has the save Rel(n) - in each hp ( needed by ineq1_of_term ) *) - - (* ? fix if None ?????*) - (* fix change superlift with a real name *) - - let l_context = superlift context 1 in - let hyps = filter_real_hyp l_context l_context in - - debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n"); - - let lineq =ref [] in - - (* transform hyps into inequations *) - - List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq)) - with _-> ()) - hyps; - - - debug ("applico fourier a "^ string_of_int (List.length !lineq)^ - " disequazioni\n"); - - let res=fourier_lineq (!lineq) in - let tac=ref Tacticals.id_tac in - if res=[] then - (print_string "Tactic Fourier fails.\n";flush stdout; - failwith "fourier_tac fails") - else - ( - match res with (*match res*) - [(cres,sres,lc)]-> - - (* in lc we have the coefficient to "reduce" the system *) - - print_string "Fourier's method can prove the goal...\n";flush stdout; - - debug "I coeff di moltiplicazione rit sono: "; - - let lutil=ref [] in - List.iter - (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil); - (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *)) - ) - (List.combine (!lineq) lc); - - print_string (" quindi lutil e' lunga "^ - string_of_int (List.length (!lutil))^"\n"); - - (* on construit la combinaison linéaire des inéquation *) - - (match (!lutil) with (*match (!lutil) *) - (h1,c1)::lutil -> - debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n"; - - let s=ref (h1.hstrict) in - - - let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in - let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in - - List.iter (fun (h,c) -> - s:=(!s)||(h.hstrict); - t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl - [_Rmult;rational_to_real c;h.hleft ] ]); - t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl - [_Rmult;rational_to_real c;h.hright] ])) - lutil; - - let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in - let tc=rational_to_real cres in - - -(* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *) - - debug "inizio a costruire tac1\n"; - Fourier.print_rational(c1); - - let tac1=ref ( fun ~status -> - if h1.hstrict then - (Tacticals.thens - ~start:( - fun ~status -> - debug ("inizio t1 strict\n"); - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find - (function (m,_,_) -> m=goal) metasenv in - debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); - debug ("ty = "^ CicPp.ppterm ty^"\n"); - PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status) - ~continuations:[tac_use h1;tac_zero_inf_pos - (rational_to_fraction c1)] - ~status - ) - else - (Tacticals.thens - ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le) - ~continuations:[tac_use h1;tac_zero_inf_pos - (rational_to_fraction c1)] ~status - ) - ) - - in - s:=h1.hstrict; - List.iter (fun (h,c) -> - (if (!s) then - (if h.hstrict then - (debug("tac1 1\n"); - tac1:=(Tacticals.thens - ~start:(PrimitiveTactics.apply_tac - ~term:_Rfourier_lt_lt) - ~continuations:[!tac1;tac_use h;tac_zero_inf_pos - (rational_to_fraction c)]) - ) - else - (debug("tac1 2\n"); - Fourier.print_rational(c1); - tac1:=(Tacticals.thens - ~start:( - fun ~status -> - debug("INIZIO TAC 1 2\n"); - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) - metasenv in - debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); - debug ("ty = "^ CicPp.ppterm ty^"\n"); - PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status) - ~continuations:[!tac1;tac_use h;tac_zero_inf_pos - (rational_to_fraction c)]) - ) - ) - else - (if h.hstrict then - (debug("tac1 3\n"); - tac1:=(Tacticals.thens - ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt) - ~continuations:[!tac1;tac_use h;tac_zero_inf_pos - (rational_to_fraction c)]) - ) - else - (debug("tac1 4\n"); - tac1:=(Tacticals.thens - ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le) - ~continuations:[!tac1;tac_use h;tac_zero_inf_pos - (rational_to_fraction c)]) - ) - ) - ); - s:=(!s)||(h.hstrict)) lutil;(*end List.iter*) - - let tac2 = - if sres then - tac_zero_inf_false goal (rational_to_fraction cres) - else - tac_zero_infeq_false goal (rational_to_fraction cres) - in - tac:=(Tacticals.thens - ~start:(my_cut ~term:ineq) - ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_ - ~start:(fun ~status:(proof,goal as status) -> - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) - metasenv in - PrimitiveTactics.change_tac ~what:ty - ~with_what:(Cic.Appl [ _not; ineq]) ~status) - ~continuation:(Tacticals.then_ - ~start:(PrimitiveTactics.apply_tac ~term: - (if sres then _Rnot_lt_lt else _Rnot_le_le)) - ~continuation:(Tacticals.thens - ~start:( - fun ~status -> - debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n"); - let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc - ~status - in - (match r with (p,gl) -> - debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" )); - r) - ~continuations:[(Tacticals.thens - ~start:( - fun ~status -> - let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in - (match r with (p,gl) -> - debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" )); - r) - ~continuations: - [PrimitiveTactics.apply_tac ~term:_Rinv_R1 - ;Tacticals.try_tactics - ~tactics:[ "ring", (fun ~status -> - debug("begin RING\n"); - let r = Ring.ring_tac ~status in - debug ("end RING\n"); - r) - ; "id", Tacticals.id_tac] - ]) - ;(*Tacticals.id_tac*) - Tacticals.then_ - ~start: - ( - fun ~status:(proof,goal as status) -> - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m= - goal) metasenv in - (* check if ty is of type *) - let w1 = - debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n"); - (match ty with - Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a]) - |_ -> assert false) - in - let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in - debug("fine MY_CHNGE\n"); - r - - ) - ~continuation:(*PORTINGTacticals.id_tac*)tac2])) - ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*) - - |_-> assert false)(*match (!lutil) *) - |_-> assert false); (*match res*) - debug ("finalmente applico tac\n"); - ( - let r = !tac ~status:(proof,goal) in - debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r - - ) -;; - -let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);; - - diff --git a/helm/gTopLevel/fourierR.mli b/helm/gTopLevel/fourierR.mli deleted file mode 100644 index e5790ec0f..000000000 --- a/helm/gTopLevel/fourierR.mli +++ /dev/null @@ -1,5 +0,0 @@ -(* -val rewrite_tac: term:Cic.term -> ProofEngineTypes.tactic -val rewrite_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic -*) -val fourier_tac: ProofEngineTypes.tactic diff --git a/helm/gTopLevel/introductionTactics.ml b/helm/gTopLevel/introductionTactics.ml deleted file mode 100644 index bc28c4170..000000000 --- a/helm/gTopLevel/introductionTactics.ml +++ /dev/null @@ -1,59 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - - -let constructor_tac ~n ~status:(proof, goal) = - let module C = Cic in - let module R = CicReduction in - let (_,metasenv,_,_) = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - match (R.whd context ty) with - (C.MutInd (uri, typeno, exp_named_subst)) - | (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) -> - PrimitiveTactics.apply_tac ~status:(proof, goal) - ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst)) - | _ -> raise (ProofEngineTypes.Fail "Constructor: failed") -;; - - -let exists_tac ~status = - constructor_tac ~n:1 ~status -;; - - -let split_tac ~status = - constructor_tac ~n:1 ~status -;; - - -let left_tac ~status = - constructor_tac ~n:1 ~status -;; - - -let right_tac ~status = - constructor_tac ~n:2 ~status -;; - diff --git a/helm/gTopLevel/introductionTactics.mli b/helm/gTopLevel/introductionTactics.mli deleted file mode 100644 index c3a12720b..000000000 --- a/helm/gTopLevel/introductionTactics.mli +++ /dev/null @@ -1,31 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -val constructor_tac: n:int -> ProofEngineTypes.tactic - -val exists_tac: ProofEngineTypes.tactic -val split_tac: ProofEngineTypes.tactic -val left_tac: ProofEngineTypes.tactic -val right_tac: ProofEngineTypes.tactic diff --git a/helm/gTopLevel/negationTactics.ml b/helm/gTopLevel/negationTactics.ml deleted file mode 100644 index 2b87bb911..000000000 --- a/helm/gTopLevel/negationTactics.ml +++ /dev/null @@ -1,71 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - - -let absurd_tac ~term ~status:((proof,goal) as status) = - let module C = Cic in - let module U = UriManager in - let module P = PrimitiveTactics in - let _,metasenv,_,_ = proof in - let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) (* ma questo controllo serve?? *) - then P.apply_tac - ~term:(C.Appl [(C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/absurd.con") , [] )) ; term ; ty]) ~status - else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition") -;; - - -let contradiction_tac ~status = - let module C = Cic in - let module U = UriManager in - let module P = PrimitiveTactics in - let module T = Tacticals in - try - T.then_ - ~start: P.intros_tac - ~continuation:( - T.then_ - ~start: (EliminationTactics.elim_type_tac - ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] )) - ~continuation: VariousTactics.assumption_tac) - ~status - with - (ProofEngineTypes.Fail "Assumption: No such assumption") -> raise (ProofEngineTypes.Fail "Contradiction: No such assumption") - (* sarebbe piu' elegante se Assumtion sollevasse un'eccezione tutta sua che questa cattura, magari con l'aiuto di try_tactics *) -;; - -(* Questa era in fourierR.ml -(* !!!!! fix !!!!!!!!!! *) -let contradiction_tac ~status:(proof,goal)= - Tacticals.then_ - ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima della chiamata*) - ~continuation:(Tacticals.then_ - ~start:(VariousTactics.elim_type_tac ~term:_False) - ~continuation:(assumption_tac)) - ~status:(proof,goal) -;; -*) - - diff --git a/helm/gTopLevel/negationTactics.mli b/helm/gTopLevel/negationTactics.mli deleted file mode 100644 index bfa3e8d5d..000000000 --- a/helm/gTopLevel/negationTactics.mli +++ /dev/null @@ -1,28 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -val absurd_tac: term:Cic.term -> ProofEngineTypes.tactic -val contradiction_tac: ProofEngineTypes.tactic - diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml deleted file mode 100644 index ccd8ccfe0..000000000 --- a/helm/gTopLevel/primitiveTactics.ml +++ /dev/null @@ -1,548 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -open ProofEngineHelpers -open ProofEngineTypes - -exception NotAnInductiveTypeToEliminate -exception NotTheRightEliminatorShape -exception NoHypothesesFound -exception WrongUriToVariable of string - -(* lambda_abstract newmeta ty *) -(* returns a triple [bo],[context],[ty'] where *) -(* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *) -(* and [bo] = Lambda/LetIn [context].(Meta [newmeta]) *) -(* So, lambda_abstract is the core of the implementation of *) -(* the Intros tactic. *) -let lambda_abstract context newmeta ty mknames = - let module C = Cic in - let rec collect_context context = - function - C.Cast (te,_) -> collect_context context te - | C.Prod (n,s,t) -> - let n' = C.Name (mknames n) in - let (context',ty,bo) = - collect_context ((Some (n',(C.Decl s)))::context) t - in - (context',ty,C.Lambda(n',s,bo)) - | C.LetIn (n,s,t) -> - let (context',ty,bo) = - collect_context ((Some (n,(C.Def s)))::context) t - in - (context',ty,C.LetIn(n,s,bo)) - | _ as t -> - let irl = identity_relocation_list_for_metavariable context in - context, t, (C.Meta (newmeta,irl)) - in - collect_context context ty - -let eta_expand metasenv context t arg = - let module T = CicTypeChecker in - let module S = CicSubstitution in - let module C = Cic in - let rec aux n = - function - t' when t' = S.lift n arg -> C.Rel (1 + n) - | C.Rel m -> if m <= n then C.Rel m else C.Rel (m+1) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = aux_exp_named_subst n exp_named_subst in - C.Var (uri,exp_named_subst') - | C.Meta _ - | C.Sort _ - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty) - | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t) - | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t) - | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t) - | C.Appl l -> C.Appl (List.map (aux n) l) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = aux_exp_named_subst n exp_named_subst in - C.Const (uri,exp_named_subst') - | C.MutInd (uri,i,exp_named_subst) -> - let exp_named_subst' = aux_exp_named_subst n exp_named_subst in - C.MutInd (uri,i,exp_named_subst') - | C.MutConstruct (uri,i,j,exp_named_subst) -> - let exp_named_subst' = aux_exp_named_subst n exp_named_subst in - C.MutConstruct (uri,i,j,exp_named_subst') - | C.MutCase (sp,i,outt,t,pl) -> - C.MutCase (sp,i,aux n outt, aux n t, - List.map (aux n) pl) - | C.Fix (i,fl) -> - let tylen = List.length fl in - let substitutedfl = - List.map - (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo)) - fl - in - C.Fix (i, substitutedfl) - | C.CoFix (i,fl) -> - let tylen = List.length fl in - let substitutedfl = - List.map - (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo)) - fl - in - C.CoFix (i, substitutedfl) - and aux_exp_named_subst n = - List.map (function uri,t -> uri,aux n t) - in - let argty = - T.type_of_aux' metasenv context arg - in - (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg]) - -(*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *) -let classify_metas newmeta in_subst_domain subst_in metasenv = - List.fold_right - (fun (i,canonical_context,ty) (old_uninst,new_uninst) -> - if in_subst_domain i then - old_uninst,new_uninst - else - let ty' = subst_in canonical_context ty in - let canonical_context' = - List.fold_right - (fun entry canonical_context' -> - let entry' = - match entry with - Some (n,Cic.Decl s) -> - Some (n,Cic.Decl (subst_in canonical_context' s)) - | Some (n,Cic.Def s) -> - Some (n,Cic.Def (subst_in canonical_context' s)) - | None -> None - in - entry'::canonical_context' - ) canonical_context [] - in - if i < newmeta then - ((i,canonical_context',ty')::old_uninst),new_uninst - else - old_uninst,((i,canonical_context',ty')::new_uninst) - ) metasenv ([],[]) - -(* Auxiliary function for apply: given a type (a backbone), it returns its *) -(* head, a META environment in which there is new a META for each hypothesis,*) -(* a list of arguments for the new applications and the indexes of the first *) -(* and last new METAs introduced. The nth argument in the list of arguments *) -(* is just the nth new META. *) -let new_metasenv_for_apply newmeta proof context ty = - let module C = Cic in - let module S = CicSubstitution in - let rec aux newmeta = - function - C.Cast (he,_) -> aux newmeta he - | C.Prod (name,s,t) -> - let irl = identity_relocation_list_for_metavariable context in - let newargument = C.Meta (newmeta,irl) in - let (res,newmetasenv,arguments,lastmeta) = - aux (newmeta + 1) (S.subst newargument t) - in - res,(newmeta,context,s)::newmetasenv,newargument::arguments,lastmeta - | t -> t,[],[],newmeta - in - (* WARNING: here we are using the invariant that above the most *) - (* recente new_meta() there are no used metas. *) - let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in - res,newmetasenv,arguments,lastmeta - -(* Useful only inside apply_tac *) -let - generalize_exp_named_subst_with_fresh_metas context newmeta uri exp_named_subst -= - let module C = Cic in - let params = - match CicEnvironment.get_obj uri with - C.Constant (_,_,_,params) - | C.CurrentProof (_,_,_,_,params) - | C.Variable (_,_,_,params) - | C.InductiveDefinition (_,params,_) -> params - in - let exp_named_subst_diff,new_fresh_meta,newmetasenvfragment,exp_named_subst'= - let next_fresh_meta = ref newmeta in - let newmetasenvfragment = ref [] in - let exp_named_subst_diff = ref [] in - let rec aux = - function - [],[] -> [] - | uri::tl,[] -> - let ty = - match CicEnvironment.get_obj uri with - C.Variable (_,_,ty,_) -> - CicSubstitution.subst_vars !exp_named_subst_diff ty - | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) - in - let irl = identity_relocation_list_for_metavariable context in - let subst_item = uri,C.Meta (!next_fresh_meta,irl) in - newmetasenvfragment := - (!next_fresh_meta,context,ty)::!newmetasenvfragment ; - exp_named_subst_diff := !exp_named_subst_diff @ [subst_item] ; - incr next_fresh_meta ; - subst_item::(aux (tl,[])) - | uri::tl1,((uri',_) as s)::tl2 -> - assert (UriManager.eq uri uri') ; - s::(aux (tl1,tl2)) - | [],_ -> assert false - in - let exp_named_subst' = aux (params,exp_named_subst) in - !exp_named_subst_diff,!next_fresh_meta, - List.rev !newmetasenvfragment, exp_named_subst' - in -prerr_endline ("@@@ " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst)) ^ " |--> " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst'))) ; - new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff -;; - -let apply_tac ~term ~status:(proof, goal) = - (* Assumption: The term "term" must be closed in the current context *) - let module T = CicTypeChecker in - let module R = CicReduction in - let module C = Cic in - let (_,metasenv,_,_) = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let newmeta = new_meta ~proof in - let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = - match term with - C.Var (uri,exp_named_subst) -> - let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = - generalize_exp_named_subst_with_fresh_metas context newmeta uri - exp_named_subst - in - exp_named_subst_diff,newmeta',newmetasenvfragment, - C.Var (uri,exp_named_subst') - | C.Const (uri,exp_named_subst) -> - let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = - generalize_exp_named_subst_with_fresh_metas context newmeta uri - exp_named_subst - in - exp_named_subst_diff,newmeta',newmetasenvfragment, - C.Const (uri,exp_named_subst') - | C.MutInd (uri,tyno,exp_named_subst) -> - let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = - generalize_exp_named_subst_with_fresh_metas context newmeta uri - exp_named_subst - in - exp_named_subst_diff,newmeta',newmetasenvfragment, - C.MutInd (uri,tyno,exp_named_subst') - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = - generalize_exp_named_subst_with_fresh_metas context newmeta uri - exp_named_subst - in - exp_named_subst_diff,newmeta',newmetasenvfragment, - C.MutConstruct (uri,tyno,consno,exp_named_subst') - | _ -> [],newmeta,[],term - in - let metasenv' = metasenv@newmetasenvfragment in -prerr_endline ("^^^^^TERM': " ^ CicPp.ppterm term') ; - let termty = - CicSubstitution.subst_vars exp_named_subst_diff - (CicTypeChecker.type_of_aux' metasenv' context term) - in -prerr_endline ("^^^^^TERMTY: " ^ CicPp.ppterm termty) ; - (* newmeta is the lowest index of the new metas introduced *) - let (consthead,newmetas,arguments,_) = - new_metasenv_for_apply newmeta' proof context termty - in - let newmetasenv = metasenv'@newmetas in - let subst,newmetasenv' = - CicUnification.fo_unif newmetasenv context consthead ty - in - let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in - let apply_subst = CicUnification.apply_subst subst in - let old_uninstantiatedmetas,new_uninstantiatedmetas = - (* subst_in doesn't need the context. Hence the underscore. *) - let subst_in _ = CicUnification.apply_subst subst in - classify_metas newmeta in_subst_domain subst_in newmetasenv' - in - let bo' = - apply_subst - (if List.length newmetas = 0 then - term' - else - Cic.Appl (term'::arguments) - ) - in -prerr_endline ("XXXX " ^ CicPp.ppterm (if List.length newmetas = 0 then term' else Cic.Appl (term'::arguments)) ^ " |>>> " ^ CicPp.ppterm bo') ; - let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in - let (newproof, newmetasenv''') = - let subst_in = CicUnification.apply_subst ((metano,bo')::subst) in - subst_meta_and_metasenv_in_proof - proof metano subst_in newmetasenv'' - in - (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas) - - (* TODO per implementare i tatticali e' necessario che tutte le tattiche - sollevino _solamente_ Fail *) -let apply_tac ~term ~status = - try - apply_tac ~term ~status - (* TODO cacciare anche altre eccezioni? *) - with CicUnification.UnificationFailed as e -> - raise (Fail (Printexc.to_string e)) - -let intros_tac ~status:(proof, goal) = - let module C = Cic in - let module R = CicReduction in - let (_,metasenv,_,_) = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let newmeta = new_meta ~proof in - let (context',ty',bo') = - lambda_abstract context newmeta ty (ProofEngineHelpers.fresh_name) - in - let (newproof, _) = - subst_meta_in_proof proof metano bo' [newmeta,context',ty'] - in - (newproof, [newmeta]) - -let cut_tac ~term ~status:(proof, goal) = - let module C = Cic in - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let newmeta1 = new_meta ~proof in - let newmeta2 = newmeta1 + 1 in - let context_for_newmeta1 = - (Some (C.Name "dummy_for_cut",C.Decl term))::context in - let irl1 = - identity_relocation_list_for_metavariable context_for_newmeta1 in - let irl2 = identity_relocation_list_for_metavariable context in - let newmeta1ty = CicSubstitution.lift 1 ty in - let bo' = - C.Appl - [C.Lambda (C.Name "dummy_for_cut",term,C.Meta (newmeta1,irl1)) ; - C.Meta (newmeta2,irl2)] - in - let (newproof, _) = - subst_meta_in_proof proof metano bo' - [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty]; - in - (newproof, [newmeta1 ; newmeta2]) - -let letin_tac ~term ~status:(proof, goal) = - let module C = Cic in - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let _ = CicTypeChecker.type_of_aux' metasenv context term in - let newmeta = new_meta ~proof in - let context_for_newmeta = - (Some (C.Name "dummy_for_letin",C.Def term))::context in - let irl = - identity_relocation_list_for_metavariable context_for_newmeta in - let newmetaty = CicSubstitution.lift 1 ty in - let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta (newmeta,irl)) in - let (newproof, _) = - subst_meta_in_proof - proof metano bo'[newmeta,context_for_newmeta,newmetaty] - in - (newproof, [newmeta]) - - (** functional part of the "exact" tactic *) -let exact_tac ~term ~status:(proof, goal) = - (* Assumption: the term bo must be closed in the current context *) - let (_,metasenv,_,_) = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let module T = CicTypeChecker in - let module R = CicReduction in - if R.are_convertible context (T.type_of_aux' metasenv context term) ty then - begin - let (newproof, metasenv') = - subst_meta_in_proof proof metano term [] in - (newproof, []) - end - else - raise (Fail "The type of the provided term is not the one expected.") - - -(* not really "primitive" tactics .... *) - -let elim_tac ~term ~status:(proof, goal) = - let module T = CicTypeChecker in - let module U = UriManager in - let module R = CicReduction in - let module C = Cic in - let (curi,metasenv,_,_) = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let termty = T.type_of_aux' metasenv context term in - let uri,exp_named_subst,typeno,args = - match termty with - C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) - | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) -> - (uri,exp_named_subst,typeno,args) - | _ -> raise NotAnInductiveTypeToEliminate - in - let eliminator_uri = - let buri = U.buri_of_uri uri in - let name = - match CicEnvironment.get_obj uri with - C.InductiveDefinition (tys,_,_) -> - let (name,_,_,_) = List.nth tys typeno in - name - | _ -> assert false - in - let ext = - match T.type_of_aux' metasenv context ty with - C.Sort C.Prop -> "_ind" - | C.Sort C.Set -> "_rec" - | C.Sort C.Type -> "_rect" - | _ -> assert false - in - U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") - in - let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in - let ety = T.type_of_aux' metasenv context eliminator_ref in - let newmeta = new_meta ~proof in - let (econclusion,newmetas,arguments,lastmeta) = - new_metasenv_for_apply newmeta proof context ety - in - (* Here we assume that we have only one inductive hypothesis to *) - (* eliminate and that it is the last hypothesis of the theorem. *) - (* A better approach would be fingering the hypotheses in some *) - (* way. *) - let meta_of_corpse = - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=(lastmeta - 1)) newmetas - in - let irl = - identity_relocation_list_for_metavariable canonical_context - in - Cic.Meta (lastmeta - 1, irl) - in - let newmetasenv = newmetas @ metasenv in - let subst1,newmetasenv' = - CicUnification.fo_unif newmetasenv context term meta_of_corpse - in - let ueconclusion = CicUnification.apply_subst subst1 econclusion in - (* The conclusion of our elimination principle is *) - (* (?i farg1 ... fargn) *) - (* The conclusion of our goal is ty. So, we can *) - (* eta-expand ty w.r.t. farg1 .... fargn to get *) - (* a new ty equal to (P farg1 ... fargn). Now *) - (* ?i can be instantiated with P and we are ready *) - (* to refine the term. *) - let emeta, fargs = - match ueconclusion with - C.Appl ((C.Meta (emeta,_))::fargs) -> emeta,fargs - | C.Meta (emeta,_) -> emeta,[] - | _ -> raise NotTheRightEliminatorShape - in - let ty' = CicUnification.apply_subst subst1 ty in - let eta_expanded_ty = -(*CSC: newmetasenv' era metasenv ??????????? *) - List.fold_left (eta_expand newmetasenv' context) ty' fargs - in - let subst2,newmetasenv'' = -(*CSC: passo newmetasenv', ma alcune variabili sono gia' state sostituite -da subst1!!!! Dovrei rimuoverle o sono innocue?*) - CicUnification.fo_unif - newmetasenv' context ueconclusion eta_expanded_ty - in - let in_subst_domain i = - let eq_to_i = function (j,_) -> i=j in - List.exists eq_to_i subst1 || - List.exists eq_to_i subst2 - in - (* When unwinding the META that corresponds to the elimination *) - (* predicate (which is emeta), we must also perform one-step *) - (* beta-reduction. apply_subst doesn't need the context. Hence *) - (* the underscore. *) - let apply_subst _ t = - let t' = CicUnification.apply_subst subst1 t in - CicUnification.apply_subst_reducing - subst2 (Some (emeta,List.length fargs)) t' - in - let old_uninstantiatedmetas,new_uninstantiatedmetas = - classify_metas newmeta in_subst_domain apply_subst - newmetasenv'' - in - let arguments' = List.map (apply_subst context) arguments in - let bo' = Cic.Appl (eliminator_ref::arguments') in - let newmetasenv''' = - new_uninstantiatedmetas@old_uninstantiatedmetas - in - let (newproof, newmetasenv'''') = - (* When unwinding the META that corresponds to the *) - (* elimination predicate (which is emeta), we must *) - (* also perform one-step beta-reduction. *) - (* The only difference w.r.t. apply_subst is that *) - (* we also substitute metano with bo'. *) - (*CSC: Nota: sostituire nuovamente subst1 e' superfluo, *) - (*CSC: no? *) - let apply_subst' t = - let t' = CicUnification.apply_subst subst1 t in - CicUnification.apply_subst_reducing - ((metano,bo')::subst2) - (Some (emeta,List.length fargs)) t' - in - subst_meta_and_metasenv_in_proof - proof metano apply_subst' newmetasenv''' - in - (newproof, - List.map (function (i,_,_) -> i) new_uninstantiatedmetas) -;; - -(* The simplification is performed only on the conclusion *) -let elim_intros_simpl_tac ~term = - Tacticals.then_ ~start:(elim_tac ~term) - ~continuation: - (Tacticals.thens - ~start:intros_tac - ~continuations: - [ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None]) -;; - -exception NotConvertible - -(*CSC: Bug (or feature?). [with_what] is parsed in the context of the goal, *) -(*CSC: while [what] can have a richer context (because of binders) *) -(*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *) -(*CSC: Is that evident? Is that right? Or should it be changed? *) -let change_tac ~what ~with_what ~status:(proof, goal) = - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - (* are_convertible works only on well-typed terms *) - ignore (CicTypeChecker.type_of_aux' metasenv context with_what) ; - if CicReduction.are_convertible context what with_what then - begin - let replace = - ProofEngineReduction.replace ~equality:(==) ~what ~with_what - in - let ty' = replace 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 - in - let metasenv' = - List.map - (function - (n,_,_) when n = metano -> (metano,context',ty') - | _ as t -> t - ) metasenv - in - (curi,metasenv',pbo,pty), [metano] - end - else - raise (ProofEngineTypes.Fail "Not convertible") diff --git a/helm/gTopLevel/primitiveTactics.mli b/helm/gTopLevel/primitiveTactics.mli deleted file mode 100644 index dad385339..000000000 --- a/helm/gTopLevel/primitiveTactics.mli +++ /dev/null @@ -1,41 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -val apply_tac: - term: Cic.term -> ProofEngineTypes.tactic -val exact_tac: - term: Cic.term -> ProofEngineTypes.tactic -val intros_tac: - ProofEngineTypes.tactic -val cut_tac: - term: Cic.term -> ProofEngineTypes.tactic -val letin_tac: - term: Cic.term -> ProofEngineTypes.tactic - -val elim_intros_simpl_tac: - term: Cic.term -> ProofEngineTypes.tactic - -val change_tac: - what: Cic.term -> with_what: Cic.term -> ProofEngineTypes.tactic diff --git a/helm/gTopLevel/proofEngineHelpers.ml b/helm/gTopLevel/proofEngineHelpers.ml deleted file mode 100644 index 74b6fcdac..000000000 --- a/helm/gTopLevel/proofEngineHelpers.ml +++ /dev/null @@ -1,122 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(*CSC: generatore di nomi? Chiedere il nome? *) -let fresh_name = - let next_fresh_index = ref 0 in - function - Cic.Anonymous -> - incr next_fresh_index ; - "fresh_name" ^ string_of_int !next_fresh_index - | Cic.Name name -> - incr next_fresh_index ; - name ^ string_of_int !next_fresh_index - -(* identity_relocation_list_for_metavariable i canonical_context *) -(* returns the identity relocation list, which is the list [1 ; ... ; n] *) -(* where n = List.length [canonical_context] *) -(*CSC: ma mi basta la lunghezza del contesto canonico!!!*) -let identity_relocation_list_for_metavariable canonical_context = - let canonical_context_length = List.length canonical_context in - let rec aux = - function - (_,[]) -> [] - | (n,None::tl) -> None::(aux ((n+1),tl)) - | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl)) - in - aux (1,canonical_context) - -(* Returns the first meta whose number is above the *) -(* number of the higher meta. *) -let new_meta ~proof = - let (_,metasenv,_,_) = proof in - let rec aux = - function - None,[] -> 1 - | Some n,[] -> n - | None,(n,_,_)::tl -> aux (Some n,tl) - | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl) - in - 1 + aux (None,metasenv) - -let subst_meta_in_proof proof meta term newmetasenv = - let uri,metasenv,bo,ty = proof in - let subst_in = CicUnification.apply_subst [meta,term] in - let metasenv' = - newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv) - in - let metasenv'' = - List.map - (function i,canonical_context,ty -> - let canonical_context' = - List.map - (function - Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s)) - | Some (n,Cic.Def s) -> Some (n,Cic.Def (subst_in s)) - | None -> None - ) canonical_context - in - i,canonical_context',(subst_in ty) - ) metasenv' - in - let bo' = subst_in bo in - let newproof = uri,metasenv'',bo',ty in - (newproof, metasenv'') - -(*CSC: commento vecchio *) -(* refine_meta_with_brand_new_metasenv meta term subst_in 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: Attenzione! Ora questa funzione applica anche [subst_in] a *) -(*CSC: [newmetasenv]. *) -let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv = - let (uri,_,bo,ty) = proof in - let bo' = subst_in bo in - let metasenv' = - List.fold_right - (fun metasenv_entry i -> - match metasenv_entry with - (m,canonical_context,ty) when m <> meta -> - let canonical_context' = - List.map - (function - None -> None - | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t)) - | Some (i,Cic.Def t) -> Some (i,Cic.Def (subst_in t)) - ) canonical_context - in - (m,canonical_context',subst_in ty)::i - | _ -> i - ) newmetasenv [] - in - let newproof = uri,metasenv',bo',ty in - (newproof, metasenv') - diff --git a/helm/gTopLevel/proofEngineHelpers.mli b/helm/gTopLevel/proofEngineHelpers.mli deleted file mode 100644 index de0b37596..000000000 --- a/helm/gTopLevel/proofEngineHelpers.mli +++ /dev/null @@ -1,45 +0,0 @@ -(* Copyright (C) 2000-2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -val fresh_name : Cic.name -> string - -(* identity_relocation_list_for_metavariable i canonical_context *) -(* returns the identity relocation list, which is the list [1 ; ... ; n] *) -(* where n = List.length [canonical_context] *) -val identity_relocation_list_for_metavariable : - 'a option list -> Cic.term option list - -(* Returns the first meta whose number is above the *) -(* number of the higher meta. *) -val new_meta : proof:ProofEngineTypes.proof -> int - -val subst_meta_in_proof : - ProofEngineTypes.proof -> - int -> Cic.term -> Cic.metasenv -> - ProofEngineTypes.proof * Cic.metasenv -val subst_meta_and_metasenv_in_proof : - ProofEngineTypes.proof -> - int -> (Cic.term -> Cic.term) -> Cic.metasenv -> - ProofEngineTypes.proof * Cic.metasenv diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml deleted file mode 100644 index 710a48164..000000000 --- a/helm/gTopLevel/proofEngineReduction.ml +++ /dev/null @@ -1,826 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 12/04/2002 *) -(* *) -(* *) -(******************************************************************************) - - -(* The code of this module is derived from the code of CicReduction *) - -exception Impossible of int;; -exception ReferenceToConstant;; -exception ReferenceToVariable;; -exception ReferenceToCurrentProof;; -exception ReferenceToInductiveDefinition;; -exception WrongUriToInductiveDefinition;; -exception WrongUriToConstant;; -exception RelToHiddenHypothesis;; - -let alpha_equivalence = - let module C = Cic in - let rec aux t t' = - if t = t' then true - else - match t,t' with - C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2) -> - UriManager.eq uri1 uri2 && - aux_exp_named_subst exp_named_subst1 exp_named_subst2 - | C.Cast (te,ty), C.Cast (te',ty') -> - aux te te' && aux ty ty' - | C.Prod (_,s,t), C.Prod (_,s',t') -> - aux s s' && aux t t' - | C.Lambda (_,s,t), C.Lambda (_,s',t') -> - aux s s' && aux t t' - | C.LetIn (_,s,t), C.LetIn(_,s',t') -> - aux s s' && aux t t' - | C.Appl l, C.Appl l' -> - (try - List.fold_left2 - (fun b t1 t2 -> b && aux t1 t2) true l l' - with - Invalid_argument _ -> false) - | C.Const (uri,exp_named_subst1), C.Const (uri',exp_named_subst2) -> - UriManager.eq uri uri' && - aux_exp_named_subst exp_named_subst1 exp_named_subst2 - | C.MutInd (uri,i,exp_named_subst1), C.MutInd (uri',i',exp_named_subst2) -> - UriManager.eq uri uri' && i = i' && - aux_exp_named_subst exp_named_subst1 exp_named_subst2 - | C.MutConstruct (uri,i,j,exp_named_subst1), - C.MutConstruct (uri',i',j',exp_named_subst2) -> - UriManager.eq uri uri' && i = i' && j = j' && - aux_exp_named_subst exp_named_subst1 exp_named_subst2 - | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') -> - UriManager.eq sp sp' && i = i' && - aux outt outt' && aux t t' && - (try - List.fold_left2 - (fun b t1 t2 -> b && aux t1 t2) true pl pl' - with - Invalid_argument _ -> false) - | C.Fix (i,fl), C.Fix (i',fl') -> - i = i' && - (try - List.fold_left2 - (fun b (_,i,ty,bo) (_,i',ty',bo') -> - b && i = i' && aux ty ty' && aux bo bo' - ) true fl fl' - with - Invalid_argument _ -> false) - | C.CoFix (i,fl), C.CoFix (i',fl') -> - i = i' && - (try - List.fold_left2 - (fun b (_,ty,bo) (_,ty',bo') -> - b && aux ty ty' && aux bo bo' - ) true fl fl' - with - Invalid_argument _ -> false) - | _,_ -> false (* we already know that t != t' *) - and aux_exp_named_subst exp_named_subst1 exp_named_subst2 = - try - List.fold_left2 - (fun b (uri1,t1) (uri2,t2) -> - b && UriManager.eq uri1 uri2 && aux t1 t2 - ) true exp_named_subst1 exp_named_subst2 - with - Invalid_argument _ -> false - in - aux -;; - -(* "textual" replacement of a subterm with another one *) -let replace ~equality ~what ~with_what ~where = - let module C = Cic in - let rec aux = - function - t when (equality t what) -> with_what - | C.Rel _ as t -> t - | C.Var (uri,exp_named_subst) -> - C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst) - | C.Meta _ as t -> t - | C.Sort _ as t -> t - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (aux te, aux ty) - | 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 -> - (* 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 (uri,exp_named_subst) -> - C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst) - | C.MutInd (uri,i,exp_named_subst) -> - C.MutInd - (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst) - | C.MutConstruct (uri,i,j,exp_named_subst) -> - C.MutConstruct - (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst) - | C.MutCase (sp,i,outt,t,pl) -> - C.MutCase (sp,i,aux outt, aux t,List.map aux pl) - | C.Fix (i,fl) -> - let substitutedfl = - List.map - (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo)) - fl - in - C.Fix (i, substitutedfl) - | C.CoFix (i,fl) -> - let substitutedfl = - List.map - (fun (name,ty,bo) -> (name, aux ty, aux bo)) - fl - in - C.CoFix (i, substitutedfl) - in - aux where -;; - -(* replaces in a term a term with another one. *) -(* Lifting are performed as usual. *) -let replace_lifting ~equality ~what ~with_what ~where = - let rec substaux k what = - let module C = Cic in - let module S = CicSubstitution in - function - t when (equality t what) -> S.lift (k-1) with_what - | C.Rel n as t -> t - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst - in - C.Var (uri,exp_named_subst') - | C.Meta (i, l) as t -> - let l' = - List.map - (function - None -> None - | Some t -> Some (substaux k what t) - ) l - in - C.Meta(i,l') - | C.Sort _ as t -> t - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty) - | C.Prod (n,s,t) -> - C.Prod (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t) - | C.Lambda (n,s,t) -> - C.Lambda (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t) - | C.LetIn (n,s,t) -> - C.LetIn (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t) - | C.Appl (he::tl) -> - (* Invariant: no Appl applied to another Appl *) - let tl' = List.map (substaux k what) tl in - begin - match substaux k what he with - C.Appl l -> C.Appl (l@tl') - | _ as he' -> C.Appl (he'::tl') - end - | C.Appl _ -> assert false - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst - in - C.Const (uri,exp_named_subst') - | C.MutInd (uri,i,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst - in - C.MutInd (uri,i,exp_named_subst') - | C.MutConstruct (uri,i,j,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst - in - C.MutConstruct (uri,i,j,exp_named_subst') - | C.MutCase (sp,i,outt,t,pl) -> - C.MutCase (sp,i,substaux k what outt, substaux k what t, - List.map (substaux k what) pl) - | C.Fix (i,fl) -> - let len = List.length fl in - let substitutedfl = - List.map - (fun (name,i,ty,bo) -> - (name, i, substaux k what ty, substaux (k+len) (S.lift len what) bo)) - fl - in - C.Fix (i, substitutedfl) - | C.CoFix (i,fl) -> - let len = List.length fl in - let substitutedfl = - List.map - (fun (name,ty,bo) -> - (name, substaux k what ty, substaux (k+len) (S.lift len what) bo)) - fl - in - C.CoFix (i, substitutedfl) - in - substaux 1 what where -;; - -(* replaces in a term a term with another one. *) -(* Lifting are performed as usual. *) -let replace_lifting_csc nnn ~equality ~what ~with_what ~where = - let rec substaux k = - let module C = Cic in - let module S = CicSubstitution in - function - t when (equality t what) -> S.lift (k-1) with_what - | C.Rel n as t -> - if n < k then C.Rel n else C.Rel (n + nnn) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k t) exp_named_subst - in - C.Var (uri,exp_named_subst') - | C.Meta (i, l) as t -> - let l' = - List.map - (function - None -> None - | Some t -> Some (substaux k t) - ) l - in - C.Meta(i,l') - | C.Sort _ as t -> t - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) - | C.Prod (n,s,t) -> - C.Prod (n, substaux k s, substaux (k + 1) t) - | C.Lambda (n,s,t) -> - C.Lambda (n, substaux k s, substaux (k + 1) t) - | C.LetIn (n,s,t) -> - C.LetIn (n, substaux k s, substaux (k + 1) t) - | C.Appl (he::tl) -> - (* Invariant: no Appl applied to another Appl *) - let tl' = List.map (substaux k) tl in - begin - match substaux k he with - C.Appl l -> C.Appl (l@tl') - | _ as he' -> C.Appl (he'::tl') - end - | C.Appl _ -> assert false - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k t) exp_named_subst - in - C.Const (uri,exp_named_subst') - | C.MutInd (uri,i,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k t) exp_named_subst - in - C.MutInd (uri,i,exp_named_subst') - | C.MutConstruct (uri,i,j,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k t) exp_named_subst - in - C.MutConstruct (uri,i,j,exp_named_subst') - | C.MutCase (sp,i,outt,t,pl) -> - C.MutCase (sp,i,substaux k outt, substaux k t, - List.map (substaux k) pl) - | C.Fix (i,fl) -> - let len = List.length fl in - let substitutedfl = - List.map - (fun (name,i,ty,bo) -> - (name, i, substaux k ty, substaux (k+len) bo)) - fl - in - C.Fix (i, substitutedfl) - | C.CoFix (i,fl) -> - let len = List.length fl in - let substitutedfl = - List.map - (fun (name,ty,bo) -> - (name, substaux k ty, substaux (k+len) bo)) - fl - in - C.CoFix (i, substitutedfl) - in -let res = - substaux 1 where -in prerr_endline ("@@@@ risultato replace: " ^ (CicPp.ppterm res)); res -;; - -(* Takes a well-typed term and fully reduces it. *) -(*CSC: It does not perform reduction in a Case *) -let reduce context = - let rec reduceaux context l = - let module C = Cic in - let module S = CicSubstitution in - function - C.Rel n as t -> - (match List.nth context (n-1) with - Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l) - | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo) - | None -> raise RelToHiddenHypothesis - ) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - (match CicEnvironment.get_obj uri with - C.Constant _ -> raise ReferenceToConstant - | C.CurrentProof _ -> raise ReferenceToCurrentProof - | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - | C.Variable (_,None,_,_) -> - let t' = C.Var (uri,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.Variable (_,Some body,_,_) -> - (reduceaux context l - (CicSubstitution.subst_vars exp_named_subst' body)) - ) - | C.Meta _ as t -> if l = [] then t else C.Appl (t::l) - | C.Sort _ as t -> t (* l should be empty *) - | C.Implicit as t -> t - | C.Cast (te,ty) -> - C.Cast (reduceaux context l te, reduceaux context l ty) - | C.Prod (name,s,t) -> - assert (l = []) ; - C.Prod (name, - reduceaux context [] s, - reduceaux ((Some (name,C.Decl s))::context) [] t) - | C.Lambda (name,s,t) -> - (match l with - [] -> - C.Lambda (name, - reduceaux context [] s, - reduceaux ((Some (name,C.Decl s))::context) [] t) - | he::tl -> reduceaux context tl (S.subst he t) - (* when name is Anonimous the substitution should be superfluous *) - ) - | C.LetIn (n,s,t) -> - reduceaux context l (S.subst (reduceaux context [] s) t) - | C.Appl (he::tl) -> - let tl' = List.map (reduceaux context []) tl in - reduceaux context (tl'@l) he - | C.Appl [] -> raise (Impossible 1) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - (match CicEnvironment.get_obj uri with - C.Constant (_,Some body,_,_) -> - (reduceaux context l - (CicSubstitution.subst_vars exp_named_subst' body)) - | C.Constant (_,None,_,_) -> - let t' = C.Const (uri,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.Variable _ -> raise ReferenceToVariable - | C.CurrentProof (_,_,body,_,_) -> - (reduceaux context l - (CicSubstitution.subst_vars exp_named_subst' body)) - | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - ) - | C.MutInd (uri,i,exp_named_subst) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - let t' = C.MutInd (uri,i,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.MutConstruct (uri,i,j,exp_named_subst) as t -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - let t' = C.MutConstruct (uri,i,j,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.MutCase (mutind,i,outtype,term,pl) -> - let decofix = - function - C.CoFix (i,fl) as t -> - let tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl - in - let (_,_,body) = List.nth fl i in - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) - fl - body - in - reduceaux context [] body' - | C.Appl (C.CoFix (i,fl) :: tl) -> - let tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl - in - let (_,_,body) = List.nth fl i in - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) - fl - body - in - let tl' = List.map (reduceaux context []) tl in - reduceaux context tl' body' - | t -> t - in - (match decofix (reduceaux context [] term) with - C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1)) - | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> - let (arity, r) = - match CicEnvironment.get_obj mutind with - C.InductiveDefinition (tl,_,r) -> - let (_,_,arity,_) = List.nth tl i in - (arity,r) - | _ -> raise WrongUriToInductiveDefinition - in - let ts = - let rec eat_first = - function - (0,l) -> l - | (n,he::tl) when n > 0 -> eat_first (n - 1, tl) - | _ -> raise (Impossible 5) - in - eat_first (r,tl) - in - reduceaux context (ts@l) (List.nth pl (j-1)) - | C.Cast _ | C.Implicit -> - raise (Impossible 2) (* we don't trust our whd ;-) *) - | _ -> - let outtype' = reduceaux context [] outtype in - let term' = reduceaux context [] term in - let pl' = List.map (reduceaux context []) pl in - let res = - C.MutCase (mutind,i,outtype',term',pl') - in - if l = [] then res else C.Appl (res::l) - ) - | C.Fix (i,fl) -> - let tys = - List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl - in - let t' () = - let fl' = - List.map - (function (n,recindex,ty,bo) -> - (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo) - ) fl - in - C.Fix (i, fl') - in - let (_,recindex,_,body) = List.nth fl i in - let recparam = - try - Some (List.nth l recindex) - with - _ -> None - in - (match recparam with - Some recparam -> - (match reduceaux context [] recparam with - C.MutConstruct _ - | C.Appl ((C.MutConstruct _)::_) -> - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl))) - fl - body - in - (* Possible optimization: substituting whd recparam in l*) - reduceaux context l body' - | _ -> if l = [] then t' () else C.Appl ((t' ())::l) - ) - | None -> if l = [] then t' () else C.Appl ((t' ())::l) - ) - | C.CoFix (i,fl) -> - let tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl - in - let t' = - let fl' = - List.map - (function (n,ty,bo) -> - (n,reduceaux context [] ty, reduceaux (tys@context) [] bo) - ) fl - in - C.CoFix (i, fl') - in - if l = [] then t' else C.Appl (t'::l) - and reduceaux_exp_named_subst context l = - List.map (function uri,t -> uri,reduceaux context [] t) - in - reduceaux context [] -;; - -exception WrongShape;; -exception AlreadySimplified;; - -(* Takes a well-typed term and *) -(* 1) Performs beta-iota-zeta reduction until delta reduction is needed *) -(* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *) -(* w.r.t. zero or more variables and if the Fix can be reduced, than it *) -(* is reduced, the delta-reduction is succesfull and the whole algorithm *) -(* is applied again to the new redex; Step 3) is applied to the result *) -(* of the recursive simplification. Otherwise, if the Fix can not be *) -(* reduced, than the delta-reductions fails and the delta-redex is *) -(* not reduced. Otherwise, if the delta-residual is not the *) -(* lambda-abstraction of a Fix, then it is reduced and the result is *) -(* directly returned, without performing step 3). *) -(* 3) Folds the application of the constant to the arguments that did not *) -(* change in every iteration, i.e. to the actual arguments for the *) -(* lambda-abstractions that precede the Fix. *) -(*CSC: It does not perform simplification in a Case *) -let simpl context = - (* reduceaux is equal to the reduceaux locally defined inside *) - (* reduce, but for the const case. *) - (**** Step 1 ****) - let rec reduceaux context l = - let module C = Cic in - let module S = CicSubstitution in - function - C.Rel n as t -> - (match List.nth context (n-1) with - Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l) - | Some (_,C.Def bo) -> - try_delta_expansion l t (S.lift n bo) - | None -> raise RelToHiddenHypothesis - ) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - (match CicEnvironment.get_obj uri with - C.Constant _ -> raise ReferenceToConstant - | C.CurrentProof _ -> raise ReferenceToCurrentProof - | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - | C.Variable (_,None,_,_) -> - let t' = C.Var (uri,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.Variable (_,Some body,_,_) -> - reduceaux context l - (CicSubstitution.subst_vars exp_named_subst' body) - ) - | C.Meta _ as t -> if l = [] then t else C.Appl (t::l) - | C.Sort _ as t -> t (* l should be empty *) - | C.Implicit as t -> t - | C.Cast (te,ty) -> - C.Cast (reduceaux context l te, reduceaux context l ty) - | C.Prod (name,s,t) -> - assert (l = []) ; - C.Prod (name, - reduceaux context [] s, - reduceaux ((Some (name,C.Decl s))::context) [] t) - | C.Lambda (name,s,t) -> - (match l with - [] -> - C.Lambda (name, - reduceaux context [] s, - reduceaux ((Some (name,C.Decl s))::context) [] t) - | he::tl -> reduceaux context tl (S.subst he t) - (* when name is Anonimous the substitution should be superfluous *) - ) - | C.LetIn (n,s,t) -> - reduceaux context l (S.subst (reduceaux context [] s) t) - | C.Appl (he::tl) -> - let tl' = List.map (reduceaux context []) tl in - reduceaux context (tl'@l) he - | C.Appl [] -> raise (Impossible 1) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - (match CicEnvironment.get_obj uri with - C.Constant (_,Some body,_,_) -> - try_delta_expansion l - (C.Const (uri,exp_named_subst')) - (CicSubstitution.subst_vars exp_named_subst' body) - | C.Constant (_,None,_,_) -> - let t' = C.Const (uri,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.Variable _ -> raise ReferenceToVariable - | C.CurrentProof (_,_,body,_,_) -> reduceaux context l body - | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - ) - | C.MutInd (uri,i,exp_named_subst) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - let t' = C.MutInd (uri,i,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.MutConstruct (uri,i,j,exp_named_subst) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - let t' = C.MutConstruct(uri,i,j,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.MutCase (mutind,i,outtype,term,pl) -> - let decofix = - function - C.CoFix (i,fl) as t -> - let tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in - let (_,_,body) = List.nth fl i in - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) - fl - body - in - reduceaux context [] body' - | C.Appl (C.CoFix (i,fl) :: tl) -> - let tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in - let (_,_,body) = List.nth fl i in - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) - fl - body - in - let tl' = List.map (reduceaux context []) tl in - reduceaux context tl body' - | t -> t - in - (match decofix (reduceaux context [] term) with - C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1)) - | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> - let (arity, r) = - match CicEnvironment.get_obj mutind with - C.InductiveDefinition (tl,ingredients,r) -> - let (_,_,arity,_) = List.nth tl i in - (arity,r) - | _ -> raise WrongUriToInductiveDefinition - in - let ts = - let rec eat_first = - function - (0,l) -> l - | (n,he::tl) when n > 0 -> eat_first (n - 1, tl) - | _ -> raise (Impossible 5) - in - eat_first (r,tl) - in - reduceaux context (ts@l) (List.nth pl (j-1)) - | C.Cast _ | C.Implicit -> - raise (Impossible 2) (* we don't trust our whd ;-) *) - | _ -> - let outtype' = reduceaux context [] outtype in - let term' = reduceaux context [] term in - let pl' = List.map (reduceaux context []) pl in - let res = - C.MutCase (mutind,i,outtype',term',pl') - in - if l = [] then res else C.Appl (res::l) - ) - | C.Fix (i,fl) -> - let tys = - List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl - in - let t' () = - let fl' = - List.map - (function (n,recindex,ty,bo) -> - (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo) - ) fl - in - C.Fix (i, fl') - in - let (_,recindex,_,body) = List.nth fl i in - let recparam = - try - Some (List.nth l recindex) - with - _ -> None - in - (match recparam with - Some recparam -> - (match reduceaux context [] recparam with - C.MutConstruct _ - | C.Appl ((C.MutConstruct _)::_) -> - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl))) - fl - body - in - (* Possible optimization: substituting whd recparam in l*) - reduceaux context l body' - | _ -> if l = [] then t' () else C.Appl ((t' ())::l) - ) - | None -> if l = [] then t' () else C.Appl ((t' ())::l) - ) - | C.CoFix (i,fl) -> - let tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl - in - let t' = - let fl' = - List.map - (function (n,ty,bo) -> - (n,reduceaux context [] ty, reduceaux (tys@context) [] bo) - ) fl - in - C.CoFix (i, fl') - in - if l = [] then t' else C.Appl (t'::l) - and reduceaux_exp_named_subst context l = - List.map (function uri,t -> uri,reduceaux context [] t) - (**** Step 2 ****) - and try_delta_expansion l term body = - let module C = Cic in - let module S = CicSubstitution in - try - let res,constant_args = - let rec aux rev_constant_args l = - function - C.Lambda (name,s,t) as t' -> - begin - match l with - [] -> raise WrongShape - | he::tl -> - (* when name is Anonimous the substitution should *) - (* be superfluous *) - aux (he::rev_constant_args) tl (S.subst he t) - end - | C.LetIn (_,s,t) -> - aux rev_constant_args l (S.subst s t) - | C.Fix (i,fl) as t -> - let tys = - List.map (function (name,_,ty,_) -> - Some (C.Name name, C.Decl ty)) fl - in - let (_,recindex,_,body) = List.nth fl i in - let recparam = - try - List.nth l recindex - with - _ -> raise AlreadySimplified - in - (match CicReduction.whd context recparam with - C.MutConstruct _ - | C.Appl ((C.MutConstruct _)::_) -> - let body' = - let counter = ref (List.length fl) in - List.fold_right - (function _ -> - decr counter ; S.subst (C.Fix (!counter,fl)) - ) fl body - in - (* Possible optimization: substituting whd *) - (* recparam in l *) - reduceaux context l body', - List.rev rev_constant_args - | _ -> raise AlreadySimplified - ) - | _ -> raise WrongShape - in - aux [] l body - in - (**** Step 3 ****) - let term_to_fold, delta_expanded_term_to_fold = - match constant_args with - [] -> term,body - | _ -> C.Appl (term::constant_args), C.Appl (body::constant_args) - in - let simplified_term_to_fold = - reduceaux context [] delta_expanded_term_to_fold - in - replace (=) simplified_term_to_fold term_to_fold res - with - WrongShape -> - (* The constant does not unfold to a Fix lambda-abstracted *) - (* w.r.t. zero or more variables. We just perform reduction.*) - reduceaux context l body - | AlreadySimplified -> - (* If we performed delta-reduction, we would find a Fix *) - (* not applied to a constructor. So, we refuse to perform *) - (* delta-reduction. *) - if l = [] then term else C.Appl (term::l) - in - reduceaux context [] -;; diff --git a/helm/gTopLevel/proofEngineReduction.mli b/helm/gTopLevel/proofEngineReduction.mli deleted file mode 100644 index 91bce1a39..000000000 --- a/helm/gTopLevel/proofEngineReduction.mli +++ /dev/null @@ -1,47 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -exception Impossible of int -exception ReferenceToConstant -exception ReferenceToVariable -exception ReferenceToCurrentProof -exception ReferenceToInductiveDefinition -exception WrongUriToInductiveDefinition -exception RelToHiddenHypothesis -exception WrongShape -exception AlreadySimplified - -val alpha_equivalence: Cic.term -> Cic.term -> bool -val replace : - equality:(Cic.term -> 'a -> bool) -> - what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term -val replace_lifting : - equality:(Cic.term -> Cic.term -> bool) -> - what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term -val replace_lifting_csc : - int -> equality:(Cic.term -> Cic.term -> bool) -> - what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term -val reduce : Cic.context -> Cic.term -> Cic.term -val simpl : Cic.context -> Cic.term -> Cic.term diff --git a/helm/gTopLevel/proofEngineStructuralRules.ml b/helm/gTopLevel/proofEngineStructuralRules.ml deleted file mode 100644 index d89420f58..000000000 --- a/helm/gTopLevel/proofEngineStructuralRules.ml +++ /dev/null @@ -1,149 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -open ProofEngineTypes - -let clearbody ~hyp ~status:(proof, goal) = - let module C = Cic in - match hyp with - 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 = proof in - let metano,_,_ = List.find (function (m,_,_) -> m=goal) metasenv in - let string_of_name = - function - C.Name n -> n - | C.Anonymous -> "_" - 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 - (curi,metasenv',pbo,pty), [goal] - -let clear ~hyp:hyp_to_clear ~status:(proof, goal) = - let module C = Cic in - match hyp_to_clear with - None -> assert false - | Some (n_to_clear, _) -> - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = - List.find (function (m,_,_) -> m=goal) metasenv - in - let string_of_name = - function - C.Name n -> n - | C.Anonymous -> "_" - 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 - (curi,metasenv',pbo,pty), [goal] - diff --git a/helm/gTopLevel/proofEngineStructuralRules.mli b/helm/gTopLevel/proofEngineStructuralRules.mli deleted file mode 100644 index 32ba812ac..000000000 --- a/helm/gTopLevel/proofEngineStructuralRules.mli +++ /dev/null @@ -1,27 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -val clearbody: hyp: Cic.hypothesis -> ProofEngineTypes.tactic -val clear: hyp: Cic.hypothesis -> ProofEngineTypes.tactic diff --git a/helm/gTopLevel/proofEngineTypes.ml b/helm/gTopLevel/proofEngineTypes.ml deleted file mode 100644 index f5e75fc47..000000000 --- a/helm/gTopLevel/proofEngineTypes.ml +++ /dev/null @@ -1,41 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - - (** - current proof (proof uri * metas * (in)complete proof * term to be prooved) - *) -type proof = UriManager.uri * Cic.metasenv * Cic.term * Cic.term - (** current goal, integer index *) -type goal = int - (** - a tactic: make a transition from one status to another one or, usually, - raise a "Fail" (@see Fail) exception in case of failure - *) - (** an unfinished proof with the optional current goal *) -type tactic = status:(proof * goal) -> proof * goal list - - (** tactic failure *) -exception Fail of string - diff --git a/helm/gTopLevel/reductionTactics.ml b/helm/gTopLevel/reductionTactics.ml deleted file mode 100644 index 54b439b25..000000000 --- a/helm/gTopLevel/reductionTactics.ml +++ /dev/null @@ -1,127 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* -let reduction_tac ~reduction ~status:(proof,goal) = - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let new_ty = reduction context ty in - let new_metasenv = - List.map - (function - (n,_,_) when n = metano -> (metano,context,new_ty) - | _ as t -> t - ) metasenv - in - (curi,new_metasenv,pbo,pty), [metano] -;; -*) - -(* The default of term is the thesis of the goal to be prooved *) -let reduction_tac ~also_in_hypotheses ~reduction ~term ~status:(proof,goal) = - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let term = - match term with None -> ty | Some t -> t - 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: 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 context term in - ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term' - ~where:where - with - _ -> where - in - let ty' = replace context ty in - let context' = - if also_in_hypotheses then - 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 [] - else - context - in - let metasenv' = - List.map - (function - (n,_,_) when n = metano -> (metano,context',ty') - | _ as t -> t - ) metasenv - in - (curi,metasenv',pbo,pty), [metano] -;; - -let simpl_tac = reduction_tac ~reduction:ProofEngineReduction.simpl ;; -let reduce_tac = reduction_tac ~reduction:ProofEngineReduction.reduce ;; -let whd_tac = reduction_tac ~reduction:CicReduction.whd ;; - -let fold_tac ~reduction ~also_in_hypotheses ~term ~status:(proof,goal) = - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let term' = reduction 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 - in - let ty' = replace ty in - let metasenv' = - let context' = - if also_in_hypotheses then - List.map - (function - Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t)) - | Some (n,Cic.Def t) -> Some (n,Cic.Def (replace t)) - | None -> None - ) context - else - context - in - List.map - (function - (n,_,_) when n = metano -> (metano,context',ty') - | _ as t -> t - ) metasenv - - in - (curi,metasenv',pbo,pty), [metano] -;; diff --git a/helm/gTopLevel/reductionTactics.mli b/helm/gTopLevel/reductionTactics.mli deleted file mode 100644 index 8df6c2468..000000000 --- a/helm/gTopLevel/reductionTactics.mli +++ /dev/null @@ -1,36 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* The default of term is the thesis of the goal to be prooved *) -val simpl_tac: - also_in_hypotheses:bool -> term:(Cic.term option) -> ProofEngineTypes.tactic -val reduce_tac: - also_in_hypotheses:bool -> term:(Cic.term option) -> ProofEngineTypes.tactic -val whd_tac: - also_in_hypotheses:bool -> term:(Cic.term option) -> ProofEngineTypes.tactic - -val fold_tac: - reduction:(Cic.context -> Cic.term -> Cic.term) -> - also_in_hypotheses:bool -> term:Cic.term -> ProofEngineTypes.tactic diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml deleted file mode 100644 index 25fa093f2..000000000 --- a/helm/gTopLevel/ring.ml +++ /dev/null @@ -1,594 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -open CicReduction -open PrimitiveTactics -open ProofEngineTypes -open UriManager - -(** DEBUGGING *) - - (** perform debugging output? *) -let debug = false - - (** debugging print *) -let warn s = - if debug then - prerr_endline ("RING WARNING: " ^ s) - -(** CIC URIS *) - -(** - Note: For constructors URIs aren't really URIs but rather triples of - the form (uri, typeno, consno). This discrepancy is to preserver an - uniformity of invocation of "mkXXX" functions. -*) - -let eqt_uri = uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind" -let refl_eqt_uri = (eqt_uri, 0, 1) -let equality_is_a_congruence_A = - uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/A.var" -let equality_is_a_congruence_x = - uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/x.var" -let equality_is_a_congruence_y = - uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/y.var" -let sym_eqt_uri = uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con" -let bool_uri = uri_of_string "cic:/Coq/Init/Datatypes/bool.ind" -let true_uri = (bool_uri, 0, 1) -let false_uri = (bool_uri, 0, 2) - -let r_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con" -let rplus_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con" -let rmult_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con" -let ropp_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con" -let r0_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con" -let r1_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" -let rtheory_uri = uri_of_string "cic:/Coq/Reals/Rbase/RTheory.con" - -let apolynomial_uri = - uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial.ind" -let apvar_uri = (apolynomial_uri, 0, 1) -let ap0_uri = (apolynomial_uri, 0, 2) -let ap1_uri = (apolynomial_uri, 0, 3) -let applus_uri = (apolynomial_uri, 0, 4) -let apmult_uri = (apolynomial_uri, 0, 5) -let apopp_uri = (apolynomial_uri, 0, 6) - -let quote_varmap_A_uri = uri_of_string "cic:/Coq/ring/Quote/variables_map/A.var" -let varmap_uri = uri_of_string "cic:/Coq/ring/Quote/varmap.ind" -let empty_vm_uri = (varmap_uri, 0, 1) -let node_vm_uri = (varmap_uri, 0, 2) -let varmap_find_uri = uri_of_string "cic:/Coq/ring/Quote/varmap_find.con" -let index_uri = uri_of_string "cic:/Coq/ring/Quote/index.ind" -let left_idx_uri = (index_uri, 0, 1) -let right_idx_uri = (index_uri, 0, 2) -let end_idx_uri = (index_uri, 0, 3) - -let abstract_rings_A_uri = - uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/A.var" -let abstract_rings_Aplus_uri = - uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aplus.var" -let abstract_rings_Amult_uri = - uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Amult.var" -let abstract_rings_Aone_uri = - uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aone.var" -let abstract_rings_Azero_uri = - uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Azero.var" -let abstract_rings_Aopp_uri = - uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aopp.var" -let abstract_rings_Aeq_uri = - uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aeq.var" -let abstract_rings_vm_uri = - uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/vm.var" -let abstract_rings_T_uri = - uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/T.var" -let interp_ap_uri = uri_of_string "cic:/Coq/ring/Ring_abstract/interp_ap.con" -let interp_sacs_uri = - uri_of_string "cic:/Coq/ring/Ring_abstract/interp_sacs.con" -let apolynomial_normalize_uri = - uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize.con" -let apolynomial_normalize_ok_uri = - uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize_ok.con" - -(** CIC PREDICATES *) - - (** - check whether a term is a constant or not, if argument "uri" is given and is - not "None" also check if the constant correspond to the given one or not - *) -let cic_is_const ?(uri: uri option = None) term = - match uri with - | None -> - (match term with - | Cic.Const _ -> true - | _ -> false) - | Some realuri -> - (match term with - | Cic.Const (u, _) when (eq u realuri) -> true - | _ -> false) - -(** PROOF AND GOAL ACCESSORS *) - - (** - @param proof a proof - @return the uri of a given proof - *) -let uri_of_proof ~proof:(uri, _, _, _) = uri - - (** - @param metano meta list index - @param metasenv meta list (environment) - @raise Failure if metano is not found in metasenv - @return conjecture corresponding to metano in metasenv - *) -let conj_of_metano metano = - try - List.find (function (m, _, _) -> m = metano) - with Not_found -> - failwith ( - "Ring.conj_of_metano: " ^ - (string_of_int metano) ^ " no such meta") - - (** - @param status current proof engine status - @raise Failure if proof is None - @return current goal's metasenv - *) -let metasenv_of_status ~status:((_,m,_,_), _) = m - - (** - @param status a proof engine status - @raise Failure when proof or goal are None - @return context corresponding to current goal - *) -let context_of_status ~status:(proof, goal as status) = - let metasenv = metasenv_of_status ~status:status in - let _, context, _ = List.find (function (m,_,_) -> m=goal) metasenv in - context - -(** CIC TERM CONSTRUCTORS *) - - (** - Create a Cic term consisting of a constant - @param uri URI of the constant - @proof current proof - @exp_named_subst explicit named substitution - *) -let mkConst ~uri ~exp_named_subst = - Cic.Const (uri, exp_named_subst) - - (** - Create a Cic term consisting of a constructor - @param uri triple where uri is the uri of an inductive - type, typeno is the type number in a mutind structure (0 based), consno is - the constructor number (1 based) - @exp_named_subst explicit named substitution - *) -let mkCtor ~uri:(uri, typeno, consno) ~exp_named_subst = - Cic.MutConstruct (uri, typeno, consno, exp_named_subst) - - (** - Create a Cic term consisting of a type member of a mutual induction - @param uri pair where uri is the uri of a mutual inductive - type and typeno is the type number (0 based) in the mutual induction - @exp_named_subst explicit named substitution - *) -let mkMutInd ~uri:(uri, typeno) ~exp_named_subst = - Cic.MutInd (uri, typeno, exp_named_subst) - -(** EXCEPTIONS *) - - (** - raised when the current goal is not ringable; a goal is ringable when is an - equality on reals (@see r_uri) - *) -exception GoalUnringable - -(** RING's FUNCTIONS LIBRARY *) - - (** - Check whether the ring tactic can be applied on a given term (i.e. that is - an equality on reals) - @param term to be tested - @return true if the term is ringable, false otherwise - *) -let ringable = - let is_equality = function - | Cic.MutInd uri 0 [] when (eq uri eqt_uri) -> true - | _ -> false - in - let is_real = function - | Cic.Const (uri, _) when (eq uri r_uri) -> true - | _ -> false - in - function - | Cic.Appl (app::set::_::_::[]) when (is_equality app && is_real set) -> - warn "Goal Ringable!"; - true - | _ -> - warn "Goal Not Ringable :-(("; - false - - (** - split an equality goal of the form "t1 = t2" in its two subterms t1 and t2 - after checking that the goal is ringable - @param goal the current goal - @return a pair (t1,t2) that are two sides of the equality goal - @raise GoalUnringable if the goal isn't ringable - *) -let split_eq = function - | (Cic.Appl (_::_::t1::t2::[])) as term when ringable term -> - warn ("" ^ (CicPp.ppterm t1) ^ ""); - warn ("" ^ (CicPp.ppterm t2) ^ ""); - (t1, t2) - | _ -> raise GoalUnringable - - (** - @param i an integer index representing a 1 based number of node in a binary - search tree counted in a fbs manner (i.e.: 1 is the root, 2 is the left - child of the root (if any), 3 is the right child of the root (if any), 4 is - the left child of the left child of the root (if any), ....) - @param proof the current proof - @return an index representing the same node in a varmap (@see varmap_uri), - the returned index is as defined in index (@see index_uri) - *) -let path_of_int n = - let rec digits_of_int n = - if n=1 then [] else (n mod 2 = 1)::(digits_of_int (n lsr 1)) - in - List.fold_right - (fun digit path -> - Cic.Appl [ - mkCtor (if (digit = true) then right_idx_uri else left_idx_uri) []; - path]) - (List.rev (digits_of_int n)) (* remove leading true (i.e. digit 1) *) - (mkCtor end_idx_uri []) - - (** - Build a variable map (@see varmap_uri) from a variables array. - A variable map is almost a binary tree so this function receiving a var list - like [v;w;x;y;z] will build a varmap of shape: v - / \ - w x - / \ - y z - @param vars variables array - @return a cic term representing the variable map containing vars variables - *) -let btree_of_array ~vars = - let r = mkConst r_uri [] in (* cic objects *) - let empty_vm_r = mkCtor empty_vm_uri [quote_varmap_A_uri,r] in - let node_vm_r = mkCtor node_vm_uri [quote_varmap_A_uri,r] in - let size = Array.length vars in - let halfsize = size lsr 1 in - let rec aux n = (* build the btree starting from position n *) - (* - n is the position in the vars array _1_based_ in order to access - left and right child using (n*2, n*2+1) trick - *) - if n > size then - empty_vm_r - else if n > halfsize then (* no more children *) - Cic.Appl [node_vm_r; vars.(n-1); empty_vm_r; empty_vm_r] - else (* still children *) - Cic.Appl [node_vm_r; vars.(n-1); aux (n*2); aux (n*2+1)] - in - aux 1 - - (** - abstraction function: - concrete polynoms -----> (abstract polynoms, varmap) - @param terms list of conrete polynoms - @return a pair where aterms is a list of abstract polynoms - and varmap is the variable map needed to interpret them - *) -let abstract_poly ~terms = - let varhash = Hashtbl.create 19 in (* vars hash, to speed up lookup *) - let varlist = ref [] in (* vars list in reverse order *) - let counter = ref 1 in (* index of next new variable *) - let rec aux = function (* TODO not tail recursive *) - (* "bop" -> binary operator | "uop" -> unary operator *) - | Cic.Appl (bop::t1::t2::[]) - when (cic_is_const ~uri:(Some rplus_uri) bop) -> (* +. *) - Cic.Appl [mkCtor applus_uri []; aux t1; aux t2] - | Cic.Appl (bop::t1::t2::[]) - when (cic_is_const ~uri:(Some rmult_uri) bop) -> (* *. *) - Cic.Appl [mkCtor apmult_uri []; aux t1; aux t2] - | Cic.Appl (uop::t::[]) - when (cic_is_const ~uri:(Some ropp_uri) uop) -> (* ~-. *) - Cic.Appl [mkCtor apopp_uri []; aux t] - | t when (cic_is_const ~uri:(Some r0_uri) t) -> (* 0. *) - mkCtor ap0_uri [] - | t when (cic_is_const ~uri:(Some r1_uri) t) -> (* 1. *) - mkCtor ap1_uri [] - | t -> (* variable *) - try - Hashtbl.find varhash t (* use an old var *) - with Not_found -> begin (* create a new var *) - let newvar = - Cic.Appl [mkCtor apvar_uri []; path_of_int !counter] - in - incr counter; - varlist := t :: !varlist; - Hashtbl.add varhash t newvar; - newvar - end - in - let aterms = List.map aux terms in (* abstract vars *) - let varmap = (* build varmap *) - btree_of_array ~vars:(Array.of_list (List.rev !varlist)) - in - (aterms, varmap) - - (** - given a list of abstract terms (i.e. apolynomials) build the ring "segments" - that is triples like (t', t'', t''') where - t' = interp_ap(varmap, at) - t'' = interp_sacs(varmap, (apolynomial_normalize at)) - t''' = apolynomial_normalize_ok(varmap, at) - at is the abstract term built from t, t is a single member of aterms - *) -let build_segments ~terms = - let r = mkConst r_uri [] in (* cic objects *) - let rplus = mkConst rplus_uri [] in - let rmult = mkConst rmult_uri [] in - let ropp = mkConst ropp_uri [] in - let r1 = mkConst r1_uri [] in - let r0 = mkConst r0_uri [] in - let theory_args_subst varmap = - [abstract_rings_A_uri, r ; - abstract_rings_Aplus_uri, rplus ; - abstract_rings_Amult_uri, rmult ; - abstract_rings_Aone_uri, r1 ; - abstract_rings_Azero_uri, r0 ; - abstract_rings_Aopp_uri, ropp ; - abstract_rings_vm_uri, varmap] in - let theory_args_subst' eq varmap t = - [abstract_rings_A_uri, r ; - abstract_rings_Aplus_uri, rplus ; - abstract_rings_Amult_uri, rmult ; - abstract_rings_Aone_uri, r1 ; - abstract_rings_Azero_uri, r0 ; - abstract_rings_Aopp_uri, ropp ; - abstract_rings_Aeq_uri, eq ; - abstract_rings_vm_uri, varmap ; - abstract_rings_T_uri, t] in - let interp_ap varmap = - mkConst interp_ap_uri (theory_args_subst varmap) in - let interp_sacs varmap = - mkConst interp_sacs_uri (theory_args_subst varmap) in - let apolynomial_normalize = mkConst apolynomial_normalize_uri [] in - let apolynomial_normalize_ok eq varmap t = - mkConst apolynomial_normalize_ok_uri (theory_args_subst' eq varmap t) in - let rtheory = mkConst rtheory_uri [] in - let lxy_false = (** Cic funcion "fun (x,y):R -> false" *) - Cic.Lambda (Cic.Anonymous, r, - Cic.Lambda (Cic.Anonymous, r, - mkCtor false_uri [])) - in - let (aterms, varmap) = abstract_poly ~terms in (* abstract polys *) - List.map (* build ring segments *) - (fun t -> - Cic.Appl [interp_ap varmap ; t], - Cic.Appl ( - [interp_sacs varmap ; Cic.Appl [apolynomial_normalize; t]]), - Cic.Appl [apolynomial_normalize_ok lxy_false varmap rtheory ; t] - ) aterms - - -let status_of_single_goal_tactic_result = - function - proof,[goal] -> proof,goal - | _ -> - raise (Fail "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal") - -(* Galla: spostata in variousTactics.ml - (** - auxiliary tactic "elim_type" - @param status current proof engine status - @param term term to cut - *) -let elim_type_tac ~term ~status = - warn "in Ring.elim_type_tac"; - Tacticals.thens ~start:(cut_tac ~term) - ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status -*) - - (** - auxiliary tactic, use elim_type and try to close 2nd subgoal using proof - @param status current proof engine status - @param term term to cut - @param proof term used to prove second subgoal generated by elim_type - *) -let elim_type2_tac ~term ~proof ~status = - let module E = EliminationTactics in - warn "in Ring.elim_type2"; - Tacticals.thens ~start:(E.elim_type_tac ~term) - ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] ~status - -(* Galla: spostata in variousTactics.ml - (** - Reflexivity tactic, try to solve current goal using "refl_eqT" - Warning: this isn't equale to the coq's Reflexivity because this one tries - only refl_eqT, coq's one also try "refl_equal" - @param status current proof engine status - *) -let reflexivity_tac ~status:(proof, goal) = - warn "in Ring.reflexivity_tac"; - let refl_eqt = mkCtor ~uri:refl_eqt_uri ~exp_named_subst:[] in - try - apply_tac ~status:(proof, goal) ~term:refl_eqt - with (Fail _) as e -> - let e_str = Printexc.to_string e in - raise (Fail ("Reflexivity failed with exception: " ^ e_str)) -*) - - (** lift an 8-uple of debrujins indexes of n *) -let lift ~n (a,b,c,d,e,f,g,h) = - match (List.map (CicSubstitution.lift n) [a;b;c;d;e;f;g;h]) with - | [a;b;c;d;e;f;g;h] -> (a,b,c,d,e,f,g,h) - | _ -> assert false - - (** - remove hypothesis from a given status starting from the last one - @param count number of hypotheses to remove - @param status current proof engine status - *) -let purge_hyps_tac ~count ~status:(proof, goal as status) = - let module S = ProofEngineStructuralRules in - let rec aux n context status = - assert(n>=0); - match (n, context) with - | (0, _) -> status - | (n, hd::tl) -> - aux (n-1) tl - (status_of_single_goal_tactic_result (S.clear ~hyp:hd ~status)) - | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left" - in - let (_, metasenv, _, _) = proof in - let (_, context, _) = conj_of_metano goal metasenv in - let proof',goal' = aux count context status in - assert (goal = goal') ; - proof',[goal'] - -(** THE TACTIC! *) - - (** - Ring tactic, does associative and commutative rewritings in Reals ring - @param status current proof engine status - *) -let ring_tac ~status:((proof, goal) as status) = - warn "in Ring tactic"; - let eqt = mkMutInd (eqt_uri, 0) [] in - let r = mkConst r_uri [] in - let metasenv = metasenv_of_status ~status in - let (metano, context, ty) = conj_of_metano goal metasenv in - let (t1, t2) = split_eq ty in (* goal like t1 = t2 *) - match (build_segments ~terms:[t1; t2]) with - | (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin - List.iter (* debugging, feel free to remove *) - (fun (descr, term) -> - warn (descr ^ " " ^ (CicPp.ppterm term))) - (List.combine - ["t1"; "t1'"; "t1''"; "t1'_eq_t1''"; - "t2"; "t2'"; "t2''"; "t2'_eq_t2''"] - [t1; t1'; t1''; t1'_eq_t1''; - t2; t2'; t2''; t2'_eq_t2'']); - try - let new_hyps = ref 0 in (* number of new hypotheses created *) - Tacticals.try_tactics - ~status - ~tactics:[ - "reflexivity", EqualityTactics.reflexivity_tac ; - "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ; - "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ; - "exact sym_eqt su t1 ...", exact_tac - ~term:( - Cic.Appl - [mkConst sym_eqt_uri - [equality_is_a_congruence_A, mkConst r_uri [] ; - equality_is_a_congruence_x, t1'' ; - equality_is_a_congruence_y, t1 - ] ; - t1'_eq_t1'' - ]) ; - "elim_type eqt su t1 ...", (fun ~status -> - let status' = (* status after 1st elim_type use *) - let context = context_of_status ~status in - if not (are_convertible context t1'' t1) then begin - warn "t1'' and t1 are NOT CONVERTIBLE"; - let newstatus = - elim_type2_tac (* 1st elim_type use *) - ~status ~proof:t1'_eq_t1'' - ~term:(Cic.Appl [eqt; r; t1''; t1]) - in - incr new_hyps; (* elim_type add an hyp *) - match newstatus with - (proof,[goal]) -> proof,goal - | _ -> assert false - end else begin - warn "t1'' and t1 are CONVERTIBLE"; - status - end - in - let (t1,t1',t1'',t1'_eq_t1'',t2,t2',t2'',t2'_eq_t2'') = - lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'') - in - let status'' = - Tacticals.try_tactics (* try to solve 1st subgoal *) - ~status:status' - ~tactics:[ - "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2''; - "exact sym_eqt su t2 ...", - exact_tac - ~term:( - Cic.Appl - [mkConst sym_eqt_uri - [equality_is_a_congruence_A, mkConst r_uri [] ; - equality_is_a_congruence_x, t2'' ; - equality_is_a_congruence_y, t2 - ] ; - t2'_eq_t2'' - ]) ; - "elim_type eqt su t2 ...", (fun ~status -> - let status' = - let context = context_of_status ~status in - if not (are_convertible context t2'' t2) then begin - warn "t2'' and t2 are NOT CONVERTIBLE"; - let newstatus = - elim_type2_tac (* 2nd elim_type use *) - ~status ~proof:t2'_eq_t2'' - ~term:(Cic.Appl [eqt; r; t2''; t2]) - in - incr new_hyps; (* elim_type add an hyp *) - match newstatus with - (proof,[goal]) -> proof,goal - | _ -> assert false - end else begin - warn "t2'' and t2 are CONVERTIBLE"; - status - end - in - try (* try to solve main goal *) - warn "trying reflexivity ...."; - EqualityTactics.reflexivity_tac ~status:status' - with (Fail _) -> (* leave conclusion to the user *) - warn "reflexivity failed, solution's left as an ex :-)"; - purge_hyps_tac ~count:!new_hyps ~status:status')] - in - status'')] - with (Fail s) -> - raise (Fail ("Ring failure: " ^ s)) - end - | _ -> (* impossible: we are applying ring exacty to 2 terms *) - assert false - - (* wrap ring_tac catching GoalUnringable and raising Fail *) -let ring_tac ~status = - try - ring_tac ~status - with GoalUnringable -> - raise (Fail "goal unringable") - diff --git a/helm/gTopLevel/ring.mli b/helm/gTopLevel/ring.mli deleted file mode 100644 index b6eb34b69..000000000 --- a/helm/gTopLevel/ring.mli +++ /dev/null @@ -1,12 +0,0 @@ - - (* ring tactics *) -val ring_tac: ProofEngineTypes.tactic - -(*Galla: spostata in variuosTactics.ml - (* auxiliary tactics *) -val elim_type_tac: term: Cic.term -> ProofEngineTypes.tactic -*) - -(* spostata in variousTactics.ml -val reflexivity_tac: ProofEngineTypes.tactic -*) diff --git a/helm/gTopLevel/tacticals.ml b/helm/gTopLevel/tacticals.ml deleted file mode 100644 index 1319c13ca..000000000 --- a/helm/gTopLevel/tacticals.ml +++ /dev/null @@ -1,249 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -open CicReduction -open ProofEngineTypes -open UriManager - -(** DEBUGGING *) - - (** perform debugging output? *) -let debug = false - - (** debugging print *) -let warn s = - if debug then - prerr_endline ("TACTICALS WARNING: " ^ s) - - -(** TACTIC{,AL}S *) - - (* not a tactical, but it's used only here (?) *) - -let id_tac ~status:(proof,goal) = - (proof,[goal]) - - - (** - naive implementation of ORELSE tactical, try a sequence of tactics in turn: - if one fails pass to the next one and so on, eventually raises (failure "no - tactics left") - TODO warning: not tail recursive due to "try .. with" boxing - - Galla: is this exactly Coq's "First"? - - *) -let rec try_tactics ~(tactics: (string * tactic) list) ~status = - warn "in Tacticals.try_tactics"; - match tactics with - | (descr, tac)::tactics -> - warn ("Tacticals.try_tactics IS TRYING " ^ descr); - (try - let res = tac ~status in - warn ("Tacticals.try_tactics: " ^ descr ^ " succedeed!!!"); - res - with - e -> - match e with - (Fail _) - | (CicTypeChecker.NotWellTyped _) - | (CicUnification.UnificationFailed) -> - warn ( - "Tacticals.try_tactics failed with exn: " ^ - Printexc.to_string e); - try_tactics ~tactics ~status - | _ -> raise e (* [e] must not be caught ; let's re-raise it *) - ) - | [] -> raise (Fail "try_tactics: no tactics left") - - - -let thens ~start ~continuations ~status = - let (proof,new_goals) = start ~status in - try - List.fold_left2 - (fun (proof,goals) goal tactic -> - let (proof',new_goals') = tactic ~status:(proof,goal) in - (proof',goals@new_goals') - ) (proof,[]) new_goals continuations - with - Invalid_argument _ -> raise (Fail "thens: wrong number of new goals") - - - -let then_ ~start ~continuation ~status = - let (proof,new_goals) = start ~status in - List.fold_left - (fun (proof,goals) goal -> - let (proof',new_goals') = continuation ~status:(proof,goal) in - (proof',goals@new_goals') - ) (proof,[]) new_goals - - -(* Galla *) -(* si suppone che tutte le tattiche sollevino solamente Fail? *) - - -(* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *) - -(* This keep on appling tactic until it fails *) -(* When generates more than one goal, you have a tree of - application on the tactic, repeat_tactic works in depth on this tree *) - -let rec repeat_tactic ~tactic ~status = - warn "in repeat_tactic"; - try let (proof, goallist) = tactic ~status in - let rec step proof goallist = - match goallist with - [] -> (proof, []) - | head::tail -> - let (proof', goallist') = repeat_tactic ~tactic ~status:(proof, head) in - let (proof'', goallist'') = step proof' tail in - proof'', goallist'@goallist'' - in - step proof goallist - with - (Fail _) as e -> - warn ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e) ; - id_tac ~status -;; - - - -(* This tries to apply tactic n times *) - -let rec do_tactic ~n ~tactic ~status = - warn "in do_tactic"; - try - let (proof, goallist) = - if (n>0) then tactic ~status - else id_tac ~status in -(* else (proof, []) in *)(* perche' non va bene questo? stessa questione di ##### ? *) - let rec step proof goallist = - match goallist with - [] -> (proof, []) - | head::tail -> - let (proof', goallist') = do_tactic ~n:(n-1) ~tactic ~status:(proof, head) in - let (proof'', goallist'') = step proof' tail in - proof'', goallist'@goallist'' - in - step proof goallist - with - (Fail _) as e -> - warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ; - id_tac ~status -;; - - - -(* This applies tactic and catches its possible failure *) - -let rec try_tactic ~tactic ~status = - warn "in Tacticals.try_tactic"; - try - tactic ~status - with - (Fail _) as e -> - warn ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e); - id_tac ~status -;; - - -(* This tries tactics until one of them doesn't _solve_ the goal *) -(* TODO: si puo' unificare le 2(due) chiamate ricorsive? *) - -let rec solve_tactics ~(tactics: (string * tactic) list) ~status = - warn "in Tacticals.solve_tactics"; - match tactics with - | (descr, currenttactic)::moretactics -> - warn ("Tacticals.solve_tactics is trying " ^ descr); - (try - let (proof, goallist) = currenttactic ~status in - match goallist with - [] -> warn ("Tacticals.solve_tactics: " ^ descr ^ " solved the goal!!!"); -(* questo significa che non ci sono piu' goal, o che current_tactic non ne ha aperti di nuovi? (la 2a!) ##### *) -(* nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *) - (proof, goallist) - | _ -> warn ("Tacticals.solve_tactics: try the next tactic"); - solve_tactics ~tactics:(moretactics) ~status - with - (Fail _) as e -> - warn ("Tacticals.solve_tactics: current tactic failed with exn: " ^ Printexc.to_string e); - solve_tactics ~tactics ~status - ) - | [] -> raise (Fail "solve_tactics cannot solve the goal"); - id_tac ~status -;; - - - - - - - - - - - (** tattica di prova per debuggare i tatticali *) -(* -let thens' ~start ~continuations ~status = - let (proof,new_goals) = start ~status in - try - List.fold_left2 - (fun (proof,goals) goal tactic -> - let (proof',new_goals') = tactic ~status:(proof,goal) in - (proof',goals@new_goals') - ) (proof,[]) new_goals continuations - with - Invalid_argument _ -> raise (Fail "thens: wrong number of new goals") - -let prova_tac = - let apply_T_tac ~status:((proof,goal) as status) = - let curi,metasenv,pbo,pty = proof in - let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in - let rel = - let rec find n = - function - [] -> assert false - | (Some (Cic.Name name,_))::_ when name = "T" -> n - | _::tl -> find (n+1) tl - in - prerr_endline ("eseguo find"); - find 1 context - in - prerr_endline ("eseguo apply"); - apply_tac ~term:(Cic.Rel rel) ~status - in -(* do_tactic ~n:2 *) - repeat_tactic - ~tactic: - (then_ - ~start:(intros_tac ~name:"pippo") - ~continuation:(thens' ~start:apply_T_tac ~continuations:[id_tac ; apply_tac ~term:(Cic.Rel 1)])) -(* id_tac *) -;; -*) - - diff --git a/helm/gTopLevel/tacticals.mli b/helm/gTopLevel/tacticals.mli deleted file mode 100644 index b1861b5fa..000000000 --- a/helm/gTopLevel/tacticals.mli +++ /dev/null @@ -1,61 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - - -val id_tac : ProofEngineTypes.tactic - - - - (* pseudo tacticals *) -val try_tactics: - tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic - -val thens: - start: ProofEngineTypes.tactic -> - continuations: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic - -val then_: - start: ProofEngineTypes.tactic -> - continuation: ProofEngineTypes.tactic -> ProofEngineTypes.tactic - - -val repeat_tactic: - tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic - -val do_tactic: - n: int -> - tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic - -val try_tactic: - tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic - -val solve_tactics: - tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic - - - -(* -val prova_tac : ProofEngineTypes.tactic -*) diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml deleted file mode 100644 index 1df9128c1..000000000 --- a/helm/gTopLevel/variousTactics.ml +++ /dev/null @@ -1,206 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - - -(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio -chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una -funzione di callback che restituisce la (sola) hyp da applicare *) - -let assumption_tac ~status:((proof,goal) as status) = - let module C = Cic in - let module R = CicReduction in - let module S = CicSubstitution in - let _,metasenv,_,_ = proof in - let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let rec find n = function - hd::tl -> - (match hd with - (Some (_, C.Decl t)) when - (R.are_convertible context (S.lift n t) ty) -> n - | (Some (_, C.Def t)) when - (R.are_convertible context - (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n - | _ -> find (n+1) tl - ) - | [] -> raise (ProofEngineTypes.Fail "Assumption: No such assumption") - in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context)) -;; - -(* Questa invece era in fourierR.ml -let assumption_tac ~status:(proof,goal)= - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let num = ref 0 in - let tac_list = List.map - ( fun x -> num := !num + 1; - match x with - Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num))) - | _ -> ("fake",tcl_fail 1) - ) - context - in - Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal) -;; -*) - - -(* ANCORA DA DEBUGGARE *) - -(* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda -e li aggiunga nel context, poi si conta la lunghezza di questo nuovo -contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *) - -let generalize_tac ~term ~status:((proof,goal) as status) = - let module C = Cic in - let module P = PrimitiveTactics in - let module T = Tacticals in - let _,metasenv,_,_ = proof in - let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in -(* - let found = false in - let rec new_context context ty = - if ty == term then let found = true in context - else match ty with - C.Rel _ - | C.Var _ - | C.Meta _ (* ???? *) - | C.Sort s - | C.Implicit -> context - | C.Cast (val,typ) -> - let tmp_context = new_context context val in - tmp_context @ (new_context tmp_context typ) - | C.Prod (binder, source, target) -> - | C.Lambda (binder, source, target) -> - let tmp_context = new_context context source in - tmp_context @ (new_context tmp_context binder) - | C.LetIn (binder, term, target) -> - | C.Appl applist -> - let rec aux context = - match applist with - [] -> context - | hd::tl -> - let tmp_context = (new_context context hd) - in aux tmp_context tl - in aux context applist - | C.Const (uri, exp_named_subst) - | C.MutInd (uri, typeno, exp_named_subst) - | C.MutConstruct (uri, typeno, consno, exp_named_subst) -> - match exp_named_subst with - [] -> context - | (uri,t)::_ -> new_context context (type_of_aux' context t) - | _ -> assert false - | C.MutCase (uri, typeno, outtype, iterm, patterns) - | C.Fix (funno, funlist) - | C.CoFix (funno, funlist) -> - match funlist with - [] -> context (* caso possibile? *) - | (name, index, type, body)::_ -> - let tmp_context = ~ - in -*) - T.thens - ~start:(P.cut_tac - ~term:( - C.Prod( - (C.Name "dummy_for_gen"), - (CicTypeChecker.type_of_aux' metasenv context term), - (ProofEngineReduction.replace_lifting_csc 1 - ~equality:(==) - ~what:term - ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *) - ~where:ty) - ))) - ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac] - ~status -;; - - -(* IN FASE DI IMPLEMENTAZIONE *) - -let decide_equality_tac = -(* il goal e' un termine della forma t1=t2\/~t1=t2; la tattica decide se l'uguaglianza -e' vera o no e lo risolve *) - Tacticals.id_tac -;; - - -let compare_tac ~term ~status:((proof, goal) as status) = -(* term is in the form t1=t2; the tactic leaves two goals: in the first you have to *) -(* demonstrate the goal with the additional hyp that t1=t2, in the second the hyp is ~t1=t2 *) - let module C = Cic in - let module U = UriManager in - let module P = PrimitiveTactics in - let module T = Tacticals in - let _,metasenv,_,_ = proof in - let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in - let termty = (CicTypeChecker.type_of_aux' metasenv context term) in - match termty with - (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> - - let term' = (* (t1=t2)\/~(t1=t2) *) - C.Appl [ - (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/or.ind"), 0, [])) ; - term ; - C.Appl [ - (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 1, [])) ; - t1 ; - C.Appl [C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/not.con"), []) ; t2] - ] - ] - in - T.thens - ~start:(P.cut_tac ~term:term') - ~continuations:[ - T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; - decide_equality_tac] - | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> - let term' = (* (t1=t2) \/ ~(t1=t2) *) - C.Appl [ - (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/or.ind"), 0, [])) ; - term ; - C.Appl [ - (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind"), 1, [])) ; - t1 ; - C.Appl [C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/not.con"), []) ; t2] - ] - ] - in - T.thens - ~start:(P.cut_tac ~term:term') - ~continuations:[ - T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; - decide_equality_tac] - | _ -> raise (ProofEngineTypes.Fail "Compare: Not an equality") -;; - - -let discriminate_tac ~term ~status:((proof, goal) as status) = - let module C = Cic in - let module U = UriManager in - let module P = PrimitiveTactics in - let module T = Tacticals in - T.id_tac -;; - diff --git a/helm/gTopLevel/variousTactics.mli b/helm/gTopLevel/variousTactics.mli deleted file mode 100644 index 27b59682f..000000000 --- a/helm/gTopLevel/variousTactics.mli +++ /dev/null @@ -1,34 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -val assumption_tac: ProofEngineTypes.tactic - -val generalize_tac: term:Cic.term -> ProofEngineTypes.tactic - -(* -val decide_equality_tac: ProofEngineTypes.tactic -val compare_tac: term1:Cic.term -> term2:Cic.term -> ProofEngineTypes.tactic -*) - -- 2.39.2