X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FhelmLibraryObjects.ml;h=3038582ab67e6ce60f6e573bb3dd27cd83fb4ed5;hb=a7063fc0997a9d9eae6c329443e67ab92c4b6a0f;hp=83f2d36479015f3d0626c6959a9b3a640a451c2b;hpb=b3bfd6b249600b15552c890306a635aee30c2a74;p=helm.git diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml index 83f2d3647..3038582ab 100644 --- a/helm/ocaml/cic/helmLibraryObjects.ml +++ b/helm/ocaml/cic/helmLibraryObjects.ml @@ -1,3 +1,30 @@ +(* 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://cs.unibo.it/helm/. + *) + +(* $Id$ *) + (** {2 Auxiliary functions} *) let uri = UriManager.uri_of_string @@ -24,30 +51,6 @@ let indconuri_of_uri uri = int_of_string (String.sub uri index_con (String.length uri - index_con))) -let term_of_uri ?(subst = []) uri = - let s = UriManager.string_of_uri uri in - try - (* Constant *) - (* TODO explicit substitutions? *) - let len = String.length s in - let sub = String.sub s (len -4) 4 in - if sub = ".con" then - const ~subst uri - else if sub = ".var" then - var ~subst uri - else - (try - (* Inductive Type *) - let (uri, typeno) = indtyuri_of_uri s in - mutind ~subst uri typeno - with - | UriManager.IllFormedUri _ | Failure _ | Invalid_argument _ -> - (* Constructor of an Inductive Type *) - let (uri, typeno, consno) = indconuri_of_uri s in - mutconstruct ~subst uri typeno consno) - with - | Invalid_argument _ | Not_found -> raise (UriManager.IllFormedUri s) - (** {2 Helm's objects shorthands} *) module Logic = @@ -80,15 +83,6 @@ module Logic = let absurd_URI = uri "cic:/Coq/Init/Logic/absurd.con" end -module Logic_Type = - struct - let eqt_URI = uri "cic:/Coq/Init/Logic_Type/eqT.ind" - let sym_eqt_URI = uri "cic:/Coq/Init/Logic_Type/sym_eqT.con" - - let refl_eqt = mutconstruct eqt_URI 0 1 - let sym_eqt = const sym_eqt_URI - end - module Datatypes = struct let bool_URI = uri "cic:/Coq/Init/Datatypes/bool.ind" @@ -105,15 +99,20 @@ module Reals = let r_URI = uri "cic:/Coq/Reals/Rdefinitions/R.con" let rplus_SURI = "cic:/Coq/Reals/Rdefinitions/Rplus.con" let rplus_URI = uri rplus_SURI - let rminus_URI = uri "cic:/Coq/Reals/Rdefinitions/Rminus.con" - let rmult_URI = uri "cic:/Coq/Reals/Rdefinitions/Rmult.con" - let rdiv_URI = uri "cic:/Coq/Reals/Rdefinitions/Rdiv.con" + let rminus_SURI = "cic:/Coq/Reals/Rdefinitions/Rminus.con" + let rminus_URI = uri rminus_SURI + let rmult_SURI = "cic:/Coq/Reals/Rdefinitions/Rmult.con" + let rmult_URI = uri rmult_SURI + let rdiv_SURI = "cic:/Coq/Reals/Rdefinitions/Rdiv.con" + let rdiv_URI = uri rdiv_SURI let ropp_SURI = "cic:/Coq/Reals/Rdefinitions/Ropp.con" let ropp_URI = uri ropp_SURI let rinv_SURI = "cic:/Coq/Reals/Rdefinitions/Rinv.con" let rinv_URI = uri rinv_SURI - let r0_URI = uri "cic:/Coq/Reals/Rdefinitions/R0.con" - let r1_URI = uri "cic:/Coq/Reals/Rdefinitions/R1.con" + let r0_SURI = "cic:/Coq/Reals/Rdefinitions/R0.con" + let r0_URI = uri r0_SURI + let r1_SURI = "cic:/Coq/Reals/Rdefinitions/R1.con" + let r1_URI = uri r1_SURI let rle_SURI = "cic:/Coq/Reals/Rdefinitions/Rle.con" let rle_URI = uri rle_SURI let rge_SURI = "cic:/Coq/Reals/Rdefinitions/Rge.con" @@ -122,8 +121,9 @@ module Reals = let rlt_URI = uri rlt_SURI let rgt_SURI = "cic:/Coq/Reals/Rdefinitions/Rgt.con" let rgt_URI = uri rgt_SURI - let rtheory_URI = uri "cic:/Coq/Reals/Rbase/RTheory.con" - let rinv_r1_URI = uri "cic:/Coq/Reals/Rbase/Rinv_R1.con" + let rtheory_URI = uri "cic:/Coq/Reals/RIneq/RTheory.con" + let rinv_r1_URI = uri "cic:/Coq/Reals/RIneq/Rinv_1.con" + let pow_URI = uri "cic:/Coq/Reals/Rfunctions/pow.con" let r = const r_URI let rplus = const rplus_URI @@ -138,8 +138,10 @@ module Peano = struct let plus_SURI = "cic:/Coq/Init/Peano/plus.con" let plus_URI = uri plus_SURI - let minus_URI = uri "cic:/Coq/Init/Peano/minus.con" - let mult_URI = uri "cic:/Coq/Init/Peano/mult.con" + let minus_SURI = "cic:/Coq/Init/Peano/minus.con" + let minus_URI = uri minus_SURI + let mult_SURI = "cic:/Coq/Init/Peano/mult.con" + let mult_URI = uri mult_SURI let pred_URI = uri "cic:/Coq/Init/Peano/pred.con" let le_SURI = "cic:/Coq/Init/Peano/le.ind" let le_URI = uri le_SURI @@ -148,18 +150,51 @@ module Peano = let ge_URI = uri ge_SURI let lt_SURI = "cic:/Coq/Init/Peano/lt.con" let lt_URI = uri lt_SURI - let gt_SURI = "cic:/Coq/Init/Peano/lt.con" + let gt_SURI = "cic:/Coq/Init/Peano/gt.con" let gt_URI = uri gt_SURI - let lt_URI = uri "cic:/Coq/Init/Peano/lt.con" let plus = const plus_URI let mult = const mult_URI let pred = const pred_URI end +module BinPos = + struct + let positive_SURI = "cic:/Coq/NArith/BinPos/positive.ind" + let positive_URI = uri positive_SURI + let xI = mutconstruct positive_URI 0 1 + let xO = mutconstruct positive_URI 0 2 + let xH = mutconstruct positive_URI 0 3 + let pplus_SURI = "cic:/Coq/NArith/BinPos/Pplus.con" + let pplus_URI = uri pplus_SURI + let pplus = const pplus_URI + let pminus_SURI = "cic:/Coq/NArith/BinPos/Pminus.con" + let pminus_URI = uri pminus_SURI + let pminus = const pminus_URI + let pmult_SURI = "cic:/Coq/NArith/BinPos/Pmult.con" + let pmult_URI = uri pmult_SURI + let pmult = const pmult_URI + end + module BinInt = struct + let zmult_URI = uri "cic:/Coq/ZArith/BinInt/Zmult.con" + let zmult = const zmult_URI let zplus_SURI = "cic:/Coq/ZArith/BinInt/Zplus.con" + let zplus_URI = uri zplus_SURI + let zplus = const zplus_URI + let zminus_SURI = "cic:/Coq/ZArith/BinInt/Zminus.con" + let zminus_URI = uri zminus_SURI + let zminus = const zminus_URI + let z_SURI = "cic:/Coq/ZArith/BinInt/Z.ind" + let z_URI = uri z_SURI + let z0 = mutconstruct z_URI 0 1 + let zpos = mutconstruct z_URI 0 2 + let zneg = mutconstruct z_URI 0 3 + let zopp_SURI = "cic:/Coq/ZArith/BinInt/Zopp.con" + let zopp_URI = uri zopp_SURI + let zopp = const zopp_URI + let zpower_URI = uri "cic:/Coq/ZArith/Zpower/Zpower.con" end (** {2 Helpers for creating common terms} @@ -184,3 +219,12 @@ let build_real n = in aux n +let build_bin_pos n = + if n < 1 then raise NegativeInteger; + let rec aux = function + | 1 -> BinPos.xH + | n when n mod 2 = 0 -> Cic.Appl [ BinPos.xO; aux (n / 2) ] + | n -> Cic.Appl [ BinPos.xI; aux (n / 2) ] + in + aux n +