From: Stefano Zacchiroli Date: Tue, 24 Feb 2004 16:09:38 +0000 (+0000) Subject: added functions and uris for binary {positive,integer} X-Git-Tag: v0_0_4~82 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9c015f8aeb17a9c2dc893208be09ac74b72b59c1;p=helm.git added functions and uris for binary {positive,integer} --- diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml index 913fc9ef3..dc621c5a9 100644 --- a/helm/ocaml/cic/helmLibraryObjects.ml +++ b/helm/ocaml/cic/helmLibraryObjects.ml @@ -155,9 +155,40 @@ module Peano = 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 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 end (** {2 Helpers for creating common terms} @@ -182,3 +213,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 +