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.
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
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
--- /dev/null
+(* 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
--- /dev/null
+(* 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
--- /dev/null
+(* 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
--- /dev/null
+(* 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
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
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 =
~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]))
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")
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
projects / helm.git / commitdiff