From ed207660b8a0fa34f1d34b9dbb41144c5be29e68 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 2 Jul 2005 14:42:46 +0000 Subject: [PATCH] All the equalityTactics have now been ported to use both the equality of Coq and that of Matita. Note: the only problematic tactic is replace that must pick an equality without any hint. Right now it always picks the one of matita. --- helm/ocaml/cic/.depend | 6 +++ helm/ocaml/cic/Makefile | 4 +- helm/ocaml/cic/libraryObjects.ml | 59 +++++++++++++++++++++++++ helm/ocaml/cic/libraryObjects.mli | 36 +++++++++++++++ helm/ocaml/cic/matitaLibraryObjects.ml | 35 +++++++++++++++ helm/ocaml/cic/matitaLibraryObjects.mli | 33 ++++++++++++++ helm/ocaml/tactics/equalityTactics.ml | 22 ++++----- 7 files changed, 183 insertions(+), 12 deletions(-) create mode 100644 helm/ocaml/cic/libraryObjects.ml create mode 100644 helm/ocaml/cic/libraryObjects.mli create mode 100644 helm/ocaml/cic/matitaLibraryObjects.ml create mode 100644 helm/ocaml/cic/matitaLibraryObjects.mli diff --git a/helm/ocaml/cic/.depend b/helm/ocaml/cic/.depend index 9cf7fc911..74dff2733 100644 --- a/helm/ocaml/cic/.depend +++ b/helm/ocaml/cic/.depend @@ -17,3 +17,9 @@ cicUtil.cmo: cic.cmo cicUtil.cmi cicUtil.cmx: cic.cmx cicUtil.cmi helmLibraryObjects.cmo: cic.cmo helmLibraryObjects.cmi helmLibraryObjects.cmx: cic.cmx helmLibraryObjects.cmi +matitaLibraryObjects.cmo: matitaLibraryObjects.cmi +matitaLibraryObjects.cmx: matitaLibraryObjects.cmi +libraryObjects.cmo: matitaLibraryObjects.cmi helmLibraryObjects.cmi \ + libraryObjects.cmi +libraryObjects.cmx: matitaLibraryObjects.cmx helmLibraryObjects.cmx \ + libraryObjects.cmi diff --git a/helm/ocaml/cic/Makefile b/helm/ocaml/cic/Makefile index 37009b545..9a3d05383 100644 --- a/helm/ocaml/cic/Makefile +++ b/helm/ocaml/cic/Makefile @@ -8,7 +8,9 @@ INTERFACE_FILES = \ deannotate.mli \ cicParser.mli \ cicUtil.mli \ - helmLibraryObjects.mli + helmLibraryObjects.mli \ + matitaLibraryObjects.mli \ + libraryObjects.mli IMPLEMENTATION_FILES = \ cic.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = cic.ml cic.cmi diff --git a/helm/ocaml/cic/libraryObjects.ml b/helm/ocaml/cic/libraryObjects.ml new file mode 100644 index 000000000..d9fb88f6b --- /dev/null +++ b/helm/ocaml/cic/libraryObjects.ml @@ -0,0 +1,59 @@ +(* Copyright (C) 2005, 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://helm.cs.unibo.it/ + *) + +(*CSC: how can we choose between the two libraries? *) +let eq_URI = + MatitaLibraryObjects.Equality.eq_URI + +let is_eq_URI uri = + UriManager.eq uri HelmLibraryObjects.Logic.eq_URI || + UriManager.eq uri MatitaLibraryObjects.Equality.eq_URI + +exception Not_recognized;; + +let something_URI coq matita ~eq = + if UriManager.eq eq HelmLibraryObjects.Logic.eq_URI then coq + else if UriManager.eq eq MatitaLibraryObjects.Equality.eq_URI then matita + else raise Not_found + +let eq_ind_URI = + something_URI + HelmLibraryObjects.Logic.eq_ind_URI + MatitaLibraryObjects.Equality.eq_ind_URI + +let eq_ind_r_URI = + something_URI + HelmLibraryObjects.Logic.eq_ind_r_URI + MatitaLibraryObjects.Equality.eq_ind_r_URI + +let sym_eq_URI = + something_URI + HelmLibraryObjects.Logic.sym_eq_URI + MatitaLibraryObjects.Equality.sym_eq_URI + +let trans_eq_URI = + something_URI + HelmLibraryObjects.Logic.trans_eq_URI + MatitaLibraryObjects.Equality.trans_eq_URI diff --git a/helm/ocaml/cic/libraryObjects.mli b/helm/ocaml/cic/libraryObjects.mli new file mode 100644 index 000000000..6a7bb1833 --- /dev/null +++ b/helm/ocaml/cic/libraryObjects.mli @@ -0,0 +1,36 @@ +(* Copyright (C) 2005, 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://helm.cs.unibo.it/ + *) + +(*CSC: how can we choose between the two libraries? *) +val eq_URI : UriManager.uri + +val is_eq_URI : UriManager.uri -> bool + +exception Not_recognized;; + +val eq_ind_URI : eq:UriManager.uri -> UriManager.uri +val eq_ind_r_URI : eq:UriManager.uri -> UriManager.uri +val trans_eq_URI : eq:UriManager.uri -> UriManager.uri +val sym_eq_URI : eq:UriManager.uri -> UriManager.uri diff --git a/helm/ocaml/cic/matitaLibraryObjects.ml b/helm/ocaml/cic/matitaLibraryObjects.ml new file mode 100644 index 000000000..33129ce4c --- /dev/null +++ b/helm/ocaml/cic/matitaLibraryObjects.ml @@ -0,0 +1,35 @@ +(* Copyright (C) 2004, 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://helm.cs.unibo.it/ + *) + +let uri = UriManager.uri_of_string;; + +module Equality = + struct + let eq_URI = uri "cic:/matita/equality/eq.ind" + let eq_ind_URI = uri "cic:/matita/equality/eq_ind.con" + let eq_ind_r_URI = uri "cic:/matita/equality/eq_ind_r.con" + let sym_eq_URI = uri "cic:/matita/equality/sym_eq.con" + let trans_eq_URI = uri "cic:/matita/equality/trans_eq.con" + end diff --git a/helm/ocaml/cic/matitaLibraryObjects.mli b/helm/ocaml/cic/matitaLibraryObjects.mli new file mode 100644 index 000000000..fd254622d --- /dev/null +++ b/helm/ocaml/cic/matitaLibraryObjects.mli @@ -0,0 +1,33 @@ +(* Copyright (C) 2004, 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://helm.cs.unibo.it/ + *) + +module Equality : + sig + val eq_URI : UriManager.uri + val eq_ind_URI : UriManager.uri + val eq_ind_r_URI : UriManager.uri + val sym_eq_URI : UriManager.uri + val trans_eq_URI : UriManager.uri + end diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 31c9b60b4..3d54fd18b 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -32,7 +32,6 @@ let rewrite_tac ~direction ~pattern equality = let module PER = ProofEngineReduction in let module PEH = ProofEngineHelpers in let module PT = PrimitiveTactics in - let module HLO = HelmLibraryObjects in assert (wanted = None); (* this should be checked syntactically *) assert (hyps_pat = []); (*CSC: not implemented yet! *) let proof,goal = status in @@ -43,18 +42,19 @@ let rewrite_tac ~direction ~pattern equality = in let curi, metasenv, pbo, pty = proof in let (metano,context,gty) as conjecture = CicUtil.lookup_meta goal metasenv in - let eq_uri = HLO.Logic.eq_URI in let ty_eq,_ = CicTypeChecker.type_of_aux' metasenv context equality CicUniv.empty_ugraph in let eq_ind, ty, t1, t2 = match ty_eq with - | C.Appl [C.MutInd (uri, 0, []); ty; t1; t2] when U.eq uri eq_uri -> - let eq_ind = - C.Const (if_right_to_left HLO.Logic.eq_ind_URI HLO.Logic.eq_ind_r_URI,[]) + | C.Appl [C.MutInd (uri, 0, []); ty; t1; t2] + when LibraryObjects.is_eq_URI uri -> + let ind_uri = + if_right_to_left LibraryObjects.eq_ind_URI LibraryObjects.eq_ind_r_URI in - if_right_to_left (eq_ind, ty, t2, t1) (eq_ind, ty, t1, t2) + let eq_ind = C.Const (ind_uri uri,[]) in + if_right_to_left (eq_ind, ty, t2, t1) (eq_ind, ty, t1, t2) | _ -> raise (PET.Fail "Rewrite: argument is not a proof of an equality") in (* now we always do as if direction was `LeftToRight *) let fresh_name = @@ -175,7 +175,7 @@ let replace_tac ~pattern ~with_what = ~start:( P.cut_tac (C.Appl [ - (C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, [])) ; + (C.MutInd (LibraryObjects.eq_URI, 0, [])) ; ty_of_with_what ; what ; with_what])) @@ -224,10 +224,10 @@ let symmetry_tac = let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) - when (U.eq uri HelmLibraryObjects.Logic.eq_URI) -> + when LibraryObjects.is_eq_URI uri -> ProofEngineTypes.apply_tactic (PrimitiveTactics.apply_tac - ~term: (C.Const (HelmLibraryObjects.Logic.sym_eq_URI, []))) + ~term: (C.Const (LibraryObjects.sym_eq_URI uri, []))) (proof,goal) | _ -> raise (ProofEngineTypes.Fail "Symmetry failed") @@ -246,11 +246,11 @@ let transitivity_tac ~term = let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) - when (uri = HelmLibraryObjects.Logic.eq_URI) -> + when LibraryObjects.is_eq_URI uri -> ProofEngineTypes.apply_tactic (T.thens ~start:(PrimitiveTactics.apply_tac - ~term: (C.Const (HelmLibraryObjects.Logic.trans_eq_URI, []))) + ~term: (C.Const (LibraryObjects.trans_eq_URI uri, []))) ~continuations: [PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac]) status -- 2.39.2